英伟达开源其IMO验证方案，同时利用一点五太字节显存门槛巩固其AI算力垄断地位。

9月9日，英伟达（NVIDIA）在2026年国际数学奥林匹克竞赛（IMO）上发布了驱动 Nemotron 3 Ultra 的完整数学推理系统。该系统最终得分30分（满分42分），超过了当年金牌分数线29分。在整个比赛过程中，该模型仅使用自然语言生成证明，未调用 Lean 等形式化证明器、外部工具或网络搜索。然而，此次发布的意义远超分数本身。英伟达同时开源了支撑这一30分成绩的两个数学专家检查点（checkpoints），以及监督微调（SFT）和强化学习（RL）训练数据集、推理代码、训练配方、竞赛提交证明，并新增了200道精心策划的 Nemotron-IMO-Bench 题目。本质上，发布的内容不仅仅是一个更强的独立数学模型，而是一个涵盖从训练到竞赛推理的全流程管道。Nemotron 3 Ultra 作为基础底座；随后的专家模型、大规模证明搜索、模型验证和多轮重写共同构成了将性能提升至金牌标准的完整链条。

两天后的9月11日，包括陶哲轩（Terence Tao）、彼得·舒尔茨（Peter Scholze）和玛丽娜·维亚佐夫斯卡（Maryna Viazovska）在内的25位菲尔兹奖得主发表联合声明，批评人工智能生成的数学出版物加速涌现，指出由于时间不足，证明验证、方法论澄清和可重复性研究始终滞后。在此背景下，英伟达的开源方式脱颖而出，因为它刻意保留了实现 IMO 金牌水平结果所需的底层模型、数据、推理工作流和计算成本。

技术架构始于对反复采样单一 Nemotron 3 Ultra 检查点的有意背离。相反，英伟达训练了两个表现出截然不同行为的数学专家。Nemotron 的核心设计原则之一是将后训练直接对齐到下游搜索操作。SFT 数据集不仅包含完整的证明，还包含大量的证明修改、验证和再验证轨迹。因此，训练出的模型不仅学会了如何从头生成证明，还学会了如何诊断部分撰写或局部错误的草稿中的缺陷，并沿着原始轨迹继续完善。当集成到搜索系统中时，这种能力从根本上改变了计算资源的利用方式。高难度数学问题很少处于“可解”或“不可解”的二元状态；大量候选方案处于中间地带，其结构框架几乎可行，仅在特定引理、边界条件或推导闭合处失败。一个只能从头重启的模型会在每次失败时重新进入整个证明空间，而一个经过修改训练的模型则将现有证明视为中间状态，从而有效地保留先前计算中发现的有效结构。

RL 专家解决了另一层问题：调整不同证明路径的选择概率。IMO 级别问题的证明空间极其稀疏。虽然模型可能具备解决某些类型问题所需的局部能力，但正确的组合排列仅占生成分布的一小部分。单纯增加采样量可能会最终遇到正确路径，但如果大多数样本仍聚集在相似区域，扩展计算量在实际覆盖面上带来的收益微乎其微。此处的 RL 根据成功和失败的轨迹重新校准生成分布。成功闭合证明的路径获得更高权重，而反复将模型引入死胡同的选择则受到抑制。这并没有发明新的数学知识；它重新分配了模型现有能力显现的频率。结合基础模型、SFT 和 RL 检查点，确立了三种截然不同的解题先验。这种差异对于下游搜索至关重要，因为有效性取决于有效的样本多样性，而非原始输出量。如果单个模型连续生成200个证明，其中大部分围绕相同的构造展开，那么200篇文本并不等同于200条独立路径。较高的候选相关性会降低额外计算的信息产出。引入经过不同后训练的检查点会主动改变采样分布，将计算资源引导至替代的证明空间。英伟达的实验证实了这一点：扩展单一 RL 模型的采样会导致收益迅速递减，而在相似的生成预算下，整合 SFT 专家显著扩大了问题覆盖率。因此，此处的后训练超越了单纯的单模型能力提升。SFT 实现了迭代式证明修改，RL 调节高价值路径的出现频率，多检查点部署降低了候选相关性。它们共同解决了如何在有限的推理计算中最大化证明路径覆盖的问题——这是后续384次初始生成有效运作的前提。高度重复的候选方案即使面对庞大的搜索池也会使其失效。

