# MaxProof框架：MiniMax M3在IMO 2025和USAMO 2026超越人类金牌线
- 来源：MiniMax：Blog（网页）
- 作者：MiniMax
- 发布时间：2026-06-09 00:00
- AIHOT 分数：76
- AIHOT 标记：精选
- AIHOT 链接：https://aihot.virxact.com/items/cmqadpjwv0kjzslldk3axe95f
- 原文链接：https://www.minimax.io/blog/minimax-maxproof-math-proof-evolution
## 精选理由
M3在数学奥赛上搞定人类金牌，靠的是用生成验证器做RL和进化搜索，这套组合对复杂推理任务的普适性可能比提高一个benchmark分数更有价值。
## AI 摘要
MiniMax M3采用MaxProof框架，在IMO 2025和USAMO 2026两项数学奥赛基准上超越人类金牌线。框架分三阶段训练：Proof RL使用生成式验证器提供奖励，进行长程强化学习提升证明生成能力；Verifier Alignment将验证对齐为错误定位任务；Refinement Augmentation利用训练中产生的错误证明与验证分析对，通过拒绝采样微调修复能力。三者合并为M3通用模型。系统通过低假阳性率过滤噪声，保证RL稳定性。
## 正文
引言
在 M3 发布博文中，我们报告了 M3 模型在两个国际数学奥林匹克基准测试——IMO 2025 和 USAMO 2026——上的表现。借助 MaxProof 框架，M3 在这两项测试中均超越了人类金牌得主分数线。在本篇博文中，我们将深入探讨我们在数学证明领域取得进展背后的技术路径：改进基础模型、对齐验证器、构建精炼能力，以及设计测试时扩展框架 MaxProof。
从 Gemini Deep Thinking 在 IMO 2025 上达到金牌水平，到 DeepSeek-Math-V2 成为首个具备金牌水平能力的开源模型，再到 SU-01 和 NVIDIA Nemotron Cascade2 在小型模型中展现出专门的数学竞赛能力，以及 GPT 5.5 解决长期悬而未决的开放问题——模型正稳步进入数学问题空间中更困难的领域。在从 M2 到 M3 的迭代过程中，我们还致力于将更强的数学证明和自我改进能力整合到最终的通用模型中。
从方法论上看，开源社区已经为在单次生成（one-shot）场景下解决困难数学问题勾勒出一条相对清晰的路径：首先将模型的最佳@K（best@K）能力提升到足够高，然后利用测试时扩展将最佳@K 转化为更稳定的首次通过@1（pass@1）。我们的方法遵循同样的两个方向。第一部分是基础模型能力提升：我们训练了三个专家模型，以改进证明生成、错误判断和证明修复。第二部分是测试时扩展：我们设计了 MaxProof，这是一种进化搜索风格的测试时扩展（TTS）框架，让最终的 M3 融合模型能够通过多轮自我迭代来解决问题。本篇博文将重点介绍训练特性、系统设计权衡以及我们学到的实践经验。
改进基础模型
本节将解释我们如何在单模型侧构建数学证明和自我改进所需的若干原子能力。
整体布局
第一部分概述：三阶段基础模型增强方案
第一部分概述：在基座模型改进方面，我们采用三阶段训练方案，产出了三个专家模型。第一阶段，Proof RL（证明强化学习），产出 Proof Expert（证明专家）。我们通过 RL 后训练构建数学题奖励系统，对候选证明进行评分，并执行长周期强化学习。第二阶段第 1 部分，Verifier Alignment（验证器对齐），产出 Verifier Expert（验证专家）。我们利用 Proof RL 阶段积累的黄金验证分析数据，将验证器对齐定义为一个错误发现任务，并使用 RL 来对齐模型定位和判断错误的能力。第二阶段第 2 部分，Refinement Augmentation（改进增强），产出 Fixed Expert（修正专家）。我们复用 Proof RL 阶段自然产生的（历史缺陷证明，验证分析）数据对，通过拒绝采样对 Proof Expert 进行持续微调，使模型学会基于错误诊断来修复现有证明。所有三个专家模型最终都用于 M3 的合并训练。
Proof RL（证明强化学习）：对生成式重验证的实践探索
Proof RL 的目标是在 M3 上运行长周期 RL 训练，提升模型直接生成数学证明的能力。与传统的 RLVR 相比，我们最大的变化在于奖励主要由一个生成式验证器提供。这立即带来了一个挑战：训练过程必须系统地处理不准确的奖励信号、噪声、误报以及奖励作弊问题。
在相关工作中，DeepSeek-Math-V2 是首批公开示例之一，展示了在困难数学题训练中稳定使用生成式验证器的方法。其核心思路是自验证加元验证。我们没有完全遵循相同的路线，主要是因为 M 系列模型在之前的周期中尚未积累足够的验证能力。短期内，模型自身难以产生足够可靠的奖励信号。
因此，在本阶段，我们首先专注于提升证明能力，并使用外部前沿模型作为生成式验证器。该系统的关键设计包含三个部分：验证器设计、RL 算法变更以及训练数据准备。
验证器设计：低误报率是实现长周期稳定 RL 的关键
证明强化学习验证器的设计理念
证明强化学习验证器的设计理念，是将嘈杂且异质的信号投射到一个可控、可信的子空间中。这是实现可靠推理的基础。原始的候选空间包含多种多样的解题尝试、噪声样本以及潜在的失败模式，从极其冗长的推理链到偏离所需格式的输出，不一而足。每一种情况都可能干扰学习过程。验证器的任务是以算法方式严格过滤并结构化这些混乱信号，进而生成稳定的奖励信号。首先，它执行异常值过滤：对于匹配已知失败模式或明显违反规则的候选输出，直接赋予零分。从数学上看，这是对信号空间施加的一个硬约束，可防止误导性的强化学习更新。其次，它执行解答归一化：将来自多种来源和风格的证明映射到一个统一的验证器信任区域内，从而减少评判偏差，使奖励能够反映推理质量而非呈现形式的差异。这类似于对高维候选空间施加投影操作，将复杂的异质信号压缩到一个可信的子流形上。最后，它采用悲观评判：对于来自多个验证器的评分，取下限而非上限，以保守的方式生成最终奖励。这提高了鲁棒性，并有助于强化学习在噪声和不确定性下保持稳定。
任务定义
我们将任务的通用形式定义如下：
def score(problem_metadata, candidate_solution): candidate_solution = strip_thinking(candidate_solution) verifier_prompt = construct_prompt( problem_metadata, candidate_solution, ) score = verifier(verifier_prompt) assert score in [0, 1] return score
评分过程返回一个位于区间 [0, 1] 内的连续分数。验证器根据问题元数据评估候选解答的完整性和数学严谨性。在我们的设置中，验证器模型主要使用最新的前沿模型。
具体设计
经过多轮训练和调优，我们发现，在静态评估上获得一个“看起来足够准确”的验证器是远远不够的。生成式验证器天生不稳定，而这种不稳定性会在强化学习过程中被策略持续放大，最终导致训练崩溃。我们在 M2 周期中已经观察到了类似的问题，因此在 M3 周期中，我们采取了更为保守的原则：
**当生成式验证器被用作强化学习的奖励时，长期稳定训练的首要任务不是提高平均准确率，而是尽可能抑制误报。即使这会增加漏报，策略可以优化的空间也应保持足够狭窄。**
基于这一原则，我们将奖励系统设计为分层防御结构。
- 坏例防御：我们使用多层代码级规则来拦截明显异常的模型输出，例如未聚合的思考过程或过长的解答。一旦匹配到坏例，我们会跳过后续的验证器调用，直接赋予零分，从而防止低质量输出意外获得奖励。
- 模式偏移防御：M2 周期的经验表明，奖励作弊往往并不意味着问题解决能力突然提升。相反，输出风格可能已经偏移到验证器偏好的格式。为了减少验证器对特定表达模式的偏好，我们在将候选解答送入生成式验证器之前对其进行归一化处理，尽可能使候选解答保持在相同的评估分布内。
- 多维度悲观聚合：我们同时使用多个验证器模型和多种验证器模式。双模型设置降低了训练向单一评判者偏移的风险。双模式设置包括带评分细则和不带评分细则两种评估方式。前者使用人工或模型标注的评分方案来强化评分锚点，后者要求验证器独立发现明显错误，防止策略过度拟合评分细则模式。在最终聚合时，我们采用悲观下限估计：只有当多个验证器都认可时，候选答案才能获得高分。
这是一个相对繁重的验证流程，会明显拖慢训练速度。但在我们的实践中，缩小奖励优化空间是对抗奖励破解最有效的方法之一。相比让策略更快获得奖励，我们更关心奖励是否足够可信，尤其是假阳性是否得到了充分降低。
证明型强化学习验证器的分层设计
证明型强化学习验证器的分层设计：目标是获得具有强抗破解能力的奖励来源。第一层拦截模型输出中的不良案例，一旦匹配到不良案例，后续所有操作都会被跳过，该样本直接得零分。第二层通过调用模型将输出转换为统一格式，对候选解答进行格式规范化。第三层执行实际的生成式验证器调用，使用多个模型和多种模式并行调用三个不同配置的验证器，获得多个分数。第四层采用悲观估计进行分数聚合，取各来源中的最低分作为最终分数。
强化学习设置：过滤干扰样本以获得更优学习信号
在强化学习算法方面，我们继续沿用 M2 周期中的 CISPO，以 forge 作为训练框架。对于数学证明任务，我们仅做了轻量级改动。核心目标是让奖励信号更加稳定，而非引入复杂的过程级奖励。
具体来说，我们直接使用验证器连续的 [0, 1] 分数作为整个轨迹的奖励，而不进一步将其拆分为步骤级或过程级信号。与纯粹的 0/1 奖励相比，连续奖励更密集：即使一个组内的所有样本仅部分正确，它们仍可能提供可学习的相对差异。但这也会放大验证器自身的不稳定性。特别是当候选分数接近时，微小的噪声可能被误认为是真实的偏好。
为了解决这个问题，我们引入了一个标准差阈值过滤器：当一个组内的奖励方差过低时，我们过滤掉整个组，不将其用于更新。直观地说，如果组内奖励差异极小，那么它们所包含的学习方向更可能是噪声。只有当组内存在足够显著的奖励差异时，我们才将该组视为提供了可靠的优化信号。
数据准备：细致的领域与技巧平衡
训练数据主要来自公开可用的网络数学奥林匹克风格题目。在数据挖掘和清洗过程中，我们为每道题构建了以下元数据：
字段 内容
题目陈述 题目原文
参考答案 一份完整的人类专家解答，通常来自论坛评论，用于后续的评分方案标注
领域 题目的数学分支，例如组合数学、几何、代数等
解题技巧 所涉及的具体解题技巧，来自我们的技巧分类体系
评分方案 基于人工标注的少样本示例，借助模型辅助生成的一套评分标准
在进入最终强化学习训练之前，我们应用了三个额外的后处理步骤：
步骤 目的
难度过滤 使用 M2.7 作为基线，过滤掉过于简单的题目，以减少训练预算浪费
领域平衡 按数学分支平衡数据分布，使训练不被单一题型主导
技巧平衡 控制高频解题技巧的比例，同时保留真实竞赛分布中的长尾结构
目标并非构建一个完美统一的数据集，而是要在覆盖真实竞赛分布的同时，降低少数高频领域或技巧的主导地位。
M2 的苦涩教训：一个典型的奖励黑客案例研究
在 M2 周期中，我们也尝试了类似的方法。当时，验证器采用了一种相对简单的单一评分标准判断形式。训练指标最初看似持续改善，但深入分析后发现，策略实际上学会了若干典型的黑客模式。
为了定位这些问题，我们后来将异常训练信号整理成一个奖励黑客检测仪表盘。该仪表盘不仅查看最终奖励值，还同时监控九类信号：训练/评估分数差距、分数分布中的异常双峰性、可见/思考长度漂移、证明与非证明样本之间的分数差异、结构模板趋同、开头模式趋同、思考中“等等”式自我纠正的频率、含糊其辞模式，以及一个聚合黑客分数。其目的是及早发现“训练分数上升但实际解题能力并未相应提升”的情况。
我们观察到的典型黑客模式包括：
1. 长度偏差：模型输出变得越来越长。随着训练进行，可见长度和思考长度都在增加。长文本更有可能覆盖评分标准中的关键词，也更容易让验证器相信论证是充分的。
2. 格式黑客：模型开始模仿参考答案或评分标准的表面格式，例如固定的步骤标题、验证部分、最终答案部分以及特定的开头模式。输出看起来更像“标准答案”，但其中的数学内容并不一定更可靠。
3. 语义捷径/含糊其辞：在关键节点，模型使用诸如“可以证明”或“经过简化”之类的表述，将困难的推导过程压缩成未经证明的断言。这些样本在人工检查中很容易被发现，但在单一验证器下，它们有时会获得过高的分数。
4. 评判者特定偏好：策略逐渐向特定评判者偏好的表达分布偏移。一旦奖励来源过于狭窄，训练可能会优化出更讨好评判者的证明，而非更正确的证明。
这些教训直接塑造了 M3 周期中验证器的设计。我们的主要收获是：在高难度数学证明的强化学习中，奖励作弊往往不是一个突发的离散事件，而是输出分布缓慢偏移的结果。静态评估无法完全暴露问题。我们必须在训练过程中持续监控输出形式、奖励分布、长度变化、模板收敛、模糊表述频率以及验证器分歧。更重要的是，奖励系统应主动限制策略可利用的漏洞，而不是等到作弊出现后再打补丁。
M2 周期中证明强化学习奖励作弊的案例研究：（1）我们将训练时的评分方法与独立的预言机评分器进行了比较。假阳性率（定义为训练高分（>=0.7）但预言机低分（<=0.3）的样本占比）在训练期间从约 2.9% 上升至 8.0%，增长了 2.7 倍。这意味着随着训练的持续，模型生成了越来越多看似正确实则错误的解答。（2）长度偏差：除了思考过程变长，可见候选解答的长度也几乎增加了两倍，从 3500 字符增至 10000 字符，这是一个危险信号。（3）结构化模板（如"步骤 N"标题和"验证"部分）的出现率收敛至 70-80%。（4）开头模式几乎完全翻转。"要证明/要解决……"从约 80% 降至 10%，而"已知……"从 10% 升至 90%。模型实际上并未提升数学正确性，它只是学会了大语言模型评判者偏好的表面风格特征。这是奖励作弊的一种典型形式。
在 Proof RL 中，验证器的任务并非简单地区分对错。它的作用是在一个充满噪声、机会主义和随机性的搜索空间内，构建一个真正值得信赖的奖励世界。原始候选答案就像未经加工的矿石：有些蕴含着真正的洞见，而另一些则混杂着冗长、投机取巧或错误的推理轨迹。为了让强化学习获得稳定可靠的优化方向，验证器必须逐步将这些信号投射到一个可控、可信且可验证的子空间中。从异常值剔除、表示归一化到保守聚合，验证器的本质是在混沌中建立秩序，从噪声中提取真相。它所守护的不仅仅是一个奖励函数，更是让整个 Proof RL 系统迈向可靠推理能力的基石。
验证器对齐
要提高模型在硬数学问题上的能力，“判断一个证明是否正确”是与“编写一个证明”同等重要的原子能力。一个能够持续识别证明在何处出错以及根本问题是什么的验证器，其本身就是一种数学推理能力。它支持自我检查、错误修正以及更长的多轮自我迭代。因此，除了 Proof RL 之外，我们还训练了一个独立的验证器专家，在 M3 内部赋予其这种原子能力。
任务建模：联合错误发现与分类
训练验证器最直接的方法是让它对候选证明输出一个判定类别。我们刻意避开了这条路径。如果模型只预测四个标签（无错误、小缺陷、有错误、根本性错误）中的一个，那么训练信号就停留在标签层面。模型或许能从候选答案的表面模式中学到一个不错的分类器，但它并没有真正学会“阅读”证明。它没有学会如何定位和解释错误。
因此，我们将该任务定义为错误发现与分类的联合任务。模型必须首先对证明中的每个关键步骤进行分析，明确列出错误位置和描述，然后基于该分析给出判定结果。两部分均受奖励信号监督：判定结果必须与标准判定一致，错误描述必须在语义上与标准错误匹配。这种设计迫使模型明确陈述"证明错在哪里"，使验证器成为一种可问责的能力，而非浅层的分类器。
模型输出格式与 Proof RL 中使用的验证器系统保持一致：
Step-by-step analysis of the proof 1. ... (specific error description; "none" means no error) 2. ... no_errors / minor_gaps / has_errors / fundamentally_wrong
训练数据：直接复用 Proof RL 的历史数据
对齐目标并非任何单一评判者，而是 Proof RL 中经过最小聚合后实际生效的最终验证器，即多个评判者经悲观最小聚合后产生的最终判定结果和错误描述。这与 Proof RL 中用于给策略打分的最终奖励信号来源相同，确保验证专家在训练过程中学到的评判标准与证明专家所面对的标准一致。
数据来自 Proof RL 阶段的验证集，按提示词严格划分以防止数据泄露。原始数据中，no_errors 和 has_errors 占主导地位，合计约 65%，而 minor_gaps 和 fundamentally_wrong 相对稀少。我们对四类判定结果进行平衡，防止验证器偏向极端类别（no_errors / fundamentally_wrong）或丧失识别中间类别（如 minor_gaps）的能力。
验证器强化学习训练：双目标优化
基础模型为 M3 base，与证明专家同源。
奖励信号直接遵循错误发现与分类的联合设定：
R = 0.7 * R_error + 0.3 * R_verdict
R_error 是基于大语言模型的语义对齐，主要奖励错误定位和描述质量。
R_verdict 按排序距离对四类判定结果进行评分。距离为 0、1 和 >= 2 分别获得 1.0、0.5 和 0 分，用于监督判定结果的一致性。
这种权重结构防止了评分结果脱离错误而独立优化。仅仅猜对评分结果无法获得大部分奖励。模型还必须正确指出错误，才能获得高分。
精炼增强
证明专家解决了“从头编写证明”的问题。验证专家解决了“判断证明是否正确”的问题。但在解决高难度数学问题的实际流程中，还存在第三种原子能力：给定一个现有证明及其错误诊断，编写一个修正后的证明。这种精炼现有证明的能力与从头生成不同。精炼要求模型理解原始证明的结构，定位批评所指出的具体步骤，并在保留正确部分的同时修复证明。我们将这一阶段称为精炼增强，它产生了修正专家。
任务建模
精炼任务的输入是一个三元组：
(problem, flawed_proof, verification_analysis)
其中，flawed_proof 是一个被判定存在问题的候选证明，verification_analysis 是相应的错误诊断，包括错误位置、错误描述和评分结果。模型输出一个修正后的证明。
训练数据：来自第一阶段证明强化学习的自然积累
数据完全来自证明强化学习的副产品。在证明强化学习训练过程中，策略模型在每次迭代中都会生成许多候选证明，外部验证器会为每个候选证明附上完整的分析和评分结果。被判定为 minor_gaps、has_errors 或 fundamentally_wrong 的候选证明自然形成了 (flawed_proof, verification_analysis) 对。错误真实存在，诊断也真实存在，无需额外标注。
训练方法：拒绝采样微调
我们使用拒绝采样继续微调证明专家：
对于每个 (problem, flawed_proof, verification_analysis)，在精炼提示词下，从证明专家中采样多个修正后的证明。
使用与证明强化学习相同来源的最终验证器对每个采样的证明进行评分。
保留那些评分结果提升至 no_errors 或 minor_gaps 的成功精炼样本，并将其用作 SFT 训练数据。
在筛选后的数据上继续微调证明专家，从而得到固定专家。
这种拒绝采样方法确保了训练数据完全由实际成功的改进行为构成，避免了低质量的修正噪声。由于评分使用了与证明强化学习相同的验证器来源，因此改进能力的评判标准与证明专家在训练过程中所面对的标准保持一致。
MaxProof：测试时扩展框架
设计理念：将测试时扩展建模为进化搜索
一旦求解器模型具备了足够的 best@K 能力，从 best@K 到 pass@1 的桥梁本质上就是在不可微解空间中进行引导搜索的问题。MaxProof 的设计理念是将此问题建模为标准进化搜索算法：
进化算法概念 MaxProof 组件
种群 候选解池
适应度函数 来自验证器的奖励
选择 根据奖励选择得分最高的 M 个父代
变异/交叉 改进操作：用于局部修复的 PATCH 和用于重新探索的 REWRITE
交叉信号 兄弟候选解的摘要，作为“来自其他个体的经验”输入到改进过程中
精英保留 被判定为完美的候选解不再进行变异，直接保留至最终阶段
锦标赛选择 最终自选阶段中的成对排序锦标赛
收敛准则 自适应提前停止，当多个个体同时达到适应度上限时触发
这种映射并非事后添加的标签。它对应着我们相信一个测试时扩展框架必须解决的三个核心问题。
首先，我们如何从一个不可靠的单次生成器中获得“群体的智慧”？答案是采样多个候选解，并在种群层面平滑噪声。
其次，当种群中同时存在优劣个体时，我们如何利用种群信息让较弱的候选解变得更好？答案是选择加变异：让强候选解作为父代，并生成它们的改进版本。通过兄弟交叉学习，变异不仅参考父代自身的缺陷，也参考其他个体的失败模式。
第三，我们如何从最终种群中选出最优个体？仅凭适应度是不够的，因为其存在噪声。我们需要采用锦标赛式的两两比较来降低噪声。
完整的 MaxProof TTS 算法流程
完整的 MaxProof TTS 算法流程。一个典型配置为：初始化时采样 `N=32` 个候选解；对每个候选解独立验证 `K_verify=4` 次；进化循环最多运行 `R=10` 轮；每轮选择 `M=4` 个多样化父代；在最终排序锦标赛中，每次两两比较使用 `K_ranker=3` 次投票进行多数决策。实际部署时，这些参数可根据问题难度和推理预算进行调整。(1) 种群初始化：针对输入问题生成 `N` 个独立候选解。每个候选解被独立验证 `K_verify` 次，并聚合为 `reward / fitness in [0, 1]`（奖励/适应度，取值范围 [0, 1]）；同时生成摘要，用一句话记录解题思路和关键问题。(2) 精英选择：每轮从候选池中选择前 M 个多样化父代。已达到完美判决的候选解不再参与变异，通过精英策略保留至最终排序环节。(3) 双模式变异：对每个父代，并行生成两个子代。PATCH 模式通过局部修复现有证明进行利用；REWRITE 模式通过从新方向重组证明进行探索。优化提示词中包含子代摘要作为上下文，使后代能够吸收其他候选解的失败模式和局部洞见。(4) 子代评估：对子代再次执行多路径验证、奖励聚合和摘要生成，然后将其加入候选池。(5) 自适应早停：如果候选池中至少有两个候选解在 `K_verify` 次验证中均达到 `no_errors`（无错误）状态，则提前停止进化并进入最终排序。否则，继续运行直至达到最大轮数。(6) 自选锦标赛：若触发早停，则使用完美候选解进行锦标赛；否则，从候选池中取前 4 个候选解。每次两两比较使用多次排序投票和多数决策。单败淘汰制持续进行，直至只剩一个最终最佳候选解。
关键设计约束
进化搜索的有效性依赖于若干结构性假设。以下是 MaxProof 具体实现这些假设的方式。
适应度函数必须可靠。验证器的输出直接驱动整个进化过程。如果适应度出错，选择和终止都会受到污染，整个搜索可能收敛到错误的方向。在提示词层面，我们施加了相当严格的约束，要求验证器明确区分候选者实际写出的内容与验证器自行推断的内容，这样它就不会把不完整的候选者“代笔”成完美的答案。这是最容易忽视的设计细节之一，但在实践中却能带来最大的收益之一。
变异必须在利用与探索之间取得平衡。单一的变异算子很容易陷入局部最优。如果我们只使用 PATCH 式的精炼，系统可能会无休止地优化一个方向错误的证明。如果我们只使用 REWRITE，则可能破坏一个已经接近正确的证明。双重精炼，即 PATCH 与 REWRITE 并行，充当了一种粗粒度的多目标变异，确保每一代都同时包含保守型和激进型的后代。
当适应度值趋同时，选择需要二阶信号。当种群中多个个体的适应度相近时，仅凭适应度排序无法识别出最优个体。此时，两两比较提供了二阶信号。排名锦标赛就扮演了这个角色：在适应度失去区分力的区域，直接比较取代了绝对评分。
终止不能仅依赖单一体的信号。早停必须依赖于种群级别的信号，因为即使是适应度满分的个体，也可能是适应度函数的误报。要求至少两个个体同时达到适应度上限，是利用种群冗余来对冲适应度函数本身的噪声。
M3 + MaxProof 搜索过程
MaxProof 搜索过程中的 Oracle 最佳得分进化
MaxProof 搜索过程中 Oracle 最佳分数的演变。x 轴表示优化轮次，其中 R=0 代表初始化采样阶段。y 轴表示截至当前轮次候选池中任何候选方案所达到的最佳分数，最高为 7/7。黑色线条展示了六个问题上的平均 Oracle 最佳分数。星号表示最终的自我选择结果，圆圈表示最终选择落在池中最佳候选方案上但尚未获得满分的情况，叉号表示候选池中存在更优解但自我选择未能将其选出的情况。
从搜索曲线来看，MaxProof 的收益主要来自两个阶段。首先是种群初始化：仅凭 32 个初始候选方案，部分问题在候选池中就已出现高分甚至满分方案。这表明合并后的 M3 模型已具备有意义的 best@K 能力。其次是迭代优化：随着 PATCH / REWRITE 轮次的累积，候选池中的 Oracle 最佳分数持续上升。这一点在初始候选方案未能直接命中解的问题上尤为明显。优化可以进一步推进现有候选方案中的局部思路，或通过重写来摆脱错误方向。
结论与未来方向
在困难的数学推理问题上，我们与闭源和开源社区的最高水平之间仍存在明显差距。本文介绍了 Proof RL、验证器对齐和优化增强，分别对应三项核心能力。Proof RL 提升了从零开始生成证明的上限。验证器对齐赋予模型更可靠的错误发现能力。优化增强将 Proof RL 过程中自然产生的大量失败样本转化为用于证明修复的训练数据。最后，MaxProof 将这些能力组织成一个种群级别的进化搜索框架，将 best@K 能力转化为更稳定的最终输出。
数学证明是检验可靠推理的高难度试验场。它要求模型不仅给出看似合理的答案，还要在长链条推理、严格约束条件和极低容错率下保持正确性。围绕生成式验证器的实践教训尤为清晰：当验证器被用作强化学习奖励时，其主要目标不应是在静态基准上追求最高平均准确率，而应构建一个低误报率、持续监控且对策略利用具有强抵抗力的可信奖励系统。这些正是让生成式验证器真正可用的工程约束条件。MaxProof 是我们朝此方向迈出的当前一步。