Nemotron IMO Gold 精读：开源模型金牌的完整配方
题目：An Open Recipe for IMO Gold: Training Nemotron for Olympiad Mathematics 链接：https://arxiv.org/abs/2609.10712 代码：HF collection
nvidia/nemotron-labs-imo-2026；NeMo-Skills 训练配方；NeMo-RL 指南 团队：NVIDIA（Ivan Moshkov, Stephen Ge, George Armstrong, Wei Du, Sadegh Mahdavi, Igor Gitman 等） 数据日：2026-09-12（HF 日榜第 9 名，22 赞）
一、题目与背景
IMO（国际数学奥林匹克）证明题是自然语言数学推理的最高峰。当前两条路线分野：形式化路线（AlphaProof/Lean 系）把问题翻译成形式语言后用证明器搜索——可靠但需人工形式化且脱离自然语言；自然语言路线直接生成人类可读证明——流畅但无法机器验证，错误随题目难度骤增。NVIDIA 选择了后者的系统化：不追求形式化保证，而用验证与选择的工程冗余弥补单次生成的不可靠。
背景的另一层：同日 25 位菲尔兹奖得主联合声明抗议"AI 公司把解数学题当基准跑分"。本文恰好是一个观察窗口——当 IMO 成绩成为 AI 竞技场，数学共同体的抗议与 NVIDIA 的开放配方形成微妙对照。论文本身对这层张力只字未提。
二、研究定位
前序脉络：Google DeepMind 的 AlphaProof/AlphaGeometry 混合路线（2024 银牌水平、形式化验证）；各家开源推理模型在 AIMO 类竞赛的选择题/数值题上刷分，但自然语言证明生成（无法对答案的选择）系统性落后。本文定位：首个公开完整配方（模型+数据+代码+推理策略）的自然语言 IMO 金牌系统，价值在于可复现性与方法论透明，而非单点分数。
三、问题定义
抽象问题：当生成器在难任务上单点错误率不可忽略、且无形式化验证器可用时，如何组织测试时计算使"系统级正确率"达标？
形式化：给定问题集 Q 与生成器族 {G_sft, G_rl}，设计管线（生成 → 验证 V → 精炼 R → 元选择 S）使最终提交得分的期望最大化，约束是全程自然语言（无 Lean/外部工具/检索）。
四、解法
训练侧：Nemotron 3 Ultra（GA 版）之上，用大规模自然语言证明语料 SFT 得到证明生成专精 checkpoint；再用可验证奖励 RL（证明被验证器接受的奖励信号）得到 RL checkpoint。两个 specialist 与 GA 模型构成三模型池。
推理侧（测试时搜索管线）：
- 迭代搜索：三 checkpoint 各自生成候选证明 → 独立验证器 checkpoint 检查证明逻辑（分步验证而非整体判断）→ 未通过者送精炼器改写 → 循环。
- 高算力终选：每个问题积累大量候选后，一个独立的元选择阶段（含 IMO 风格 judge prompt 与 jury reconciliation prompt）在候选间精挑最终提交——把"哪个证明最可能被人类阅卷者接受"变成一个独立的评估问题。
- 失败实验的诚实披露：附录 A 记录了三种没用的尝试（跨证明上下文、zero-first 排序、分诊式精炼路由）——这部分对复现者价值极高。
五、实验结果
| 项 | 结果 |
|---|---|
| IMO 2026 官方成绩 | 30/42（金牌线） |
| 单 checkpoint 管线 | 显著低于三模型集成（7.1 vs 7.2/7.3 节对照） |
| 验证器贡献 | 消融显示验证过滤是候选质量的主要来源 |
| 开放 artifact | 2 checkpoint + SFT 数据（Nemotron-Math-Proofs-v3-SFT）+ RL 题集 + 训练/推理代码 + 提交证明 + Nemotron-IMO-Bench（200 新题） |
实验设计的证明力：IMO 是对抗污染的近乎完美测试（题目赛前绝密），30/42 不可刷分；论文把管线每个环节（checkpoint 选择、验证、精炼、终选）的贡献在 7.1-7.3 节逐层拆解，读者可以看清"金牌 = 生成质量 × 选择质量"中每个因子的权重——这比只报总分的工作方法论价值高一个量级。
六、知识反推
作者必须掌握：（1）可验证奖励 RL 的设计（证明可验证性如何转化为奖励信号）；（2）验证器训练——分步验证与整体判断的差异；（3）测试时搜索的算力分配策略（生成-验证-精炼-终选的预算划分）；（4）奥数证明的人类评分标准（IMO judge prompt 的设计需要阅卷经验）；（5）大规模分布式推理工程。
融合节点：把"生成器不可靠"当作给定条件，转而优化选择结构——这是从单模型思维到系统思维的转变，与 METR 式"AI 任务工时"评测背后"系统组合产出"的世界观一致。
七、通用灵感
- 把"生成质量"瓶颈转化为"选择质量"工程问题（论文证据：单 checkpoint vs 三模型集成的显著差距）：当单点不可靠时，冗余+独立验证+精挑的系统设计比继续训练单模型更有效。推广：代码生成（生成多候选+验证器+选择器已是 SWE 方向标配）、科学假设生成、任何"生成分数高但错误不可容忍"的场景。
- 失败实验的披露是复现性的核心（论文证据：附录 A 三种失败路径）：告诉社区"这条路不通"与告诉"这条路通"同样有价值。推广：科研写作、工程 postmortem 文化。
- 对抗污染评测的黄金标准是"赛前绝密"（Nemotron-IMO-Bench 200 新题）：自建新题基准比在旧基准上刷分可信一个量级。推广：一切 benchmark 构造。