9月9日，英伟达公布了其Nemotron 3 Ultra模型在2026年国际数学奥林匹克竞赛（IMO）中使用的整套数学推理系统。该系统最终获得30分（满分42分），超过当届29分的金牌线。比赛过程中，模型仅使用自然语言书写证明，未调用Lean等形式化证明器，也未借助外部工具或联网检索。英伟达同时开源了支撑该成绩的两个数学专家checkpoint、SFT与RL训练数据、推理代码、训练配方、比赛提交证明，以及200道新的Nemotron-IMO-Bench测试集。
此次开源的核心并非单一更强的数学模型，而是一套从训练到推理的完整系统。Nemotron 3 Ultra作为底座模型，配合两个数学专家模型、大规模证明搜索、模型验证与多轮改写，构成了将成绩推至金牌线的完整链路。这一动作发生在25位菲尔兹奖得主联合发声批评AI数学成果发布过快、复现与检查不足的两天之后。陶哲轩、Peter Scholze、Maryna Viazovska等学者于9月11日联名指出，当前AI数学成果的证明检查与方法梳理往往缺乏足够时间展开。在此背景下，英伟达将金牌级结果背后的模型、数据、推理流程与计算成本一并公开，具有不同的行业意义。
该系统的技术起点在于，英伟达并未对同一个Nemotron 3 Ultra反复采样，而是先训练了两个行为特征不同的数学专家模型。其中SFT专家的训练数据不仅包含完整证明，还加入了大量证明修改、验证与再验证轨迹。这使得模型学到的能力不仅是从题目生成证明，还包括在拿到一份局部存在错误的证明后，判断问题所在并沿原路线继续修正。在搜索系统中，这种能力直接影响计算资源的利用效率。高难数学题很少只有会做与不会做两种状态，大量候选证明处于中间区域——主体结构接近可用，仅在某个引理、边界条件或推导闭环上存在问题。仅会重新作答的模型每次失败后都需重新进入整个证明空间，而接受过修改训练的模型可将已有证明作为中间状态继续推进，保留前次计算中已找到的有效结构。
RL专家则处理另一层问题：如何调整证明路线的采样概率。IMO级题目的证明空间极为稀疏，模型可能已具备解决某类问题所需的局部能力，但正确组合仅占生成分布中极小部分。强化学习根据成功与失败轨迹重新调整生成分布，使能够完整闭合证明的思路获得更高权重，反复进入死路的选择被压低。这一过程并未增加新的数学知识，而是重新安排模型已有能力出现的频率。通用版、SFT与RL三份checkpoint由此形成三种不同的解题偏好。搜索效果取决于有效样本量，而非表面生成的答案数量。若同一模型连续生成200份证明且大部分围绕同几种构造，则200份文本并不等于200条独立路线。候选之间相关性越高，新增计算提供的新信息越少。加入经过不同后训练的checkpoint，相当于主动改变采样分布，使计算资源进入另一片证明空间。英伟达实验显示，继续增加同一RL模型的采样，收益很快放缓；加入SFT专家后，即使生成预算接近，可覆盖的问题明显增加。
在首轮生成阶段，系统为每道题生成384份证明。这些证明并未被当作终点，而是进入一个持续更新的搜索池。每份证明经过验证后分为三类：直接通过、整体方向可用但存在需修补的问题、路线价值较低。系统不会简单删除后两类，而是保留评分较高的证明，并将验证器指出的问题送回模型继续修改。这一机制改变了推理过程的性质。普通多次采样是从起点不断重新出发，每次生成彼此之间几乎没有记忆；而proof pool将历史计算保留下来，一条路线走到什么位置、哪里出了问题、哪些部分仍然可用，都会成为下一轮搜索的输入。验证器给出的批改信息在此承担方向信号的角色。自然语言证明没有连续可微的目标函数，系统无法像训练神经网络那样直接计算下一步方向，批改意见起到近似作用，告诉模型当前证明与可接受答案之间的差距，refinement再围绕该局部区域继续寻找。
多轮改写并非对同一篇答案反复润色。每轮都会重新产生多个候选，这些候选再次进入全局证明池，与之前的路线一起竞争。某条证明若持续获得较高评价，计算资源会继续沿该路径投入；若修改几轮后仍无法解决关键漏洞，则逐渐失去继续扩展的机会。由此，系统同时具备搜索宽度与搜索深度：首轮数百份证明负责铺开搜索空间，后续多轮refinement让接近正确的路线继续推进，无需每次重新开始。这与简单暴力采样的区别在于，暴力采样依赖从固定分布中不断抽取新样本，而该系统根据已出现候选的质量，动态决定下一批计算继续投入哪些路线。
这种搜索存在一个天然限制：自然语言数学证明缺乏类似围棋那样明确的规则系统。围棋搜索中，一个动作是否合法可直接判断，终局输赢也有确定答案；而自然语言证明中，一个证明前面几十步可能全部成立，仅在最后使用了一个并不存在的对称性，也可能某一步写得较为跳跃但整体数学思路仍然成立。因此verifier在系统中不仅负责给答案打分，还会直接影响计算资源的流向。它认为某条路线值得保留，该路线才会继续获得修改机会；它认为某份证明已经成立，搜索可能提前停止。验证误差在此已不只是评分偏差，还会进一步影响后续搜索路径。搜索规模越大，verifier对整体结果的影响越明显。
为降低错误证明被放行的概率，英伟达将接受门槛设得很高：两个专家反复检查同一份证明，只有所有判断全部通过，候选才会被接受。这一设计与搜索系统的成本结构有关。正确证明被误判，损失主要是算力，因为系统还可继续修改；错误证明一旦被接受，影响更大，可能让搜索提前停在错误答案上。因此系统选择接受较高的误拒率。从行业视角看，此次开源将IMO金牌级数学推理的完整工程链路——包括双专家checkpoint设计、384路初始生成、基于proof pool的多轮搜索以及高门槛验证机制——置于公开可查的状态。对于企业级AI推理系统的构建者而言，这套方案提供了一种在有限算力下提升有效样本覆盖率的工程思路，其价值不仅限于数学竞赛场景。
该文观点仅代表作者本人，企服科学平台仅提供信息存储空间服务。
