Maxproof

# MaxProof：利用生成式验证器强化学习与群体级测试时扩展扩展数学证明  
来源：https://arxiv.org/html/2606.13473  
\\reportnumber  
Xinyu Zhang（复旦大学）、Shunkai Zhang（北京大学）、Yanmohan Wang（MiniMax、清华大学）、Lin Li（MiniMax）、Tiancheng Qin（MiniMax）、Qin Wang（MiniMax）、Zhengmao Zhu（MiniMax）、Tianle Li（MiniMax）、Jingyang Li（MiniMax）、Zehan Li（MiniMax）、Binyang Jiang（MiniMax）、Jin Zhu（MiniMax）、Han Ding（MiniMax）、Fei Yu（MiniMax）、Chenyu Du（MiniMax）、Zijian Song（MiniMax）、Jiayuan Song（MiniMax）、Zhi Zhang（MiniMax）、Yunan Huang（MiniMax）、Weiyu Cheng（MiniMax）、Pengyu Zhao（MiniMax）、Yu Cheng（香港中文大学）  

###### 摘要  
我们提出MaxProof，一种针对竞赛级数学证明的群体级测试时扩展框架，应用于MiniMax-M3系列。M3首先通过低误报率的深度防御生成式验证器，训练三种面向证明的能力——证明生成、证明验证和基于批判的证明修复——这些能力被合并到单一发布的M3模型中。在测试时，MaxProof将模型视为生成器、验证器、优化器和排序器，在候选证明群体中进行搜索，并通过锦标赛选择返回最终证明。借助MaxProof测试时扩展，M3模型在IMO 2025上达到35/42，在USAMO 2026上达到36/42，均超过人类金牌阈值。  

请参照图1：MaxProof流程。M3首先通过验证器引导的证明强化学习训练证明生成能力，通过校准的错误发现训练证明验证能力，通过精炼增强训练基于批判的证明修复能力。这些能力被合并到M3发布模型中，MaxProof在测试时通过群体搜索和锦标赛选择进行扩展。  

