一句话总结

MaxProof 是一个面向 MiniMax-M3 系列的群体级测试时扩展框架，利用生成式验证器强化学习训练证明生成、验证和基于批评的条件修复能力，采用候选证明群体的锦标赛选择，在 IMO 2025 上获得 35/42 分，在 USAMO 2026 上获得 36/42 分，均超过人类金牌分数线。

核心贡献

• 本文介绍了 MaxProof，这是一个面向 MiniMax-M3 系列竞赛级数学证明的群体级测试时扩展框架。该系统利用专为低误报率设计的纵深防御生成式验证器训练三种面向证明的能力，随后将它们合并为单个发布模型。
• 在推理期间，该框架将模型视为生成器、验证器、精炼器和排名器，在候选证明群体中进行搜索。最终证明通过聚合这些能力的锦标赛选择过程选定。
• 实验结果表明，M3 模型通过这种扩展方法在 IMO 2025 上获得 35/42 分，在 USAMO 2026 上获得 36/42 分。这些性能指标在两项竞赛基准上均超过人类金牌分数线。

数据集

• 数据集构成与来源
  • 主要训练数据来源于包含问题陈述和人类编写参考解答的公开竞赛资源。
  • 专用专家模型利用直接从 Proof Expert 训练运行中收集的数据，以消除额外的标注成本。
• 关键子集详情
  • Proof Expert： 问题包含数学领域和解题技巧的标注。团队排除像 IMO 2025 这样的保留评估集，并应用近重复过滤。
  • Verifier Expert： 该集包含问题、候选、分析、错误和判决的元组。作者选择与悲观最小分数配对的批评，以与 Proof Expert 的奖励信号保持一致。
  • Fixer Expert： 该子集捕获由 minor_gaps 或 fundamentallyWrong 等判决识别出的有缺陷证明。
• 处理与平衡
  • 评分方案由强模型利用少样本提示对照人类范例生成。
  • 难度过滤移除上一代 M2.7 模型能可靠解决的问题。
  • 领域平衡确保代数、组合学、几何和数论得到均匀表示。
  • 技巧频率控制平滑高频出现情况，同时保留罕见技术的长尾。
  • 类别重平衡调整 Verifier 数据集，以避免极端判决的过度代表。
• 训练划分与防泄漏
  • Verifier 和 Fixer 专家的数据按提示而非候选进行划分，以防止从 Proof Expert 分布中泄漏。
  • 目标避免均匀的数据集混合，以保留结构信息，同时确保没有单一领域或技巧主导训练过程。

方法

MaxProof 框架引入了 MiniMax-M3 模型，该模型训练以掌握三种核心面向证明的能力：证明生成、证明验证和基于批评的条件证明修复。这些能力被蒸馏为三个专用模块，即 Proof Expert、Verifier Expert 和 Fixer Expert。在训练阶段，这些专家独立开发，随后合并为单个发布模型。在推理时，MaxProof 系统通过提示激活相关能力以执行群体级测试时扩展。从专家训练到进化搜索过程的完整管道如框架图所示。

Proof Expert 使用长视界强化学习 (RL) 训练，以生成偶尔接近正确的证明。该过程的奖励信号由纵深防御生成式验证器提供。此验证器至关重要，因为它定义了策略的奖励景观。为确保稳定性并防止奖励黑客攻击，验证器采用多层防御策略。这包括过滤坏案例，将解决方案归一化到信任区域以减少格式偏差，并通过多裁判评分应用悲观判断。验证器管道详述了这些防御层。

Proof Expert 的训练目标利用 CISPO，这是一种离线策略 REINFORCE 风格算法。对于问题 $p$p，采样 $G$G 个候选证明组，每个获得验证器奖励 $R_i \in [0, 7]$Ri​∈[0,7]。组归一化优势 $A_i$Ai​ 计算如下：

$$A_i = \frac{R_i - \mu_R}{\sigma_R + \epsilon}, \quad \mu_R = \frac{1}{G} \sum_{j=1}^{G} R_j, \quad \sigma_R = \sqrt{\frac{1}{G} \sum_{j=1}^{G} (R_j - \mu_R)^2}$$Ai​=σR​+ϵRi​−μR​​,μR​=G1​j=1∑G​Rj​,σR​=G1​j=1∑G​(Rj​−μR​)2​

为防止来自噪声信号的更新，应用组级标准差阈值滤波器，确保仅当 $\sigma_R > \tau_{\text{std}}$σR​>τstd​ 时 rollout 组才贡献更新。

Verifier Expert 训练以执行对齐的错误查找而非简单分数预测。它被提示生成包含 <assessment> 块、<errors> 块和 <verdict> 的结构化输出。这种表述确保模型在做出判决前阅读证明以定位错误。Fixer Expert 通过拒绝采样微调 (RSFT) 在 (问题，flawed_proof, verification_analysis) 三元组上训练。它学习通过解决特定批评来修复证明，同时保留正确部分，使用相同的保守验证器验证成功修复。

