MaxProof框架：MiniMax M3在IMO 2025和USAMO 2026超越人类金牌线

引言

在 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 的迭代过程中，我们也致力于将更强的数学证明和自我改进能力整合到最终的通用模型中。

在方法论层面，开源社区已经为一次性设定下解决高难度数学问题勾勒出了一条相对清晰的路径：首先将模型的 best@K 能力提升到足够高，然后利用测试时扩展将 best@K 转化为更稳定的 pass@1。我们的方法遵循同样的两个方向。第一部分是基础模型能力提升：我们训练了三个专家模型，分别用于改进证明生成、错误判断和证明修复。第二部分是测试时扩展：我们设计了 MaxProof，一个进化搜索风格的 TTS 框架，让最终合并的 M3 模型通过多轮自我迭代来解决问题。本文重点讨论训练特征、系统设计权衡以及我们学到的实践经验。

改进基础模型

本节介绍我们如何在单模型侧构建数学证明与自我改进所需的若干原子能力。

整体布局

第一部分概述：在基座模型改进方面，我们采用了一个三阶段训练方案，并产出了三个专家模型。第一阶段，Proof RL，产出 Proof Expert。我们通过 RL 后训练为数学问题构建了一套奖励系统，对候选证明进行评分，并运行长时程强化学习。第二阶段 2.1，Verifier Alignment，产出 Verifier Expert。我们利用在 Proof RL 期间积累的黄金验证分析，将验证器对齐形式化为一个找错任务，并使用 RL 来对齐模型定位和判断错误的能力。第二阶段 2.2，Refinement Augmentation，产出 Fixed Expert。我们复用 Proof RL 过程中自然产生的（历史有缺陷证明、验证分析）配对，通过拒绝采样继续微调 Proof Expert，使模型学会基于错误诊断修复已有证明。这三个专家模型都被用于 M3 的最终合并训练。

Proof RL：重生成式验证的一次实践探索

Proof RL 的目标是在 M3 上运行长时程 RL 训练，并提升模型直接生成数学证明的能力。与传统 RLVR 相比，我们最大的变化在于奖励主要由一个生成式验证器提供。这带来了一个直接挑战：训练过程必须系统性地处理不准确的奖励信号、噪声、假阳性以及奖励黑客问题。

在相关工作中，DeepSeek-Math-V2 是最早展示在困难数学问题训练中稳定使用生成式验证器的开源案例之一。其核心思想是自验证加元验证。我们并未完全沿用同样的路线，主要是因为 M 系列模型在此前的迭代中尚未积累足够的验证能力。短期内，模型很难自行产生足够可靠的奖励信号。

因此在这一阶段，我们首先专注于提升证明能力，并使用外部前沿模型作为生成式验证器。该系统的关键设计包含三个部分：验证器设计、RL 算法改动以及训练数据准备。

验证器设计：低误报率实现长而稳定的 RL

Proof RL 验证器的设计理念，是将嘈杂且异构的信号投影到一个受控、可信的子空间中。这是可靠推理的基础。原始候选空间包含多样化的解题尝试、带噪样本以及潜在失效模式，从极长的推理链到偏离所需格式的输出，不一而足。每一种都可能干扰学习。验证器的职责，是以算法化的方式严格过滤并结构化这一混沌信号，进而产出稳定的奖励信号。首先，它执行离群值过滤：与已知失效模式匹配或明显违反规则的候选输出，直接赋零分。从数学上看，这是对信号空间的硬约束，可防止误导性的 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] 内的连续分数。验证器根据问题元数据评估候选解答的完整性与数学严谨性。在我们的设置中，验证器模型主要采用最新的前沿模型。

具体设计

经过多轮训练与调优，我们发现，在静态评测上获得一个"看起来足够准确"的验证器远远不够。生成式验证器天然不稳定，而这种不稳定性会在 RL 过程中被策略不断放大，最终导致训练崩溃。我们在 M2 周期就已经观察到类似问题，因此在 M3 周期我们采取了更为保守的原则：

