Nemotron摘得IMO金牌：开源奥数证明生成全流程解密

数学奥林匹克竞赛长期被视为衡量AI推理能力的试金石。它要求的不只是计算，而是需要严密的逻辑链条、创造性的思路和完整的自然语言证明。NVIDIA研究团队最新发布的论文《An Open Recipe for IMO Gold》给出了一个引人注目的答案：基于Nemotron 3 Ultra训练的系统，在IMO 2026中取得了42分中的30分，达到金牌门槛。

更关键的是，团队没有把成果锁进闭源黑箱，而是公开了训练后的模型权重、训练数据、训练与推理代码、提交的解答，以及一个全新的评测基准。这为整个开源社区提供了一份可复现的"金牌配方"。

全程自然语言，没有形式化证明器

这套系统最值得关注的设计取向，是它完全运行在自然语言层面。它不依赖形式化证明器（formal prover），不调用任何外部工具，也没有联网访问权限。

这与此前一些数学AI的思路形成鲜明对比。过去不少高水平数学推理系统会借助Lean、Coq等形式化验证工具，把证明转化为机器可检验的符号形式。这种做法能保证严谨性，但也把问题限定在可形式化的范畴内，且工程复杂度极高。

Nemotron的路线选择了更贴近人类解题方式的自然语言证明生成——直接读题、写出推理过程、给出完整论证。这意味着模型必须在没有外部"裁判"兜底的情况下，自己保证逻辑的正确性。能在这种约束下达到金牌水平，说明大模型的原生推理能力已经达到了相当的高度。

从通用模型到专家检查点

整个方案的起点是Nemotron 3 Ultra。团队在此基础上，通过监督微调（SFT）和强化学习（RL）训练出两个专门针对奥数的"专家检查点"（specialist checkpoints）。

研究重点考察了三个方面对证明质量的影响：检查点的选择、验证机制、以及答案的迭代精炼（refinement）。这三者构成了后训练阶段的核心变量。SFT让模型先学会奥数证明的表达范式和解题套路，RL则进一步优化其在难题上的推理策略与稳定性。

这种"通用模型 + 专家化后训练"的分层思路，反映出当前大模型能力构建的一个主流范式：基座提供广泛的知识与语言能力，后训练则把能力聚焦到特定的高难度任务上。

三模型协同的测试时计算流水线

真正让分数达标的，是一套精心设计的测试时计算（test-time compute）流水线。系统同时调用三个Nemotron 3 Ultra检查点——通用版本加上两个后训练专家——来驱动一个迭代式搜索过程。

这个流程可以拆解为三个环节：

生成、验证与精炼的迭代循环

多个模型协同生成候选证明，随后对这些证明进行验证，找出漏洞或错误，再据此精炼改进。这个"生成—验证—精炼"的循环不断迭代，逐步逼近正确且完整的解答。这种自我验证与修正的机制，弥补了单次生成容易出错的缺陷。

高算力选择阶段

在迭代产出多个候选之后，还有一个独立的高算力阶段负责挑选每道题的最终提交答案。换言之，系统不是简单地相信第一个看起来对的答案，而是投入额外的计算资源做最终裁决。

这种设计印证了近年来"以推理时算力换取推理质量"的趋势——与其单纯堆砌参数，不如在推理阶段让模型"多想几遍、反复检查"，从而在困难任务上获得显著提升。

开源的分量与新基准Nemotron-IMO-Bench

这项工作最大的社区价值在于它的开放程度。团队释放了两个后训练检查点、训练数据、训练和推理代码，以及实际提交的解答。这意味着其他研究者不仅能看到结果，还能完整复现整条路径。

另一边，团队还推出了Nemotron-IMO-Bench——一个包含200道全新奥数级别难题的基准测试集。奥数AI研究长期面临一个隐患：网络上的经典题目很可能已经进入训练数据，导致"刷分"而非真正的推理能力评估。一个由新题构成的基准，能更公正地衡量模型的泛化推理水平。

这对AI推理意味着什么

IMO金牌门槛的达成，本身是一个象征性的里程碑，但更值得琢磨的是它背后的方法论启示。

它表明，在不借助形式化工具的前提下，纯自然语言的大模型系统已经能处理人类顶尖学生级别的数学证明。而达成这一点的关键，不只是更强的基座模型，还有后训练的专家化、多模型协同、以及测试时的迭代搜索与验证。

对整个行业而言，这份"开源配方"降低了高水平数学推理研究的门槛，也为如何在真实困难任务上组织推理流水线提供了一个可参考的工程范式。当模型能力、后训练策略与推理时计算三者被系统性地组合起来，AI在严肃推理领域的能力边界正在被持续推远。