IMO 金牌的开放配方：为奥林匹克数学训练 Nemotron

TL;DR 基于 Nemotron 3 Ultra 后训练两个专用 checkpoints，以纯自然语言迭代生成、验证与精炼证明，IMO 2026 获得 30/42 达金牌线，并全面开源模型、数据与代码。

问题

问题背景

国际数学奥林匹克（IMO）证明题目前是衡量 AI 数学推理能力的标杆。业界关注如何让模型直接生成自然语言证明，而非依赖形式化验证器，以更接近人类解题方式并达到金牌水平。

现有方法局限

• 形式化方法（如 Lean）需要将自然语言问题翻译为形式语言，翻译过程可能丢失信息，且形式化搜索空间巨大，工具链维护成本高。
• 单模型直接生成 在长证明中容易出现逻辑跳跃或错误，缺乏自我校验机制；传统 Best-of-N 或树搜索主要针对短答案或选择题，难以直接扩展到长文本证明的连贯性约束。
• 验证器训练 面临证明正确性评估的主观性与复杂性，难以获得高质量监督信号。

为什么这个问题难/重要

IMO 题目要求深度洞察、多步推理和严格论证，自然语言证明没有可执行检查，验证本身就需要强数学能力。设计高效的 test-time compute 流水线（生成-验证-精炼）涉及计算预算分配、错误累积控制、最终答案选择等开放问题。该领域吸引大量关注，因为攻克它能推动通用 AI 推理系统的进步，并作为模型能力的基准。

行业类比

类似自动驾驶中的闭环验证：单一感知模型不够，需要规划、预测与验证模块协同迭代；而数学证明的验证更难，因为不存在物理世界的可执行反馈。

核心洞察

• 纯自然语言证明生成达到 IMO 金牌阈值，证明不依赖形式化验证器的路线在竞赛数学中可行。与 AlphaProof 等神经符号系统相比，该系统直接在自然语言上生成、验证和精炼证明，验证器同样是自然语言模型，省去了翻译到 Lean 等形式语言的步骤，更贴近人类解题风格，同时避免了形式化转换中的信息损耗。这种路径对开放模型推理时缩放提供了新证据：只要后训练与验证迭代设计合理，自然语言推理也能匹配甚至超越形式化方法的性能。
• 通过 SFT 与 RL 训练两个专家 checkpoint，并与通用模型组成三模型集成，再叠加迭代“生成-验证-精炼”循环和高计算阶段选择，揭示了数学证明生成中多 checkpoint 协作的关键作用。与单模型基线或单纯增加采样次数相比，验证和精炼的分离以及多个专业模型的互补显著提升了最终得分。该设计不依赖外部工具或网络访问，全部在模型内部完成，为复杂推理任务的 test-time compute 分配提供了可迁移的工程范式：验证器应与生成器分别训练，且最终提交需要独立的高计算筛选阶段。

方法

输入与关键模块

• 输入：自然语言描述的 IMO 级别数学问题，无形式化符号或工具辅助。
• 基础模型：Nemotron 3 Ultra 通用 checkpoint，作为生成、验证与细化的统一骨干。
• 后训练专家：在高质量证明数据上进行 监督微调 (SFT)，再通过 强化学习 (RL) 针对证明接受度优化，得到两个专家 checkpoint。三者共同驱动测试时迭代搜索。
• 迭代搜索：循环执行生成候选证明（generation prompt）、验证（proof-verification prompt 与 meta-verification prompt，分别检查局部推理与全局元层面）、细化（refinement prompt，可结合跨证明上下文与多样化证明细化）。验证反馈引导后续探索。
• 高计算选择：独立高计算阶段使用 IMO-style judge prompt 与 jury reconciliation prompt 进行多模型评审，选择最终提交的证明。

输出：一份自然语言证明，直接提交至 IMO 评分标准。

差异点：与依赖形式化证明器、外部工具或符号验证器的 Neuro-symbolic 方法不同，本系统完全在自然语言空间内通过后训练与测试时验证-细化循环实现高可靠性证明生成，且全部组件开源。

实验

实验设计