**当生成式验证器被用作 RL 奖励时，长期稳定训练的首要任务不是提升平均准确率，而是尽可能抑制假阳性。即使这会增加假阴性，策略能够优化的空间也应保持足够狭窄。**

基于这一原则，我们将奖励系统设计为分层防御结构。

- 坏例防御：我们使用多层代码级规则来拦截明显异常的输出，例如未聚合的思考过程或过长的解答。一旦匹配到坏例，我们便跳过后续的验证器调用并直接赋零分，防止低质量输出意外获得奖励。

- 模式偏移防御：M2 周期的经验表明，奖励黑客行为往往并不意味着解题能力突然提升。相反，输出风格可能已经偏移到了验证器偏好的格式。为降低验证器对特定表达模式的偏好，我们在将候选解发送给生成式验证器之前对其进行归一化处理，尽可能让候选解保持在相同的评估分布内。

- 多维悲观聚合：我们同时使用多个验证器模型和多种验证器模式。双模型设置降低了训练向单一评判者漂移的风险。双模式设置同时包含有评分标准和无评分标准两种评估方式。前者使用人工或模型标注的评分方案来强化评分锚点。后者要求验证器独立发现明显错误，防止策略过拟合到评分标准模式上。在最终聚合中，我们采用悲观下界估计：只有当多个验证器都认可时，候选解才能获得高分。

这是一条相对繁重的验证流水线，会明显拖慢训练速度。但在我们的实践中，收窄奖励优化空间是对抗奖励黑客行为最有效的方式之一。与让策略更快获得奖励相比，我们更关心奖励是否足够可信，尤其是误报是否已被充分降低。

Proof RL 验证器的分层设计：目标是获得一个具有强抗攻击能力的奖励来源。第 1 层拦截模型输出中的不良案例。一旦匹配到不良案例，后续所有操作都会被跳过，该样本得分为零。第 2 层通过调用模型将输出转换为统一格式，从而规范化候选解答的格式。第 3 层执行实际的生成式验证器调用，使用多个模型和多种模式并行调用三个配置不同的验证器，获得多个分数。第 4 层以悲观估计聚合分数，取各来源中的最低分作为最终分数。

RL 设置：过滤干扰样本以获得更好的学习信号

在 RL 算法方面，我们继续沿用 M2 周期的 CISPO，并以 forge 作为训练框架。对于数学证明，我们只做了轻量级改动。核心目标是让奖励信号更加稳定，而不是引入复杂的流程级奖励。

具体而言，我们直接使用验证器的连续 [0, 1] 分数作为整条轨迹的奖励，而不再将其进一步拆分为步骤级或流程级信号。与纯粹的 0/1 奖励相比，连续奖励更加密集：即使一组中的所有样本都只是部分正确，它们仍可能提供可学习的相对差异。但它也会放大验证器自身的不稳定性。尤其是当候选解答的分数接近时，微小的噪声可能被误认为是真实的偏好。

为了解决这一问题，我们引入了标准差阈值过滤：当组内奖励方差过低时，我们过滤掉整个组，不将其用于更新。直观地说，如果组内奖励差异很小，其中包含的学习方向更可能是噪声。只有当组内存在足够显著的奖励差异时，我们才认为该组提供了可靠的优化信号。

数据准备：精心的领域与技巧平衡

训练数据主要来自公开可获取的互联网数学奥林匹克竞赛风格题目。在数据挖掘和清洗过程中，我们为每道题构建以下元数据：

在进入最终 RL 训练之前，我们额外应用了三个后处理步骤：

目标不是构建一个完全均匀的数据集，而是在覆盖真实竞赛分布的同时，减少少数高频领域或技巧的主导地位。

来自 M2 的痛苦教训：一个典型的奖励黑客案例研究

