IMO 2026 赛场上,NVIDIA 的 Nemotron 系统作为正式参赛者拿到 30/42 分,超过 29 分的金牌线,全部答卷由官方阅卷人评分:P1、P2、P4、P5 拿满分,P3 和 P6 各得 1 分。与依赖形式化证明器的 AlphaProof 路线不同,这套系统从头到尾只用自然语言——不用形式化证明器、不调外部工具、不联网,吃进官方 LaTeX 题面,吐出人类可读的证明。9 月 9 日团队把整条管线写成技术报告挂上 arXiv(arXiv:2609.10712),金牌配方可复现。
三个 checkpoint,一套 16 票全票制
管线骨架是迭代式「生成—验证—精炼」。生成侧由三个 Nemotron 3 Ultra checkpoint 组成:公开基座 GA,加上分别经 SFT 和 RL 后训练的两个专家。第一轮每题生成 384 个证明尝试——每个 checkpoint 从 8 个互补提示词各采样 16 次,提示词分别引导引理分解、路线对比、反例搜索等不同解题策略。
验证侧由 RL、SFT 两个 checkpoint 充当免参考验证器:每个证明收 16 个独立判分,满分 1 分、小错 0.5 分、致命错误 0 分,16 票全部给满才算「接受」。无人过线时,系统从证明池挑排名前 16 的候选,附上最多 8 条验证批评送回三个模型精炼,每轮 192 次新尝试,最多迭代 8 轮。
后训练的增益有硬数字
30 题开发集上,两个后训练专家全面压过基座:8 轮搜索加兜底后,RL 管线累计 180 分、SFT 165 分,GA 基座只有 162 分(独立评审团口径)。预算怎么花更划算,论文给出了直接对照:RL 单模型把尝试加到 256 次只接受 14 题;换成 RL 与 SFT 各 128 次的混合池,接受题数涨到 18。团队对此的结论是:第二个 checkpoint 能解出第一个解不出的题,而给单个 checkpoint 翻倍采样增益甚微——换模型比堆采样值钱。
算力账本:7 亿 token 找齐全部证明
四个满分证明在开赛后 76 分钟内全部通过终选面板,另两题也在 100 分钟内定稿;全部 6 个提交证明约耗 7.07 亿 token、1464 个 GB200 GPU 小时,把在途轮次跑满则总计约 23.1 亿 token、4800 GPU 小时。赛后复盘留了个警示:切断时刻两套模型验证器都给出约 32 分的估计,比官方评分高 2 分,差额全部来自 P3 和 P6——模型评审在同一批证明上集体看走眼,这是模型验证的共性盲区,不是某一家的噪声。
五件套全开源,561B 权重直接下载
HF collection(nvidia/nemotron-labs-imo-2026)里躺着两个 561B 专家 checkpoint(OpenMDW-1.1 许可)、13.3 万条 SFT 语料加 9600 条 RL 题集(CC BY 4.0),以及与 Titu Andreescu 教授合作的 200 题全新基准 Nemotron-IMO-Bench;推理代码进 NeMo-Skills,RL 配方进 NeMo-RL,连提交的证明原文都在。论文结论值得抄下来:光堆生成规模不够,收益来自互补的后训练 checkpoint、验证制导精炼,以及花在终选上的算力——更花哨的路由和激进过滤,反而会把后来被证明正确的候选提前扔掉。
对做推理系统的人,这份配方的价值不在分数本身,而在每一步都带消融数字和算力账,可以直接对答案。