An Open Recipe for IMO Gold: Training Nemotron for Olympiad Mathematics
Ivan Moshkov, Stephen Ge, George Armstrong, Wei Du, Sadegh Mahdavi, Igor Gitman
cs.AI
2026-09-10
NVIDIA从Nemotron 3 Ultra训出两个证明专精检查点，配生成-验证-精修搜索，全程自然语言、不用形式化证明器。IMO 2026官方评分30/42，金牌线29。
IMO 已经变成大模型证明能力的公开考场。2024 年 AlphaProof 加 AlphaGeometry 2 用形式化工具摸到银牌附近；2025 年 Gemini Deep Think 和 OpenAI 实验模型用自然语言拿到金牌。缺的是一份可复现的开源配方：检查点怎么训、验证怎么设、测试时算力怎么花。
NVIDIA 这条线从 Nemotron 3 Ultra（550B-A55B）出发，问题很窄：只做自然语言证明，不接 Lean、不接工具、不联网。目标是把后训练和推理编排的贡献拆开，并公开到别人能重跑。
三个检查点：原版 GA，从 GA 做长上下文 SFT 的 Ultra-SFT，从 GA 做 RL 的 Ultra-RL。SFT 语料 414,890 条，覆盖证明生成、精修、验证和元验证，最大序列 425,984 token，512 张 GB200，选 step 1300。RL 用 9,597 道「四次尝试中对 1 到 3 次」的中等难度题，奖励基本跟 DeepSeekMath-V2，去掉自分析项。
比赛管线两段。
搜索：三个检查点一起生成。第 1 轮 384 次尝试（每检查点 × 8 套策略提示 × 16 条）。验证只用 RL 和 SFT，每份证明各打 8 次分，16 票全给 1 才算内部接受。没接受就从池子里挑最多 16 份，带上至多 8 条评语，三个检查点各采 4 条，每轮 192 次精修，最多 8 轮。
终选：每个生成检查点最多留 1 个决赛证明，三个检查点用 IMO 风格 0-7 分各打 16 次，共 48 次，取均值，平手取更短的交。
官方评分 30/42，金牌线 29。P1、P2、P4、P5 满分，P3 和 P6 各 1 分。四道满分证明在开赛 76 分钟内过终选，全部提交在 100 分钟内定稿。提交证明对应约 707M 生成 token、1,464 GB200 小时；整场跑完约 2.31B token、4,800 GPU 小时。
赛后继续搜，第 8 轮 P6 出了一份新证明，内部验证器没接受，独立人类评委给 4/7（无官方评分细则），总分可到 33，不是官方成绩。P3 没有改善。
30 题开发集上，单检查点端到端陪审团分：GA 162、SFT 165、RL 180；三人集成 188。第 1 轮把算力从 RL 128 次加倍到 256 次，接受题只多 1 道；同样 token 分给 SFT 64 次，接受题从 13 增到 15。RL 128 + SFT 128 接受 18 道，其中 5 道只有 SFT 能中，RL 加倍只追回 1 道。
验证审计 300 份证明：提交的 RL+SFT 全票通过，误接受约 1.1%、误拒绝约 81%。门槛放到 14/16，误接受升到 17%。25 份内部接受里，陪审团给 23 份满分，1 份 6 分，1 份 0 分（对称性步骤是错的），三个检查点都打了满分，任何全票规则都拦不住。
这是目前最完整的开源自然语言 IMO 金牌配方：检查点、数据、训练和推理代码、提交证明、算力账单、200 道新题基准都公开。对要复现或往下做的人，可执行的结论比分数更有用：多检查点互补强过单检查点加倍采样；验证器必须宁严勿松，因为误接受会提前停搜；终选要另花一轮高算力，搜索时的验证提示不够当评分用。
这也把代价摊在桌上。金牌线是用几千 GPU 小时堆出来的，而且模型评审在 P3、P6 上比官方多给了 2 分。
作者承认模型验证器和独立模型陪审团在 P3、P6 上有共同盲区，都把只得 1 分的证明估到更高。25 份内部接受里仍有一份完全错误的证明漏过全票规则。开发集只有 30 题，完整 200 题基准没有用高算力管线跑完。集成实验和单检查点也不是算力对齐的。
更刺的一点：全程自然语言意味着正确性没有形式保证。公开配方能复现流程，复现 30 分仍然要同等量级的 GB200。