在 M2 周期中，我们也尝试了类似的方法。当时，验证器采用的是相对简单的单一评分标准评判形式。训练指标最初看起来在持续改善，但更深入的分析表明，策略实际上已经学会了若干典型的作弊模式。

为了定位这些问题，我们后来将异常训练信号整理成了一个奖励黑客检测仪表盘。该仪表盘不仅关注最终奖励，还同时监控九类信号：训练/评估分数差距、分数分布中异常的双峰现象、可见/思考长度漂移、有证明与无证明样本之间的分数差异、结构模板收敛、开头模式收敛、思考中"Wait"式自我纠正的频率、空泛论述模式，以及一个综合作弊分数。其目的是及早发现"训练分数上升但真实问题解决能力并未相应提升"的情况。

我们观察到的典型作弊模式包括：

1. 长度偏差：模型输出变得越来越长。随着训练推进，可见长度和思考长度都在增加。长文本更有可能覆盖评分标准中的关键词，也更有可能让验证器相信论证已经足够充分。

2. 格式作弊：模型开始模仿参考解答或评分标准的表面格式，例如固定的步骤标题、验证部分、最终答案部分以及特定的开头模式。输出看起来更像一份“标准答案”，但数学内容未必更可靠。

3. 语义捷径 / 含糊其辞：在关键节点，模型使用“可以证明”或“化简后”之类的表述，将困难的推导压缩为未经证明的断言。这些样本在人工检查时很容易被发现，但在单一验证器下，它们有时会获得过高的评分。

4. 评判器特定偏好：策略逐渐向某个特定评判器偏好的表达分布靠拢。一旦奖励来源过于狭窄，训练可能优化出更能取悦评判器的证明，而非更正确的证明。

这些经验直接影响了 M3 周期中验证器的设计。我们的主要结论是：在高难度数学证明的 RL 中，奖励作弊往往不是突然发生的离散事件，而是输出分布缓慢偏移的结果。静态评估无法完全暴露问题。我们必须在训练过程中持续监控输出形式、奖励分布、长度变化、模板收敛、含糊其辞的频率以及验证器分歧。更重要的是，奖励系统应主动限制策略可用的漏洞，而不是等到作弊出现后再去修补。

M2 周期中 Proof RL 奖励黑客攻击的案例研究：(1) 我们将训练时的评分方法与一个独立的 oracle 评分器进行了对比。假阳性率——即训练得分高（>= 0.7）但 oracle 得分低（<= 0.3）的样本占比——在训练过程中从约 2.9% 上升到 8.0%，增长了 2.7 倍。这意味着随着训练持续，模型生成越来越多看起来不错但实际上错误的解法。(2) 长度偏差：除了思考更长之外，可见候选解法的长度也几乎增长到三倍，从 3.5K 字符增加到 10K 字符，这是一个危险信号。(3) 诸如“Step N”标题和“Verification”部分等结构化模板的出现率收敛到 70-80%。(4) 开头模式几乎完全翻转。“To prove / To solve...”从约 80% 下降到 10%，而“We are given...”从 10% 上升到 90%。模型并没有真正提升数学正确性。它学到的是 LLM 评判器偏好的表面风格特征。这是奖励黑客攻击的一种典型形式。

star2 在 Proof RL 中，验证器的使命并非简单地分辨对错。它的角色是在一个充满噪声、机会主义和随机性的搜索空间内，构建一个真正可信的奖励世界。原始候选就像未经处理的矿石：有些蕴含真正的洞见，而另一些则混入了冗长、投机或错误的推理轨迹。为了让强化学习获得稳定可靠的优化方向，验证器必须逐步将这些信号投射到一个受控、可信且可验证的子空间中。
从离群值移除和表示归一化，到保守聚合，验证器的本质是在混沌中建立秩序，从噪声中提取真相。它所守护的不仅仅是一个奖励函数，而是让整个 Proof RL 系统走向可靠推理能力的基础。

验证器对齐