在每道题产生首批384个证明后，实际的搜索过程开始。这些第一轮答案不被视为终点，而是被存入持续更新的证明池中。经过验证后，每个证明归入三类之一：完全接受、方向可行但需修补，或战略价值低。系统并未直接丢弃后两类，而是保留高分证明，并将验证器识别出的问题反馈给模型进行针对性完善。这一步从根本上改变了推理循环的性质。传统的多次采样从零开始重启，生成相互独立且无记忆的输出。相比之下，Nemotron 的证明池保留了历史计算。它追踪每条路径的状态、发生了哪些失败以及哪些组件仍可使用，并将这些上下文直接输入后续的搜索轮次。验证器反馈充当方向信号。自然语言证明缺乏连续、可微的目标函数，无法像神经网络训练那样进行基于梯度的直接导航。评分意见作为一种近似手段，精确指示当前证明与可接受解决方案偏离的位置，使完善工作能够针对局部缺口进行。因此，多轮重写并非仅仅是表面修饰。每次迭代都会衍生出多个新候选者，重新进入全局证明池，与之前的路径竞争。维持高评价的证明吸引持续的计算投入；在经过几次完善周期后未能解决关键漏洞的证明逐渐失去扩展机会。这种架构同时实现了搜索的广度和深度。最初的数百个证明绘制了搜索空间地图，而随后的多轮完善允许近乎正确的路径在不频繁重启的情况下逐步推进。这使得 Nemotron 区别于依赖从固定分布中持续提取的朴素暴力采样。在这里，动态计算分配直接响应新兴候选者的质量。

尽管如此，这种搜索方法面临固有的限制。与国际象棋或围棋不同，数学证明生成缺乏明确的规则系统。在围棋中，着法的合法性可以即时验证，游戏结果是确定性解决的。自然语言数学不提供如此低成本验证的手段。证明可能在数十步都完美无缺，却在最后一行使用了不存在的对称性；或者看似突兀的一步，却建立在有效的整体数学直觉之上。因此，Nemotron 中的验证器不仅仅是打分，它还主动决定计算路由。被认为值得保留的路径获得持续的完善机会；标记为完成的路径触发早期搜索终止。验证错误因此超越了单纯的评分偏差；它们直接塑造后续的搜索轨迹。随着搜索规模的扩大，验证器对整体结果的影响成比例增强。

为了最小化错误接受证明的风险，英伟达设定了极高的接受阈值：两位专家独立验证同一证明，必须达成一致才能接受。这一设计与系统的成本结构相一致。误判正确证明主要导致计算开销，因为系统可以简单地重试；误判错误证明后果更严重，可能会在错误答案上过早停止搜索。因此，系统容忍更高的假阴性率以换取更低的假阳性率。实验结果证实，提高阈值显著减少了错误接受，尽管代价是阻挡了大量有效证明。如果挑战仅在于阈值校准，权衡便只是计算支出与错误率之间的平衡。然而，Nemotron 暴露了一个更深层的结构局限：验证判断并非统计独立。尽管 SFT、RL 和基础变体经历了不同的后训练，但它们共享相同的 Nemotron 3 Ultra 基础。它们继承了高度相似的知识结构、概念表示和推理启发式方法。当错误源于随机疏忽时，重复检查可降低风险；当错误源于共同的认知盲区时，增量验证的收益急剧递减。论文引用了一个涉及置换对称性的证明，其中包含易于构建的反例，但所有三个检查点都反复未能识别出关键缺陷。问题不在于审查不足，而在于模型间的高度相关错误。如果评估者源自不同的架构，一方的盲区可由另一方弥补；如果它们共享广泛的训练和表示结构，多个评估者可能同时认可同一个错误前提。增加投票共识稳定了内部一致性，但这种稳定性并不自动转化为更高的数学可信度。