从 Nemotron 3 Ultra 基础模型出发，通过 SFT 与 RL 训练两个专用 checkpoint。随后在 IMO 2026 真题与 Nemotron-IMO-Bench 上评估：单 checkpoint 流水线性能、验证器效果、完整集成流水线。最终系统采用三个 checkpoint（通用版 + 两个专用版）进行生成、验证、细化的迭代搜索，并设置独立高算力阶段选取最终答案。

关键发现

• 纯自然语言证明生成在无形式化证明器、无外部工具条件下，可达 30/42 分，触及 IMO 金牌线。
• 验证与细化循环对提升证明质量至关重要；多 checkpoint 集成优于单模型。
• 论文还公开了 Nemotron-IMO-Bench（200 道全新奥赛级题目），为后续研究提供可复现基准。

与基线对比解读

尽管摘要未给出具体基线分数，但从章节结构可见，作者对比了单 checkpoint、仅通用模型等配置。完整流水线的增益可能来自三方面：

1. 后训练专家模型增强了证明生成的多样性与准确性；
2. 验证模块过滤低质量候选；
3. 高算力选择阶段利用测试时计算进一步优化。

相较于同时期依赖形式化证明器或外部工具的方法，本工作证明了开放模型在纯自然语言路径上的可行性。

行业影响

落地场景

该自然语言证明生成管线可直接迁移至高等数学教育 与科研辅助 产品。具体 use case：

• 在线数学学习平台：针对竞赛数学 / 大学数学证明题，提供逐步生成、验证与修正的交互式讲解，替代纯静态答案。
• 企业级逻辑合规：在金融 / 法律等需严格推理的场景中，用同一套 generate-verify-refine 迭代机制自动生成合规论证并交叉验证，降低人工审核负担。

商业价值

核心价值来自推理质量提升带来的降本与体验增益。对教育产品，实时反馈可减少对人工助教的依赖；对科研 / 工程团队，Nemotron-IMO-Bench 与开源模型可替代部分昂贵的外部 API 调用，降低高难度推理任务的边际成本。IMO 金牌级表现为差异化卖点，可支撑订阅或按 token 计费的高溢价服务。

与现有 Stack 的接口

系统以纯自然语言运行，无形式化证明器依赖，因此可通过标准 LLM serving（如 vLLM / Triton） 接入现有 agent 工作流。三个 checkpoint（通用 + 两个后训练专家）可作为独立推理节点，verification 与 meta-verification 输出可对接人工审核或下游评分。训练代码与数据开源，便于企业基于私有领域数据做持续微调，并与现有 RAG / 工具调用框架兼容。

局限

• - **缺乏形式化验证**：系统完全依赖自然语言生成和模型自验证，没有接入 Lean 等形式化证明器，因此最终提交的证明可能包含不易察觉的逻辑漏洞。尽管迭代验证和细化降低了错误率，但模型验证器本身可能产生系统性偏差，无法提供机器可检查的正确性保证。在奥林匹克数学竞赛中，人工评分或许容忍部分模糊步骤，但在需要严格证明的研究场景或自动定理证明中，该局限会显著限制可信度与可用性。
• - **领域泛化有限**：训练与评估集中于奥林匹克数学问题，这类题目具有高度结构化的解题模式，且可能存在数据污染风险（尽管作者发布了新基准）。系统在高等数学、研究级证明或更广泛的推理任务上的表现尚不明确。此外，Nemotron-IMO-Bench 的 200 个新问题虽为原创，但其难度分布与风格是否与真实 IMO 完全一致仍需进一步验证，因此泛化到其他数学竞赛或实际数学研究的能力存在不确定性。
• - **计算资源需求高**：测试时计算管道涉及三个检查点的迭代搜索、验证与细化，以及单独的高计算选择阶段，需要大量 GPU 推理时间与显存。虽然作者开源了代码和模型权重，但完整管道的复现成本对多数研究团队而言仍然较高，可能限制该方法的普及与后续改进。此外，论文中未明确给出单次推理的算力消耗或成本分析，使得实际部署的可行性评估不够透明。