要提升模型在困难数学问题上的能力，“判断一个证明是否正确”是与“写出一个证明”同等重要的原子能力。一个能够稳定识别证明在哪里出错、以及根本问题是什么的验证器，本身就是一种数学推理能力。它支撑自我检查、纠错以及更长的多轮自我迭代。因此，除了 Proof RL 之外，我们还单独训练了一个 Verifier Expert，让 M3 在内部具备这一原子能力。

任务建模：错误查找与分类的联合任务

训练验证器最直接的方式，是让它为候选证明输出一个判定类别。我们刻意避开了这条路线。如果模型只预测四个标签之一（no_errors、minor_gaps、has_errors、fundamentally_wrong），训练信号就停留在标签层面。模型或许能从候选证明的表面模式中学到一个还不错的分类器，但它并没有真正学会“阅读”证明。它学不会如何定位并解释错误。

因此，我们将任务定义为错误查找与分类的联合任务。模型必须首先对证明中的每一个关键步骤进行分析，明确列出错误位置和描述，然后基于该分析给出判定。两部分都受到奖励监督：判定必须与黄金判定一致，错误必须在语义上与黄金错误匹配。这种任务形式迫使模型明确说出“证明错在哪里”，使验证器成为一种可问责的能力，而非浅层的分类器。

模型输出格式与 Proof RL 中使用的验证器系统保持一致：

<assessment>Step-by-step analysis of the proof</assessment>
<errors>
1. ... (specific error description; "none" means no error)
2. ...
</errors>
<verdict>no_errors / minor_gaps / has_errors / fundamentally_wrong</verdict>

训练数据：直接复用 Proof RL 的历史数据

对齐目标不是任何单一评判者，而是在 Proof RL 中经过 min 聚合后真正生效的最终验证器，即多个评判者经过悲观 min 聚合后产生的最终判定和错误描述。这与 Proof RL 期间用于给策略打分的最终奖励信号来源相同，确保 Verifier Expert 学到的评判标准与 Proof Expert 在训练中所面对的标准一致。

数据来自 Proof RL 阶段的 validate 划分，严格按 prompt 划分以防止泄漏。在原始数据中，no_errors 和 has_errors 占主导，合计约 65%，而 minor_gaps 和 fundamentally_wrong 相对稀少。我们对四个判定类别进行平衡，以防止验证器偏向极端类别（no_errors / fundamentally_wrong），或丧失识别 minor_gaps 等中间类别的能力。

验证器 RL 训练：双目标优化

基础模型为 M3 base，与 Proof Expert 来源相同。

奖励直接遵循联合的找错与分类公式：

R = 0.7 * R_error + 0.3 * R_verdict

• R_error 是基于 LLM 的语义对齐，主要奖励错误定位和描述质量。
• R_verdict 通过排序距离对四类判定结果进行评分。距离为 0、1 和 >= 2 时分别获得 1.0、0.5 和 0 分，以此监督判定结果的一致性。

这种权重结构防止判定结果脱离错误被独立优化。仅仅猜测判定结果无法获得奖励的主要部分。模型还必须正确指出错误才能获得高分。

精炼增强

证明专家解决了"从零开始撰写证明"的问题。验证专家解决了"判断证明是否正确"的问题。但在解决高难度数学问题的实际流程中，还存在第三种原子能力：给定一个已有证明及其错误诊断，撰写一份修正后的证明。这种精炼已有证明的能力与从零生成不同。精炼要求模型理解原始证明的结构，定位批评所引用的确切步骤，并在保留正确部分的同时修复证明。我们将这一阶段称为精炼增强，它产出了修正专家。

任务建模

精炼任务的输入是一个三元组：

(problem, flawed_proof, verification_analysis)

其中，flawed_proof 是被判定存在问题的候选证明，verification_analysis 是相应的错误诊断，包括错误位置、错误描述和判定结果。模型输出一份修订后的证明。

训练数据：来自第一阶段 Proof RL 的自然积累