在测试时，MaxProof 将合并后的 M3 模型视为生成器、验证器、精炼器和排名器，通过群体搜索扩展性能。该过程首先初始化 $N$N 个独立候选的群体。在进化循环的每轮中，系统选择多样化的父代，应用双模式变异（PATCH 用于局部精炼，REWRITE 用于探索性搜索），并使用验证器评估后代。档案用新候选更新，该过程继续直到满足早停条件或轮次预算耗尽。最后，成对锦标赛从顶级档案条目中选择最佳候选。详细的进化循环和选择过程如下图所示。

Proof Expert 以反映人类数学推理的结构化逐步格式生成输出。这包括理解问题、确定关键条件、分析特定案例和排除其他可能性的部分。该策略输出结构的示例展示了模型如何将复杂的平铺问题分解为逻辑步骤，显式检查必要和充分条件。

实验

M2 周期识别了单一裁判验证中的关键奖励黑客攻击漏洞，促使开发分层 M3 验证器管道以抑制格式操纵和语义捷径。评估表明，虽然基础 M3 模型在数学证明基准上取得了有竞争力的独立分数，但 MaxProof 框架通过利用测试时扩展来精炼和选择高质量证明，大幅提高了竞赛性能。这些发现确认结构化系统设计可以有效缩小与前沿模型的差距，尽管在选择准确性和解决超出基础模型能力上限的问题方面仍存在挑战。

该表详细说明了结合 MaxProof 框架的 M3 模型的逐问题性能，比较系统的最终选择与搜索群体中发现的最佳解决方案。它突出显示了一个差异，即系统在一个问题上选择了次优解决方案，尽管有更好的解决方案可用，而在其他问题上成功找到完美证明。系统在几个问题上取得了满分，由于初始群体包含正确解决方案，某些问题立即触发早停。USAMO P2 上发生了显著的选择损失，排名器更喜欢风格不同但分数较低的候选者，而不是搜索后期发现的高分解决方案。USAMO P3 在 self-pick 和 oracle-best 方面均保持高但非完美的分数，表明模型在配置的搜索轮次内未能生成完美证明。

该研究评估了模型在两项数学竞赛上的性能，通过比较其自选解决方案与搜索群体中发现的最佳解决方案。结果表明，系统成功识别并选择了大多数问题的完美证明，尽管在更难的问题上观察到选择准确性和基础能力的特定失败。系统在大多数问题上匹配了最佳可能的搜索结果，在两项竞赛中均取得满分。一个 USAMO 问题显示出最佳可用证明与系统最终选择之间的巨大差距。最难 IMO 问题得分为零，表明基础模型缺乏针对该特定挑战的可行方法。

该表展示了 M3 模型在多个精炼轮次中在数学竞赛基准上的性能演变。虽然大多数问题在过程早期收敛到最高可能分数，但特定案例突出了明显的局限性，包括完全无法解决、停滞在部分分数以及选择错误（忽略了更好的解决方案）。大多数问题在早期精炼阶段达到最高分数。一个特定问题在所有轮次中均未能从初始尝试中改进。一个案例显示群体在后期轮次中找到了高分解决方案，但最终选择未能捕捉到它。

该研究评估了合并后的 M3 模型在两个数学证明基准上的表现，将其与几个不使用 MaxProof 扩展框架的前沿闭源系统进行比较。结果表明，虽然 M3 展示了强大的能力，特别是在基于答案的任务上，但在证明构建质量上仍落后于领先模型。M3 在证明构建和答案基准上均优于 Opus 4.7。该模型在两个评估集上均落后于 GPT-5.5 和 Gemini 3.1 Pro 等顶级系统。M3 与领先模型之间的性能差距在答案基准上比在证明构建基准上更窄。

研究团队在 IMO 2025 和 USAMO 2026 上评估了 M3 模型，比较标准 one-shot 设置与 MaxProof 测试时扩展框架。结果表明，MaxProof 在两项竞赛上均提供了比基线大幅的性能提升，增益在 USAMO 2026 上显得更为显著。这证明了该框架将基础模型能力转化为更强竞赛级结果的能力。MaxProof 在两个数学证明基准上均显著优于 one-shot 基线。USAMO 2026 的性能增益大于 IMO 2025。测试时扩展框架有效稳定了高级问题解决。

实验使用 MaxProof 框架在数学竞赛基准上评估 M3 模型，比较最终选择与搜索群体中发现的最佳解决方案，并评估与其他前沿系统的性能。结果表明，MaxProof 提供了比标准基线大幅的性能提升，使系统能够在大多数问题上取得满分，尽管偶尔会出现忽略更优候选的选择错误。虽然模型优于一些竞争对手，但在证明构建质量上仍继续落后于领先的闭源系统，特别是在基础能力限制仍然明显的最困难挑战上。