IMO金牌的开放配方：为奥数证明训练Nemotron An Open Recipe for IMO Gold: Training Nemotron for Olympiad Mathematics
开源Nemotron流水线纯自然语言证明获IMO 2026金牌（30/42分）
前置知识
MoE 混合专家架构
混合专家把模型参数拆成多个专家子网络，每个 token 只激活其中一小部分，从而在大容量下控制单次前向算力。本文底座 Nemotron 3 Ultra 记作 550B-A55B：总参数 5500 亿、每 token 激活 550 亿，训练时靠张量并行、上下文并行、专家并行等组合切分，SFT 序列长度高达 425,984 token。
论文所有检查点（GA/SFT/RL）都是这个 MoE 底座的后训练变体，流水线的生成、验证、精炼全部由它们驱动，理解容量与并行配置是看懂实验成本和可复现性的前提。
SFT 监督微调
用（提示, 回答）对直接对模型做逐 token 交叉熵损失 $\mathcal{L} = -\sum_i \log p(y_i|x_i)$ 训练，让模型模仿高质量示范。本文用 DeepSeek-V4-Pro 合成证明、精炼、验证、元验证四类轨迹，过滤后得到 414,890 条样本、覆盖 15,818 道难题。
SFT 检查点是首轮表现最好的单模型（70 分）也是验证面板中最挑剔的验证者（假接受率仅 4.5%），理解其数据构成才能明白它为何'宁缺毋滥'。
RLVR 可验证奖励强化学习
不再模仿参考答案，而是给模型自己生成的解打分作为奖励做策略优化。本文沿用 DeepSeekMath-V2 的奖励设计但令 $\alpha=1,\ \beta=0$ 去掉自我分析奖励，基于 NeMo-RL 的异步框架（类 PipelineRL）配合动态采样、截断重要性采样和熵控制（熵超 0.4 时屏蔽正样本低概率 token）。
RL 检查点是开发集上总分最高的单检查点（180 分）和主要生成者，奖励设计决定了它学到什么样的证明风格与自评倾向。
测试时计算
在推理阶段投入大量算力换性能：并行采样多条候选、逐条验证打分、基于反馈迭代精炼、最后在候选中择优提交。性能不再取决于模型一次前向，而取决于搜索的广度（候选数）、深度（轮数）和挑选精度（终选评审）。本文每题最多 8 轮、首轮即 384 条候选、终选每篇入围证明 48 票评审。
整篇论文的主旨就是系统消融测试时计算的哪些设计——检查点选择、验证规则、精炼策略——真正把开源系统推上金牌线。
假接受率与假拒绝率
验证器把错误证明判为正确的比例是假接受率（false accept），把正确证明判为错误的比例是假拒绝率（false reject）。二者代价不对称：假接受让搜索带着错解提前终止、不再产生新候选；假拒绝只是延迟，候选仍留在池中等待精炼或作为兜底提交。规则 $k/n$ 表示 n 票中至少 k 票满分才接受。
论文的关键设计——RL+SFT 两验证器 16/16 全票一致——就是为了把假接受率从 GA 单检查点的 31.6% 压到 1.1%，看懂 Table 3 必须先掌握这两个指标。
研究动机
IMO 长期被视为 AI 数学推理的试金石。2024 年 AlphaProof 与 AlphaGeometry 2 依靠神经-符号方法加 Lean 形式验证拿到银牌（距金牌线 1 分），但这类系统严重依赖可靠的符号验证器来生成训练语料、在高分支空间中搜索；2025 年 Gemini Deep Think 和 OpenAI 实验模型证明纯自然语言端到端系统也能拿到金牌，但两者都是闭源系统，外界既无法复现，也说不清成绩究竟来自后训练还是推理时设计。开源侧虽有 DeepSeekMath-V2 的生成器-验证器-元验证器联合训练和 Aletheia 的生成-验证-修订多智能体迭代等进展，但要么止步于基准评测、要么依托闭源前沿模型。于是核心问题悬而未决：一个完全开源、不用形式验证器、不用外部工具的系统，到底要做哪些后训练与测试时设计才能达到 IMO 金牌水平？检查点选择、验证规则、精炼、终选各组件的边际贡献又各是多少？
本文的目标是本文的目标是打造一套端到端开源的 IMO 金牌系统，并把它当作研究平台系统性地回答上述问题。具体包括三件事：其一，从 Nemotron 3 Ultra（550B-A55B）通用检查点（GA）出发，分别用监督微调 SFT 和强化学习 RL 训练两个面向证明生成的专家检查点；其二，构建无形式验证器、无外部工具、无网络的纯自然语言生成-验证-精炼流水线，接收竞赛方官方 LaTeX 题面，在 IMO 2026 正式参赛并越过金牌线（29 分）；其三，把系统尽可能完整开源——两个后训练检查点、SFT 与 RL 训练数据、训练和推理代码、向竞赛提交的全部证明、按题细分的 token 与 GPU 时账本，以及与奥数教育者 Titu Andreescu 合作新造的 200 道奥数级新题基准 Nemotron-IMO-Bench 和 30 题开发集，为后续系统级权衡研究提供可复现参考。
与已有工作不同的是，本文的独特切入有三点。第一，完全自然语言路线：不用 Lean 等形式证明器，验证全靠模型面板按 0/0.5/1 打分，并用 16 票全票一致的接受规则压制假接受——在 IMO 级别上这是少见的开源选择，作者刻意把它与'接受即正确'区分开。第二，把'检查点互补性'作为一等设计原则而非工程细节：实验证明同样的 token 花在第二个检查点上远比加倍单检查点采样有效（RL 128+SFT 128 首轮接受 18 题对 RL 256 的 14 题）。第三，诚实透明的误差审计：官方 30 分与模型评审约 32 分的 2 分差距被明确归因于 P3、P6 上模型验证器的共同盲区，并用 300 份证明的审计集量化假接受/假拒绝的不对称代价，而不是只报告好看的数字，这种负结果分析在竞赛报告里非常罕见。
核心方法
直觉上，这是让多个'性格不同'的模型对同一道难题并行攻坚：先大量尝试，再由最挑剔的两个模型交叉把关，全票满分才放行；通不过就带着批评意见回去修改，最多八轮；最后用更大的评审算力从入围者中挑一篇提交。技术路线上，底座是 Nemotron 3 Ultra 550B-A55B 的三个检查点——通用 GA、SFT 专家、RL 专家，分别承担生成（提出候选证明）、验证（0/0.5/1 打分加自然语言批评）、精炼（按批评修订）三种角色。搜索阶段每题独立运行：第一轮 3 个检查点 × 8 个互补策略提示 × 每提示 16 条 = 384 条候选证明；验证由 RL+SFT 各出 8 票共 16 票，必须全部打 1 分才接受；未通过则从全局证明池取前 16 名、各配最多 8 条批评构造精炼提示，发给 3 个检查点各采样 4 条，共 192 条/轮，验证后回池。某检查点一旦有证明被接受即停采（检查点级早停），搜索最多 8 轮。终选阶段每个入围者由 3 个检查点各 16 票 IMO 式 0-7 打分共 48 票，按均值排名、同分取更短者提交。
核心是'互补检查点 + 全票验证 + 批评驱动精炼'的组合，背后是两个不对称性洞察。其一，验证错误的代价不对称：假接受会让一道题带着错误证明永久退出搜索，后续阶段不再生成新候选；假拒绝只是延迟——高分候选仍留在池里被继续精炼或作为兜底提交。因此验证器必须极端保守：选最挑剔的 RL 与 SFT 各 8 票、要求 16/16 全票满分，宁可慢不可错。其二，生成算力应花在多样性而非重复上：不同检查点能解不同的题（RL 128+SFT 128 接受的 18 题中 6 题两者都解、7 题仅 RL、5 题仅 SFT），8 个互补策略提示（引理优先分解、路径比较、反例搜索等）用于给第一轮生成去相关。其三，把'搜索时验证'与'终选评分'拆成目标不同的提示：前者输出可执行的批评以指导下一轮精炼，后者按 IMO 0-7 评分标准做里程碑分析并参考 Dekoninck 等的评审方法论。整体与 DeepSeekMath-V2 的生成-验证-精炼思路同源，但落成全开源、纯自然语言、多检查点集成的真实竞赛系统，并附组件级量化证据。
方法步骤详情
第一步 SFT：从 Nemotron-Math-Proofs-v1 的 AoPS 子集选 15,879 道难题，用 DeepSeek-V4-Pro Max 模式生成证明尝试（上限 400K token），未解出的经最多三轮带验证反馈的精炼；并行构造验证（0/0.5/1 打分）与元验证轨迹，过滤后得 414,890 条样本——58,543 证明生成、67,971 精炼、236,360 验证、52,016 元验证；在 512 块 GB200 上以 425,984 token 序列长训练，学习率 $1.5\times10^{-5}$ 余弦退火至 $2\times10^{-6}$，按 133 道证明题评测选定第 1300 步检查点。第二步 RL：筛出基座四次尝试中恰好解出 1-3 次的 9,597 题，奖励沿用 DeepSeekMath-V2 但令 $\alpha=1,\ \beta=0$ 去掉自评奖励；基于 NeMo-RL 异步框架，全局批 128 提示×16 轨迹=2,048 条，截断重要性采样，熵超 0.4 时屏蔽正样本低概率 token，共 272 节点×4 块 GB200。第三步竞赛流水线：执行 8 轮生成-验证-精炼搜索与 48 票终选并正式提交。
技术新颖性
新颖性不在单点算法，而在于把已知组件——DeepSeekMath-V2 的奖励与验证-精炼范式、PipelineRL 式异步 RL、MathArena 的评审团调解流程——组装成在真实 IMO 上拿金牌且全开源的系统，并给出组件级量化证据。验证面板审计（Table 3，300 份证明）显示：GA 单独 8/8 规则假接受 31.6%，SFT 降到 4.5%，RL+SFT 全票 16/16 压到 1.1% 而假拒绝升至 81.3%——'宁慢勿错'设计的直接量化；放宽到 14/16 假接受即飙到 17.0%，说明没有免费的宽松午餐；再加 GA 成 24/24 也无改善，因为宽松验证者很少否决 RL 与 SFT 都接受的证明。Table 4 分解首轮算力：RL 256 对 RL 128 只多接受 1 题，而 RL 128+SFT 128 在相近 token 下接受 18 题，证明互补性优于重复采样。配套的 Nemotron-IMO-Bench（200 道新题，CC BY 4.0）与完整算力账本也体现少见的透明度。
实验结果
竞赛结果：IMO 2026 官方评分 30/42，超金牌线 29；P1/P2/P4/P5 满分各 7 分，P3/P6 各 1 分。四篇满分证明在开赛后 76 分钟内通过终选，另两篇在 100 分钟内完成；拿到全部提交证明耗费约 707M token、1,464 GB200 GPU 时，全程约 2.31B token、4,800 GPU 时。截稿后继续搜索在第 8 轮为 P6 产出更优解，人类盲评 4/7，计入则 33 分（非官方）。开发集端到端（Table 2 末行）：GA 162 分（23 题接受）、RL 180（23）、SFT 165（21），集成 188 分（25 题），且三轮内即达最终接受分。验证审计（Table 3，300 份证明）：GA 8/8 假接受 31.6%/假拒绝 22.8%，RL 12.4%/64.2%，SFT 4.5%/69.1%；提交的 RL+SFT 16/16 面板 1.1%/81.3%。25 份被接受证明中 23 份获评审团 7 分、1 份 6 分（量词形式）、1 份 0 分（列置换对称性被反例驳倒），三个检查点对后两份都打满 8 票，无投票规则能拦截。P3/P6 上模型评分约 32 分，高于官方 2 分，暴露共同盲区。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| IMO 2026 正式竞赛（6 道证明题） | 官方 42 分制总分 | 30/42（P1/P2/P4/P5 满分，P3/P6 各 1 分），全部由官方 IMO 评分员评定 | 金牌线 29 分；2025 年 Gemini Deep Think 与 OpenAI 实验模型达金但闭源 | 首个达到金牌线的开源纯自然语言系统（无形式验证器/工具/网络） |
| 30 题开发集端到端流水线（8 轮搜索+兜底） | 独立评审团累计得分（括号内为内部接受题数） | 三检查点集成 188 分（25 题） | 最强单检查点 Nemotron-3-Ultra-RL 180 分（23 题）；GA 162（23）；SFT 165（21） | 比最强单检查点多 8 分、多接受 2 题 |
| 证明验证（300 份审计集：25 份接受+275 份分层未接受） | 假接受率（评审团判错仍被接受的比例，95% bootstrap 置信区间） | 1.1% [0.0, 2.7]（RL+SFT 16/16 全票规则） | GA 单检查点 8/8 规则 31.6% [17.9, 45.4] | 假接受率降低约 30 个百分点，代价是假拒绝率从 22.8% 升至 81.3% |
| 首轮候选池算力分配 | 内部接受题数与评审团分数（约 2.4B 生成 token） | RL 128 + SFT 128：接受 18 题，accepted-only 116 分 | RL 256（同 token 加倍单检查点）：接受 14 题，accepted-only 92 分 | 多接受 4 题、多 24 分，证明互补性优于重复采样 |
局限与改进
作者承认的局限：模型验证器存在系统性偏差——P3/P6 上内部验证器与外部模型评审团都给出约 32 分而官方仅 30 分，且继续运行中 P6 的新解被内部验证拒绝、人类盲评却给 4/7，说明验证器对某类错误（如构造/组合论证）判断不可靠；25 份被接受证明中 1 份实为完全错误（评审团 0 分），任何基于这 24 票的一致性规则都无法拦截，即假接受无法降为零。方法层面：16/16 全票导致 81.3% 的假拒绝率，正确证明也常被压住，只能靠'留在池中等精炼'兜底，消耗大量算力；竞赛全程 2.31B token、4,800 GB200 GPU 时，远超学界常规预算。我的观察：消融用 GPT-5.5/Gemini 3.1 Pro/Claude Opus 4.8 当独立评审团，评审本身也是 LLM 且无参考答案，'solved'与 jury 7 分的定义可能和官方评分存在同类偏差；集成与单检查点实验并非严格算力对齐（Table 4 只部分补齐这一缺口）；被拒的那份 0 分证明与 6 分证明的完整文本分析在正文中着墨有限，独立复核评审团结论较难。
独立分析的弱点
弱点一：验证盲区跨模型相关。RL、SFT、GA 三个检查点以及 GPT-5.5/Gemini/Claude 评审团都在 P3/P6 上高估证明，Table 3 也显示给面板加 GA 的 8 票只删掉 2 份正确证明，说明这些同源或同期大模型的错误模式高度相关，简单增加投票者无解。改进方向：引入异构验证器——对关键引理做形式化抽查、对小规模情形做数值/暴力验证、用符号引擎核对代数恒等式，即使只覆盖部分子问题也能打破相关性。弱点二：全票一致的假拒绝率高达 81.3%，正确候选大量被压，依赖池内兜底排名，算力效率低。改进：为每票校准置信度、用概率聚合替代硬性一致，或按题目难度自适应调整票数与轮数。弱点三：RL 阶段显式去掉自我分析奖励（$\alpha=1,\ \beta=0$），自评能力只在 SFT 数据中训练，RL 检查点的自评校准可能退化。改进：把自评与验证一致性纳入 RL 奖励。弱点四：对未解题的兜底提交（30 题中 5 题）得分很低却消耗同量算力，缺少'何时放弃转向'的显式策略，论文附录也承认激进 triage 会误删日后能解出正确证明的候选。
未来方向
作者明确提出的方向：以 Nemotron-IMO-Bench（200 道新题+30 题开发集）为公共平台研究系统级权衡；把公开的训练配方与推理管线作为可复现基线，延伸到研究级数学（Aletheia 已展示该方向）。基于本文成果可自然延伸的：其一，自然语言+形式化混合验证——用 Lean 抽查被 16 票接受证明的关键步骤，尤其是 P6 那类'内部拒绝但人类盲评 4/7'的解做定向复核，用形式工具打破模型评审的相关盲区；其二，把 8 轮固定预算搜索与 48 票终选改造成正式的序贯决策问题（何时提前停止、何时加采样、何时切换题目），当前均为启发式；其三，RL 奖励目前只有证明质量一项，可加入验证一致性、批评可执行性等多维奖励，或恢复被置零的自评奖励并做消融；其四，论文引用 Nemotron-Cascade 2 表明紧凑模型可逼近前沿开源模型，值得在压缩检查点上重跑此配方、绘制算力-性能曲线，让中等规模实验室也能复现；其五，评审协议可引入官方评分标准或人机对照校准，减小参考自由评审与真实评分之间的系统性偏移（本文 32 对 30 的差距即来自此类偏移）。
复现评估
开源程度非常高：两个后训练检查点 nvidia/Nemotron-3-Labs-Ultra-Math-SFT/-RL（OpenMDW-1.1），SFT 语料与 RL 题集 Nemotron-Math-Proofs-v3（CC BY 4.0），基准 nvidia/Nemotron-IMO-Bench（200 道新题），推理管线、开发集组装脚本与全部提交证明在 NeMo-Skills 的 recipes/nemotron-imo-tts，RL 配方在 NeMo-RL 的 imo-26-ultra-v3 分支文档，另有按题细分的算力账本。复现门槛主要在算力：SFT 用 512 块 GB200（425K 上下文），RL 用 272 节点×4 块 GB200，竞赛推理 4,800 GB200 GPU 时。小规模研究者仍有务实路径：直接下载检查点跑单检查点 8 轮搜索（Table 2 表明单检查点可得 162-180 分），或在 Nemotron-IMO-Bench 子集上复现验证审计（Table 3）——全票验证假接受 1.1%、检查点互补性等核心结论在数十卡量级应可部分验证。
论文图表
