英伟达于 9 月 9 日公开了 Nemotron 3 Ultra 在 2026 年国际数学奥林匹克（IMO）上使用的整套数学推理系统。该系统最终获得 30/42 分，超过当届 29 分的金牌线。整个比赛过程中，模型仅以自然语言书写证明，没有调用 Lean 等形式化证明器，也没有借助外部工具或联网检索。
与成绩一同发布的，是支撑这 30 分的完整链路：两个数学专家 checkpoint、SFT 与 RL 训练数据、推理代码、训练配方、比赛提交证明，以及 200 道新的 Nemotron-IMO-Bench。换言之，英伟达公开的不是一个更强的数学模型，而是一套从训练到比赛推理的系统。Nemotron 3 Ultra 是底座，两个专家模型、大规模证明搜索、模型验证与多轮改写共同把成绩推到了金牌线。
这一发布有其背景。两天后的 9 月 11 日，陶哲轩、Peter Scholze、Maryna Viazovska 等 25 位菲尔兹奖得主联合发声，批评 AI 数学成果发布越来越快，而证明检查、方法梳理和复现往往没有足够时间展开。在这样的氛围里，英伟达把模型、数据、推理流程和计算成本一并留下，显得较为少见。
技术起点上，英伟达没有对同一个 Nemotron 3 Ultra 反复采样，而是先训练了两个行为明显不同的数学专家。SFT 数据中除了完整证明，还加入了大量证明修改、验证和再次验证的轨迹，使模型不仅会从题目生成证明，还能在拿到一份写了一半甚至局部有误的证明后，判断问题所在并沿原路线继续修补。RL 专家则处理另一层问题：改变证明路线被抽中的概率。IMO 级题目的证明空间非常稀疏，强化学习根据成功与失败轨迹重新调整生成分布，让能完整闭合的思路获得更高权重，压低反复走入死路的选择。
通用版、SFT 和 RL 三份 checkpoint 由此形成三种不同的解题偏好。搜索效果取决于有效样本量，而非表面生成数量。若同一模型连续生成 200 份证明，其中大部分围绕同几种构造打转，候选之间相关性越高，新增计算提供的新信息越少。加入经过不同后训练的 checkpoint，相当于主动改变采样分布，让算力进入另一片证明空间。实验显示，继续增加同一个 RL 模型的采样，收益很快放缓；把 SFT 专家加入后，即使生成预算接近，能够覆盖的问题明显增加。
首轮生成阶段，Nemotron 会为每道题生成 384 份证明，但这些答案并非终点，而是进入一个持续更新的搜索池。每份证明经验证后分为直接通过、方向可用但需修补、路线价值较低三类。系统不会简单删除后两类，而是保留评分较高的证明，再把验证器指出的问题送回模型继续修改。多轮改写因此不是反复润色同一篇答案，每轮都会重新产生多个候选，再次进入全局证明池与之前的路线竞争。某条证明若持续获得较高评价，算力会继续沿该路径投入；若修改几轮仍无法解决关键漏洞，就会逐渐失去扩展机会。
这种搜索也有天然限制：自然语言数学证明没有像围棋那样明确的规则系统，一个证明可能前面几十步全部成立，只在最后用了一个并不存在的对称性。于是 verifier 不仅负责打分，还会直接影响计算资源的流向。为降低错误证明被放行的概率，英伟达把接受门槛设得很高：两个专家反复检查同一份证明，只有所有判断全部通过，候选才会被接受。实验显示，提高门槛能明显减少错误证明通过，但代价是大量正确证明也被挡在外面。
更深一层的困难在于验证判断并不独立。SFT、RL 和通用版虽经不同后训练，却共享同一个 Nemotron 3 Ultra 底座，拥有大量相似的知识结构、概念表示和推理习惯。当错误来自随机疏忽时，多次检查可以降低风险；当错误来自几个模型共同拥有的理解盲区时，增加检查次数的效果就会明显减弱。论文中一份涉及列置换对称性的错误证明即为典型：证明本身存在可明确构造的反例，但三个 checkpoint 反复判断，没有一个识别出关键漏洞。第 6 题则从另一边说明问题：系统投入大量计算后得到一份新证明，内部验证未放行，但人工复核认为其中包含相当部分正确内容，可拿到部分分数。这意味着 verifier 同时存在两类偏差——错误证明因共享盲区被高置信度放过，有价值证明又因门槛保守被压下去。
因此，这条路线后续面对的并非只是训练一个更强的数学裁判，而是怎样让不同验证组件拥有尽量不同的错误来源。不同基础模型可负责交叉检查，专门的反例生成器可主动寻找推翻关键步骤的构造，符号系统可处理适合机械核验的代数关系，部分局部命题也可转交形式化证明器。生成端可以依靠更多模型、更大的搜索池和更深的修改链扩大覆盖；验证端面对的则是错误相关性，继续增加同一类模型的检查次数，收益会更快进入平台期。
开源之后，30/42 可以被还原成一组具体的系统变量，外部团队能改变 checkpoint 组合、sampling budget、verifier threshold 和 refinement 深度，再看成绩如何变化。但这与完整重跑 30 分仍是两回事：550B 级模型、TB 级显存以及数千个 GB200 GPU 小时依然构成很高的硬件门槛；Nemotron 3 Ultra 通用版自身的完整后训练链也没有做到逐阶段复刻，英伟达官方文档明确写明，部分中间 teacher 和 MOPD checkpoint 尚未开放。
从产业视角看，这条链把问题暴露得很清楚：证明生成可以依靠更多 proposal 和更多 test-time compute 继续扩展，验证却还没有同样稳定的 scaling 路线。下一步真正难处理的，是怎样让 verifier 的错误不再与 generator 高度重合。即便配方全开，8 张 B200 显卡与 1,464 小时的长考成本，依然是一道将全球绝大多数高校实验室拒之门外的硬墙。这种“只能看、买不起”的现状，被视为未来 AI4S 竞赛的预演：代码平权已经实现，但算力主权仍被少数巨头垄断。
英伟达的这套打法也揭示了未来科学发现的一种协作新范式：过去数学家多是单打独斗的独奏者，而在暴力推理时代，AI 巨头烧掉数百万美金的电费，把枯燥、重复、海量的逻辑可能性全部铲平。这并不意味着数学家的消亡，而是意味着数学家角色的位移——从寻找证据的人变成审判逻辑的人。这份报告对基础研究最大的尊重，或许不在于那 30 分的成绩，而在于它传递的信号：算力可以完成最脏最累的体力活，但关于真理的最终裁决、关于验证逻辑的一致性，仍需仰仗人类的直觉。