英伟达开源 IMO 数学推理系统：1.5TB 显存门槛下的算力壁垒与验证困境

事件概述

2026 年 9 月 9 日，NVIDIA 公布了 Nemotron 3 Ultra 在 2026 年国际数学奥林匹克（IMO）中使用的完整数学推理系统。该系统最终得分 30/42，超过当届 29 分的金牌线。与传统依赖形式化证明器或外部工具不同，该系统仅使用自然语言进行证明生成。NVIDIA 同时开源了支撑这一成绩的核心资产，包括两个数学专家 Checkpoint、SFT 与 RL 训练数据、推理代码、训练配方、比赛提交证明，以及新增的 200 道 Nemotron-IMO-Bench 测试题。

此次开源的背景是学术界对 AI 快速发布数学成果却缺乏严谨审查的担忧。2026 年 9 月 11 日，包括陶哲轩、Peter Scholze 在内的 25 位菲尔兹奖得主联合发声，批评 AI 数学成果的验证滞后。NVIDIA 的开源行为旨在提供透明性，但其背后的硬件门槛也引发了关于“代码平权”与“算力集权”的讨论。

核心技术与架构

1. 双专家 Checkpoint 策略
系统并未单纯依赖单一模型的反复采样，而是训练了两个行为差异显著的数学专家模型，以优化搜索效率：

• SFT 专家：侧重于证明的修改与验证。训练数据包含大量证明修改、验证及再次验证的轨迹，使模型具备从局部错误的中间状态继续推进的能力，而非每次失败后重新从头生成。
• RL 专家：侧重于调整生成分布。通过强化学习根据成功或失败轨迹重新加权，提高能闭合证明的思路权重，压低无效路径，从而在有限的算力下覆盖更多样的证明空间。

这种多 Checkpoint 设计降低了候选答案之间的相关性，使得首轮生成的 384 份证明具有更高的信息密度。

2. 动态证明搜索池（Proof Pool）
系统采用持续更新的搜索池机制，而非简单的暴力采样：

• 初始生成：每道题首先生成 384 份证明。
• 分类处理：验证器将证明分为三类：直接通过、需修补（方向可用但有瑕疵）、价值低。高评分且需修补的证明会被保留，并将验证器的批改意见作为方向信号送回模型进行多轮 Refinement（改写）。
• 资源动态分配：接近正确的路线会持续获得计算资源投入，而长期无法解决关键漏洞的路径则被淘汰。这种机制结合了搜索的宽度（首轮广撒网）和深度（多轮精修）。

验证困境与挑战

尽管系统取得了金牌成绩，但在验证环节暴露出了显著的技术瓶颈：

1. 验证器的错误相关性
系统采用了严格的“全票通过”机制，即两个专家必须一致判断证明正确才会放行，以降低错误接受率。然而，由于 SFT、RL 和通用版模型共享同一个 Nemotron 3 Ultra 底座，它们拥有相似的知识结构和推理习惯。这导致当出现基于共同理解盲区的错误时，多个验证器会同时失效。例如，一份存在构造反例的错误证明被三个 Checkpoint 一致误判为正确。

2. 验证偏差的两难
实验显示，提高验证门槛虽减少了错误证明的通过，但也拦截了大量包含部分正确内容、可获部分分数的有价值证明。这表明当前的验证组件存在两类偏差：一是因共享盲区导致的错误放行，二是因过于保守导致的有价值证明被压。

3. 未来改进方向
单纯增加同一类模型的检查次数收益有限。未来的验证体系可能需要引入异构组件，如不同基础模型的交叉检查、专门的反例生成器、符号系统进行代数核验，以及形式化证明器处理局部命题，以减少验证组件在同一位置同时失效的概率。

算力壁垒与现实影响

尽管 NVIDIA 开源了完整的“配方”，但复现其 IMO 金牌成绩仍面临极高的硬件门槛：

• 硬件要求：需要 550B 参数规模的模型支持，涉及 TB 级显存需求。
• 计算成本：据估算，类似规模的推理过程需要约 8 张 B200 显卡运行 1,464 小时，消耗数千个 GB200 GPU 小时。
• 数据缺失：官方文档指出，部分中间 Teacher 和 MOPD Checkpoint 尚未开放，完整重跑 30 分的成绩几乎不可能。

这一现状揭示了 AI for Science（AI4S）竞赛中的新范式：巨头通过巨额算力投入铲平了繁琐的逻辑可能性，而普通实验室即便拥有开源代码，也因无法承担高昂的算力成本而被拒之门外。数学家的角色正从“寻找证据的人”向“审判逻辑的人”转变，但最终的算力主权仍掌握在少数拥有顶级硬件设施的机构手中。