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