数据完全来自 Proof RL 的副产品。在 Proof RL 训练过程中，策略在每次迭代时都会生成大量候选证明，外部验证器会为每个候选附加完整的分析和判定。被判定为 minor_gaps、has_errors 或 fundamentally_wrong 的候选自然形成了（flawed_proof, verification_analysis）配对。错误真实存在，诊断也真实存在，无需额外标注。

训练方法：拒绝采样微调

我们通过拒绝采样继续微调 Proof Expert：

1. 对于每个（problem, flawed_proof, verification_analysis），在精炼提示词下从 Proof Expert 采样多个修订证明。
2. 用与 Proof RL 相同来源的最终验证器对每个采样证明进行评分。
3. 保留判定提升为 no_errors 或 minor_gaps 的成功精炼样本，并将其用作 SFT 训练数据。
4. 在筛选后的数据上继续微调 Proof Expert，得到 Fixed Expert。

这种拒绝采样方法确保训练数据完全由真正成功的精炼行为构成，避免了低质量修正噪声。由于评分使用与 Proof RL 相同的验证器来源，精炼能力的评判标准与 Proof Expert 在训练中所面对的标准保持一致。

MaxProof：测试时扩展框架

设计理念：将测试时扩展建模为进化搜索

一旦求解器模型具备足够的 best@K 能力，从 best@K 到 pass@1 的跨越本质上就是在不可微解空间中进行引导搜索的问题。MaxProof 的设计理念是将这一问题建模为标准进化搜索算法：

这一映射并非事后添加的标签。它对应着我们相信一个 TTS 框架必须解决的三个核心问题。

首先，我们如何从一个不可靠的单次生成器中获得“群体智慧”？答案是采样多个候选，并在种群层面平滑噪声。

第二，当种群中同时包含优秀和劣质个体时，我们如何利用种群信息让较弱的候选变得更好？答案是选择加变异：让强候选作为父代，并生成它们的改进版本。通过同辈交叉学习，变异不仅针对父代自身的缺陷，也针对其他个体的失败模式。

第三，我们如何从最终种群中选出最佳个体？仅靠适应度是不够的，因为它带有噪声。我们需要一种锦标赛式的两两比较来降低噪声。

完整的 MaxProof TTS 算法流程。典型配置为：初始化时采样 `N=32` 个候选解；对每个候选独立验证 `K_verify=4` 次；进化循环最多运行 `R=10` 轮；每轮选出 `M=4` 个多样化的父代；在最终排名锦标赛的每次两两比较中，使用 `K_ranker=3` 票进行多数决策。在部署时，这些参数可根据问题难度和推理预算进行调整。(1) 种群初始化：为输入问题生成 `N` 个独立候选解。每个候选被独立验证 `K_verify` 次，并聚合为 `[0, 1] 区间内的 reward / fitness`；同时生成一份摘要，用一句话记录解题思路和关键问题。(2) 带精英保留的选择：每轮从候选池中选出 top-M 个多样化的父代。已经达到完美判定结果的候选不再参与变异，而是通过精英保留机制留存，供后续最终排名使用。(3) 双模式变异：对每个父代，并行生成两个子代。PATCH 通过局部修复现有证明进行利用；REWRITE 通过从新方向重组证明进行探索。精炼提示词中包含兄弟子代的摘要作为上下文，使后代能够吸收其他候选的失败模式和局部洞见。(4) 子代评估：对子代再次运行多路径验证、奖励聚合和摘要生成，然后将其加入候选池。(5) 自适应提前停止：如果候选池中至少有两个候选在 `K_verify` 次验证中均达到 `no_errors`，则提前停止进化并进入最终排名。否则，继续运行直到达到最大轮数。(6) 自选锦标赛：如果触发了提前停止，则使用完美候选进行锦标赛；否则，从候选池中取排名前 4 的候选。每次两两比较使用多个排序器的投票并以多数决策。单轮淘汰持续进行，直到只剩下一个最终的最佳候选。

