Nemotron 开源路线冲击 IMO 金牌：自然语言证明如何靠训练与推理堆出来

导语

让大模型“会做数学题”并不等于让它写出可得分的奥林匹克数学证明。后者要求模型不仅找到方向，还要组织严密、覆盖关键论证，并在长链条推理中避免一个小错误毁掉整份答案。围绕这一问题，论文《An Open Recipe for IMO Gold》研究了模型训练与测试时推理设计，试图给出一套可复现的开源路线。

核心要点

• 从通用模型训练数学专才。 研究以 Nemotron 3 Ultra 为基础，使用监督微调和强化学习训练两个专用检查点，重点提升自然语言形式的竞赛数学证明能力。
• 把验证放进推理循环。 系统不是一次生成答案，而是让多个 Nemotron 检查点参与候选证明的生成、检查与改写。验证结果会影响后续修订，形成迭代搜索。
• 测试时计算承担重要角色。 除了模型本身的训练，方案还安排了独立的高计算量阶段，用于比较和选择最终提交的证明。这说明复杂数学任务的性能，可能同时取决于参数能力与推理预算。
• 不依赖外部数学工具。 论文描述的流程完全在自然语言中运行，没有形式化证明器、外部工具或互联网访问，因此更接近通用语言模型可以直接部署的推理范式。
• 开放完整研究资产。 作者计划发布两个后训练检查点、训练数据、训练与推理代码、提交的解答，以及包含 200 道新奥赛级题目的 Nemotron-IMO-Bench。

结果与边界

论文报告称，这套系统在 IMO 2026 获得 42 分中的 30 分，达到金牌门槛。这个结果的重点不只是分数本身，更在于它把“模型后训练”和“测试时搜索”放进同一个实验框架中进行考察：研究者可以比较不同检查点在生成、验证和修订环节的作用，也能进一步研究增加推理计算是否带来稳定收益。

但这并不意味着模型已经像人类竞赛选手一样可靠。自然语言验证仍可能遗漏隐蔽错误，迭代系统也需要较高的计算预算；而论文摘要提供的是整体成绩，尚不足以据此判断每道题的证明质量、各个组件的独立贡献，或方法在新题分布上的泛化程度。Nemotron-IMO-Bench 的开放，或许能为这些问题提供更系统的检验。

意义与影响

这项工作展示了一种相对务实的数学推理工程思路：不把全部希望寄托在单次生成或单个“数学模型”上，而是组合专用训练、多模型协作、自然语言自检和高预算选择。若相关代码与数据能够复现，研究社区将更容易拆分其中的收益来源，并探索其在定理证明、科学推理和教育评测中的适用范围。

来源：Hugging Face Daily Papers