###### 目录  
1. 1.引言 (https://arxiv.org/html/2606.13473#S1)  
2. 2.证明专家：深度防御验证器下的长程强化学习 (https://arxiv.org/html/2606.13473#S2)  
   1. 2.1训练流程概述 (https://arxiv.org/html/2606.13473#S2.SS1)  
   2. 2.2深度防御验证器 (https://arxiv.org/html/2606.13473#S2.SS2)  
   3. 2.3强化学习算法：带标准差阈值过滤的CISPO (https://arxiv.org/html/2606.13473#S2.SS3)  
   4. 2.4数据：领域与技巧平衡 (https://arxiv.org/html/2606.13473#S2.SS4)  
   5. 2.5M2循环：奖励作弊案例研究 (https://arxiv.org/html/2606.13473#S2.SS5)  
3. 3.验证器专家：校准的错误发现 (https://arxiv.org/html/2606.13473#S3)  
   1. 3.1任务形式化：错误发现优于分数预测 (https://arxiv.org/html/2606.13473#S3.SS1)  
   2. 3.2训练数据：复用证明专家的验证器 (https://arxiv.org/html/2606.13473#S3.SS2)  
   3. 3.3奖励设计 (https://arxiv.org/html/2606.13473#S3.SS3)  
   4. 3.4验证器专家为何重要 (https://arxiv.org/html/2606.13473#S3.SS4)  
4. 4.修复专家：通过拒绝采样微调进行证明修复 (https://arxiv.org/html/2606.13473#S4)  
   1. 4.1任务形式化 (https://arxiv.org/html/2606.13473#S4.SS1)  
   2. 4.2训练数据：证明强化学习的免费副产品 (https://arxiv.org/html/2606.13473#S4.SS2)  
   3. 4.3训练方法：拒绝采样微调 (https://arxiv.org/html/2606.13473#S4.SS3)  
   4. 4.4修复专家为何重要 (https://arxiv.org/html/2606.13473#S4.SS4)  
5. 5.MaxProof：群体级测试时扩展 (https://arxiv.org/html/2606.13473#S5)  
   1. 5.1问题设定：从best@K到pass@1 (https://arxiv.org/html/2606.13473#S5.SS1)  
   2. 5.2MaxProof循环 (https://arxiv.org/html/2606.13473#S5.SS2)  
   3. 5.3设计选择 (https://arxiv.org/html/2606.13473#S5.SS3)  
      1. 5.3.1保守适应度 (https://arxiv.org/html/2606.13473#S5.SS3.SSS1)  
      2. 5.3.2多样化父代选择 (https://arxiv.org/html/2606.13473#S5.SS3.SSS2)  
      3. 5.3.3PATCH与REWRITE精炼 (https://arxiv.org/html/2606.13473#S5.SS3.SSS3)  
      4. 5.3.4群体级早停 (https://arxiv.org/html/2606.13473#S5.SS3.SSS4)  
      5. 5.3.5最终选择 (https://arxiv.org/html/2606.13473#S5.SS3.SSS5)  
6. 6.实验：数学证明基准与MaxProof扩展 (https://arxiv.org/html/2606.13473#S6)  
   1. 6.1设置 (https://arxiv.org/html/2606.13473#S6.SS1)  
   2. 6.2独立基准结果 (https://arxiv.org/html/2606.13473#S6.SS2)  
   3. 6.3竞赛问题上的MaxProof (https://arxiv.org/html/2606.13473#S6.SS3)  
      1. 6.3.1逐问题分析 (https://arxiv.org/html/2606.13473#S6.SS3.SSS1)  
      2. 6.3.2讨论 (https://arxiv.org/html/2606.13473#S6.SS3.SSS2)  
7. 7.结论 (https://arxiv.org/html/2606.13473#S7)  
8. 参考文献 (https://arxiv.org/html/2606.13473#bib)  
9. A.逐问题结果与搜索动态 (https://arxiv.org/html/2606.13473#A1)  
   1. A.1每轮Oracle最优轨迹 (https://arxiv.org/html/2606.13473#A1.SS1)  
   2. A.2逐问题注释 (https://arxiv.org/html/2606.13473#A1.SS2)  
10. B.提示模板 (https://arxiv.org/html/2606.13473#A2)  
    1. B.1验证器提示 (https://arxiv.org/html/2606.13473#A2.SS1)  
    2. B.2精炼（PATCH）提示 (https://arxiv.org/html/2606.13473#A2.SS2)  
    3. B.3精炼（REWRITE）提示 (https://arxiv.org/html/2606.13473#A2.SS3)  
11. C.奖励作弊案例研究 (https://arxiv.org/html/2606.13473#A3)  
    1. C.1长度偏差 (https://arxiv.org/html/2606.13473#A3.SS1)  
    2. C.2格式作弊 (https://arxiv.org/html/2606.13473#A3.SS2)  
    3. C.3语义捷径 (https://arxiv.org/html/2606.13473#A3.SS3)  
    4. C.4评判者特定偏好 (https://arxiv.org/html/2606.13473#A3.SS4)  
    5. C.5从案例到防御 (https://arxiv.org/html/2606.13473#A3.SS5)  
12. D.选定模型输出 (https://arxiv.org/html/2606.13473#A4)  

## 1. 引言  
数学证明是对语言模型可靠推理的高压力压力测试。与开放式生成不同，证明必须满足一个长且紧密耦合的约束链，对那种在对话中经常不被注意的含糊其辞容忍度极低。这使得证明成为在IMO-AnswerBench和IMO-ProofBench[imobench-google]等基准中研究的通用数学推理挑战的一个更尖锐版本。随着基础模型的增长，一系列系统不断推动竞赛级证明的前沿：AlphaGeometry展示了神经符号系统可以在无需人类演示的情况下解决奥林匹克几何问题[trinh2024alphageometry]；AlphaProof[alphaproof2024]将语言模型与AlphaZero风格搜索[silver2018alphazero]相结合，在IMO 2024上获得了银牌级性能；Gemini Deep Thinking和OpenAI的前沿模型在IMO 2025上达到了金牌级性能[googledeepmind2025gemini]；DeepSeek-Math-V2成为同一竞赛中首个开放权重的金牌级模型[shao2025deepseekmathv2]；较小的开放模型如SU-01和NVIDIA Nemotron Cascade2展示了竞赛级证明可以在次前沿规模下专门化[li2026achieving,cascade2]；GPT-5.5最近解决了长期存在的开放问题，这些问题多年来一直困扰着人类数学家[gpt55open]。  

本文是来自M3一侧关于同一前沿的报告。M3发布是一个通用模型，但竞赛级证明所施加的要求比大多数其他任务更严格。将M3推过IMO 2025和USAMO 2026的金牌线，迫使我们面对三个独立的设计问题，我们将其视为一系列原子能力：  

1. 证明生成。给定一个竞赛问题，模型能否生成一个至少有时接近正确证明的候选证明？这是经典的*一次性 best@K* 问题。更广泛的推理模型文献表明，自我改进、数学专门化后训练和大规模强化学习可以显著改变模型的推理行为[zelikman2022star,shao2024deepseekmath,yang2024qwen25math,r1,kimi2025k15]。M2系列已经表明，使用来自执行或单元测试反馈的奖励进行长程强化学习可以显著提升基础模型；对于证明，等效信号必须来自生成式验证器，这引入了更困难的问题类别，围绕奖励噪声、误报和奖励作弊。  
2. 证明验证。模型能否可靠地指出给定证明*在哪里*出错，并解释*为什么*？这是第二种原子能力：*批判*证明的能力。它支撑着自我检查、错误纠正以及我们在第二部分中描述的群体级搜索，并且与数学推理中的验证器和过程监督工作密切相关[cobbe2021gsm8k,lightman2023verify]。重要的是，这是一个与“分配0-7分数”不同的目标——它需要定位和描述错误，而不是对它们排序。  
3. 证明精炼。给定一个有缺陷的证明以及一个批判，模型能否生成一个修正版本？这是第三种原子能力：*修复*证明的能力。它在结构上不同于一次性生成——模型必须阅读现有论证，保留其正确部分，并修补目标缺陷。这更接近修复而非生成，并与语言模型中迭代自我反馈和修订的最新工作相关[madaan2023selfrefine,shinn2023reflexion]。  

在M3发布流程中，我们通过一个专门化训练阶段的链条构建这三种能力：一个**证明专家**，在深度防御生成式验证器下通过长程强化学习训练；一个**验证器专家**，与同一验证器对齐，以显式的错误发现为主要目标；以及一个**修复专家**，学习修复由验证器标记的证明（第2节 (https://arxiv.org/html/2606.13473#S2)–4 (https://arxiv.org/html/2606.13473#S4)）。这些能力随后被合并到最终的M3模型中，这是交付给用户的单一模型。  

论文的第二部分介绍了**MaxProof**（第5节 (https://arxiv.org/html/2606.13473#S5)），作为一个模型无关的群体级测试时扩展框架。MaxProof仅假设生成器、验证器、精炼器和排序器接口；这些接口可以由不同模型提供，但在M3发布中，它们都由同一合并模型在不同提示下提供。该框架通过搜索候选证明群体将best@K转化为更稳定的pass@1，将验证器噪声在许多候选中摊销，并通过成对锦标赛自我选择确定最终答案，这建立在近期关于自一致性、树结构深思、验证与精炼管线以及扩展推理时计算的工作之上[wang2023selfconsistency,yao2023tree,snell2024scaling,brown2024large,wu2024empirical,huang2025winning]。  

**贡献**。具体来说，本报告做出以下贡献。  
- • 我们描述了一个四层生成式验证器管道（坏例过滤、解法归一化、多评判者并行评分和悲观最小值聚合）及其工程原理：RL时验证器的核心设计目标不是在静态基准上达到最大准确度，而是在长时间训练流上达到最小误报率。  
- • 我们分享了M2循环中的惨痛教训：使用单评判者标准验证器的长程RL运行很可能以奖励作弊平台期告终，而非实际能力提升。我们记录了观察到的四种典型作弊模式（长度偏差、格式作弊、语义捷径、评判者特定偏好），并解释了M3验证器设计如何通过使每一种都更难利用来塑造。  
- • 我们提出MaxProof作为一个群体级测试时扩展框架，采用进化启发的搜索循环，并详细介绍了使其在实践中可行的设计选择：保守的基于验证器的适应度、多样化父代选择、双PATCH/REWRITE精炼以平衡利用与探索、成对锦标赛最终选择，以及群体级早停以减少残余验证器误报。  
- • 我们报告了独立基准性能和测试时扩展结果。在IMOProofBench和IMOAnswerBench上，M3缩小了与前沿闭源模型的差距。借助MaxProof，同一M3模型在IMO 2025上达到35/42，在USAMO 2026上达到36/42。我们还分享了群体中逐问题的搜索动态，我们认为这比最终自我选择本身更具诊断信息。  

**结构**。本文其余部分组织如下。第一部分涵盖基础模型原子能力：第2节 (https://arxiv.org/html/2606.13473#S2) 描述证明专家，包括验证器管道、RL训练方法和M2循环的奖励作弊案例研究；第3节 (https://arxiv.org/html/2606.13473#S3) 描述验证器专家；第4节 (https://arxiv.org/html/2606.13473#S4) 描述修复专家。第二部分涵盖测试时扩展：第5节 (https://arxiv.org/html/2606.13473#S5) 介绍MaxProof框架。第三部分涵盖评估：第6节 (https://arxiv.org/html/2606.13473#S6) 报告独立基准性能以及在IMO 2025和USAMO 2026上MaxProof的额外增益，第7节 (https://arxiv.org/html/2606.13473#S7) 总结。逐问题分解和提示模板见附录。  

## 2. 证明专家：深度防御验证器下的长程强化学习  
我们需要的第一个原子能力是*生成*一个至少偶尔接近正确的证明的能力。对于一个已经展现出竞赛级best@K行为的模型，锐化该能力的自然途径是使用一个为候选证明打分的奖励信号进行长程RL，这遵循了推理模型的RL和可验证奖励RL研究的一般路线[lambert2024tulu,r1,kimi2025k15,su2025crossing,wen2025reinforcement,kimiteam2026kimik2openagentic,glm5team2026glm5vibecodingagentic]。然而，对于证明，没有可执行的ground truth可以调用——奖励必须来自生成式验证器，这引入了比基于结果（如代码或单元测试任务）的RL更困难的问题类别。本节描述我们如何构建证明专家、支撑它的验证器管道，以及塑造最终设计的早期迭代失败模式。  

请参照图2：证明专家的训练动态。  

### 2.1. 训练流程概述  
证明专家围绕一个核心对象进行训练：一个冻结的生成式验证器，将候选证明转化为RL奖励。对于每个竞赛问题，rollout策略采样一组长格式候选证明。每个证明随后传递给验证器，该验证器不仅检查最终答案；它阅读论证，与基于参考解法的标准进行对比，识别缺失或无效的步骤，并返回文本评估和\[0,7\]范围内的标量分数。我们使用该标量分数作为整个证明的轨迹级奖励，并通过GRPO[shao2024deepseekmath]的变体更新策略，该变体适应M系列的CISPO目标[minimax2025m1,minimax2025m2]。这一选择正是使证明RL不同于代码、工具使用或短答案数学RL的原因。在代码任务中，奖励通常可以基于执行：程序要么通过单元测试，要么不通过[chen2021humaneval,jimenez2024swebench]。在证明任务中，正确性对象是自然语言数学论证，因此奖励模型本身必须对证明进行推理[lightman2023verify,shao2025deepseekmathv2]。因此，验证器不是训练后调用的辅助评估器；它是策略从中接收学习信号的环境。如果验证器奖励一个有缺陷但具说服力的论证，RL将放大该缺陷；这是AI安全性和奖励建模工作中研究的相同基本奖励博弈风险[amodei2016concrete,skalse2022defining]。如果验证器