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

事件概述

9 月 9 日，NVIDIA 公布了 Nemotron 3 Ultra 在 2026 年国际数学奥林匹克（IMO）中使用的整套数学推理系统。该模型最终获得 30/42 分，超过当届 29 分的金牌线。与传统依赖形式化证明器或外部工具不同，该系统仅使用自然语言进行证明书写。此次开源不仅包含模型权重，还涵盖了两个数学专家 checkpoint、SFT 与 RL 训练数据、推理代码、训练配方以及 200 道新的 Nemotron-IMO-Bench 测试题，旨在提供从训练到比赛推理的全套系统方案。

核心技术与架构

1. 多 Checkpoint 策略降低采样相关性
系统未对单一模型反复采样，而是训练了两个行为差异显著的数学专家模型，结合通用版形成三份不同的解题偏好 checkpoint：

• SFT 专家：除了生成完整证明，还学习了证明修改、验证和再次验证的轨迹。这使得模型能够识别已有证明中的局部错误并进行修补，而非从头开始重新作答，从而保留前次计算的有效结构。
• RL 专家：通过强化学习调整生成分布，提高成功闭合证明路线的概率，压低导致死路的选项。这并非增加新数学知识，而是优化已有能力的出现频率。
• 效果：不同后训练策略降低了候选证明间的相关性，使有限算力能覆盖更多证明空间，显著提升了有效样本量。

2. 动态证明搜索池（Proof Pool）
系统首轮为每道题生成 384 份证明，并将其放入持续更新的搜索池中。验证器将证明分为三类：直接通过、需修补、价值低。高评分且存在问题的证明会被保留，并将验证器的批改意见作为方向信号送回模型进行多轮改写（Refinement）。这种机制结合了搜索宽度（首轮大量生成）和深度（后续沿高质量路径推进），避免了暴力采样的重复劳动。

3. 验证困境：共享底座的错误相关性
系统采用高接受门槛（需两个专家全票通过）以降低错误放行率，但这导致了高误拒率。更关键的问题在于，SFT、RL 和通用版模型共享同一底座（Nemotron 3 Ultra），拥有相似的知识结构和推理习惯。这导致验证判断高度相关：

• 共同盲区：当错误源于模型共有的理解偏差时，增加检查次数无法发现漏洞（如某例证中三个模型均未识别出的对称性错误）。
• 验证偏差：验证器既可能因共享盲区放过错误证明，也可能因门槛过高压住部分正确的有价值证明。
• 结论：单纯增加同类模型的检查次数收益有限，未来需引入基础模型各异、专门反例生成器或形式化证明器等多样化组件来降低同时失效的概率。

行业影响与挑战

1. 极高的硬件门槛
尽管开源了软件配方，但复现该系统需要 550B 参数规模的模型、TB 级显存以及数千个 GB200 GPU 小时。以 8 张 B200 显卡运行约 1,464 小时为例，其成本将全球绝大多数高校实验室拒之门外。这表明 AI 领域已实现“代码平权”，但“算力主权”仍被少数巨头垄断。

2. 科研范式转移
该案例揭示了 AI for Science 的新协作模式：AI 巨头承担海量、枯燥的逻辑推演体力活，而人类科学家的角色从“寻找证据者”转变为“逻辑审判者”。虽然 NVIDIA 通过开源分享了 IMO 金牌的红利，但也强化了其硬件定义的推理范式，用户若想复现成功，仍需依赖其高端算力基础设施。