案例6进一步说明了这种不对称性。在系统投入大量计算生成新颖证明后，内部验证仍未批准，但人类评审员发现了值得部分给分的大量正确内容。这揭示了双重验证器偏见：共同的盲区允许错误证明以高置信度通过，而过于保守的阈值则压制了有价值的证明。因此，随后的技术障碍不仅在于训练一个更强的数学裁判，更在于工程化具有最大误差差异的验证组件。部署不同的基础模型进行交叉检查、专用的反例生成器以主动探测关键步骤、用于机械可验证代数关系的符号系统，以及用于局部命题的形式化证明器，共同降低了在相同逻辑节点同时发生组件故障的概率。在此阶段，生成和验证呈现出 fundamentally 不同的扩展动态。生成通过增加模型、更大的搜索池和更深的完善链来扩展；验证则面临误差相关性。不断添加来自同一模型类别的检查点会导致更快的停滞。

随着两个专家检查点、SFT 和 RL 数据集、推理代码、RL 配方、提交证明以及200道 Nemotron-IMO-Bench 题目的公开，30/42 的分数可还原为一组透明的系统变量。外部团队可以操纵检查点组合、采样预算、验证器阈值和完善深度，以观察性能变化。然而，这与完全复现30分的运行仍有天壤之别。5500亿参数的模型、太字节级的显存需求以及数千小时的 GB200 GPU 算力构成了 formidable 的硬件壁垒。此外，英伟达官方文档明确指出，Nemotron 3 Ultra 基础变体的完整后训练链并非完全可复现，某些中间教师模型和 MOPD 检查点仍处于封闭状态。尽管如此，IMO 管道揭示了一个关键现实：证明生成可以通过增加提案和测试时计算无限扩展，而验证目前缺乏同样稳定的扩展轨迹。下一个严峻的挑战是将验证器误差与生成器相关性解耦。

剖析这一事件揭示了一个残酷的真相：尽管配方完全公开，但八块 B200 GPU 和1,464小时的扩展计算仍然是一道难以逾越的高墙，将全球99%的大学实验室排除在外。这种“可见却负担不起”的现实是对未来科学人工智能（AI4S）竞赛的预览。代码公平已经实现，但计算主权仍由少数科技巨头垄断。英伟达的战略为科学发现照亮了一种新的协作范式。历史上，数学家作为孤独的演奏者运作。在暴力推理时代，AI 公司消耗数百万美元电费，系统地消除繁琐、重复且海量巨大的逻辑可能性。这并不意味着数学家的过时，而是其功能的位移：从“证据寻找者”变为“逻辑裁判”。英伟达的报告通过对学术界发出的清晰信号——计算可以处理最艰苦、重复性的劳动，但对真理和逻辑一致性的最终裁决必须依靠人类直觉——展现了对基础研究的深刻尊重，而非仅仅通过30分这一指标。或许，这代表了科技巨头在暴力计算时代对基础研究最体面的回应。

回到开篇的隐喻，“延伸敕令”通过将利益分配给中立方以抵消阻力而取得成功。今天，英伟达通过开源将 IMO 金牌的红利分发全球，却无意中让每位参与者都陷入由英伟达硬件定义的搜索和推理范式。当研究人员试图使用发布的蓝图复制这一成功时，他们很快意识到，他们唯一可行的前进道路就是购买更多的英伟达 GPU。

参考文献：https://arxiv.org/pdf/2609.10712 | https://mathandai.org/

郑佳梅原创报道 | 岑峰编辑 | 雷锋网发布