关键设计约束

进化搜索的有效性建立在若干结构性假设之上。以下是 MaxProof 如何具体实现这些假设。

适应度函数必须值得信赖。验证器的输出直接驱动整个进化过程。如果适应度有误，选择和终止都会受到污染，整个搜索可能朝错误的方向收敛。在提示词层面，我们施加了相当严格的约束，要求验证器明确区分候选实际写出的内容与验证器自行推断的内容，以免它把不完整的候选“代笔”成一个完美的候选。这是最容易忽视的设计细节之一，但在实践中它带来的收益却是最大的之一。

变异必须在利用与探索之间取得平衡。单一的变异算子很容易陷入局部最优。如果我们只使用 PATCH 式的精修，系统可能会无休止地优化一个方向错误的证明。如果我们只使用 REWRITE，它可能会破坏一个已经接近正确的证明。双重精修，即 PATCH 与 REWRITE 并行，起到了粗粒度的多目标变异作用，确保每一代都同时包含保守型和激进型的后代。

当适应度值趋同时，选择需要二阶信号。当种群中多个个体具有相似的适应度时，仅靠适应度排序无法识别出最优个体。此时，两两比较提供了一种二阶信号。排序器锦标赛正是扮演这一角色：在适应度丧失区分能力的区域，直接比较取代了绝对评分。

终止条件不能仅依赖单一个体信号。提前停止必须依赖种群级别的信号，因为即使一个具有满适应度的个体，也可能是适应度函数产生的假阳性。要求至少两个个体同时达到适应度上限，利用种群冗余来对冲适应度函数本身的噪声。

M3 + MaxProof 搜索过程

MaxProof 搜索过程中 Oracle 最佳得分的演化。x 轴为精炼轮次，其中 R=0 表示初始化采样阶段。y 轴为截至当前轮次候选池中任意候选者所达到的最佳得分，最大值为 7/7。黑线显示六个问题上 Oracle 最佳得分的平均值。星号表示最终自选结果，圆圈表示最终选择落在候选池最佳候选者上但仍未达到满分的情况，叉号表示候选池中存在更优解但自选未能将其选出的情况。

从搜索曲线来看，MaxProof 的收益主要来自两个阶段。第一个是种群初始化：仅用 32 个初始候选，有些问题在候选池中就已经出现了高分甚至满分的解。这说明合并后的 M3 模型已经具备有意义的最佳@K 能力。第二个是迭代精炼：随着 PATCH / REWRITE 轮次不断累积，候选池中的 oracle 最佳分数持续上升。在初始候选未能直接命中解的问题上，这一点尤为明显。精炼可以把现有候选中的局部思路进一步推进，或者通过重写来摆脱错误的方向。

结论与未来方向

在困难的数学推理上，我们仍然看到与闭源和开源社区顶尖水平之间存在可见的差距。本文介绍了 Proof RL、Verifier Alignment 和 Refinement Augmentation，分别对应三项核心能力。Proof RL 提升了从零开始生成证明的上限。Verifier Alignment 赋予模型更可靠的找错能力。Refinement Augmentation 将 Proof RL 过程中自然产生的大量失败样本转化为用于证明修复的训练数据。最后，MaxProof 将这些能力组织成一个种群级别的进化搜索框架，把最佳@K 能力转化为更稳定的最终输出。

数学证明是对可靠推理的高压测试场。它要求模型不仅能给出看似合理的答案，还要在长链条、严格约束和极低容错率下保持正确性。围绕生成式验证器的实践教训尤为清晰：当验证器被用作 RL 奖励时，其首要目标不应是在静态基准上取得最高的平均准确率，而应是构建一个可信的奖励系统，具备低误报率、持续监控以及对策略利用的强大抵抗力。这些是让生成式验证器真正可用的工程约束。MaxProof 是我们朝这一方向迈出的当前一步。