英伟达开源IMO金牌级数学推理方案：不靠形式化证明器的30分

据 SegmentFault 思否《AI日报（2026年9月13日）》报道，英伟达发布了一套基于 Nemotron 3 Ultra 的纯自然语言奥数推理方案，在2026年国际数学奥林匹克（International Mathematical Olympiad，简称 IMO）中取得30分，达到金牌分数线。整套系统不依赖形式化证明器，也不调用外部工具。

这一点是理解该方案价值的关键。过去几年，AI 在数学竞赛上的高分路线大多要借助 Lean 一类的形式化证明系统，把自然语言题目翻译成机器可验证的证明脚本，再由求解器搜索。这条路有效，但代价明显：能翻译成形式化语言的题目才做得动，而现实里的数学问题多数并不长成那个样子。英伟达这次选择纯自然语言推理，把“能不能解题”和“能不能形式化”这两件事分开了。

更新于 2026-09-14。本文数据均来自公开报道。

一、30分是怎么拿到的

按报道描述，系统由两个经有监督微调（Supervised Fine-Tuning，简称 SFT）与强化学习专门训练的模型检查点构成，配合一条测试期计算（test-time compute）流水线，做迭代生成与自我验证。简单说，模型不是一次性给出答案，而是生成候选解法、逐条检验、再修正，把推理预算花在“多想几遍”上。

维度	该方案的做法	常见做法的差异
题目形式	纯自然语言，直接读题作答	需先翻译为形式化语言
外部依赖	不调用形式化证明器与外部工具	依赖求解器或代码执行环境
算力投放	测试期计算流水线迭代生成与验证	单次前向输出答案
评测成绩	IMO 2026 取得30分，达到金牌线	视题型适用范围波动大

把“测试期计算”单独拎出来说，是因为它改变了成本结构：分数不再只由训练规模决定，也可以由推理时的计算量决定。对使用者来说，这意味着同一套权重可以按需在“快而省”和“慢而准”之间调节，不必为高难度任务单独训练一个大模型。

另一个容易被忽略的点是评测的可复现性。报道提到该方案只使用自然语言与题目本身，不借助外部工具，意味着任何团队只要拿到同样的题目集与权重，就能在自己的机器上复现成绩，不必等待官方打榜。对做产品验收的人来说，这条性质比分数本身更有用——可复现，才意味着它能被当作基线使用。

二、开源了什么：三类资产

本次同步开放的内容分为三类：

模型侧：两个经有监督微调与强化学习专门训练的检查点；
工程侧：训练与推理代码，以及完整的求解记录；
评测侧：Nemotron-IMO-Bench 基准，收录200道奥数难题。

对做教育工具、解题产品与评测体系的一人公司来说，后两类资产比权重更实用。求解记录让“模型是怎么错的”可被复盘，200道难题则提供了一套现成的验收标准——把自家产品挂上去跑一遍，就能知道差距出在解题能力、还是出在题目理解与输出格式。

三、评测范式的分歧：数学家为什么不满

据腾讯研究院《AI速递 20260914》整理，陶哲轩、Peter Scholze、邓煜等25位菲尔兹奖得主此前发表公开声明，指出把解题当基准测试的竞赛式推进正在损害数学科学与学术共同体。声明提到三层意思：解题只是工具，根本目标是概念理解与洞见；以越来越快的速度批量生产真假命题，可能摧毁的是一片沃土；仓促发布的解答来不及规范写作与引用先行工作，还会引发成果归属与剽窃争议。

两件事放在一起看并不矛盾。工业界用竞赛题衡量推理能力，是工程上的合理选择，题目有标准答案、便于横向比较；数学界担心的是，当刷分成为唯一指挥棒，激励结构会被改写，愿意花五年啃一个猜想的人会变少。对企业用户而言，这条争论的现实提醒是：基准分数只能证明“能解这类题”，不能直接推导出“能解决你的业务问题”。