MaxProof: 利用生成验证器强化学习与群体级别测试时缩放扩展数学证明

TL;DR MaxProof 是一个群体级测试时扩展框架，将单一模型同时用作生成、验证、修复与排序，通过锦标赛选择从候选证明中筛出最优解，在 IMO 2025 等竞赛中取得超人类金牌水平。

问题

数学证明的自动化是 AI 推理能力的重要试金石，当前领域重点关注如何让模型产出可验证的严格证明，尤其在 IMO 等竞赛级别题目上实现稳定突破。

现有方法通常采用单模型生成+自评估流水线，通过采样多个候选答案并选择得分最高者（best@K）来提高准确率，但这面临三个核心局限：

• 验证不可靠：流行的判别式打分器或生成式自评容易产生误报，将错误证明判定为正确，导致最终输出不可信。
• 缺乏修正机制：发现错误后无法有效利用反馈信息进行局部修改或重写，只能重新生成，浪费计算且难以积累经验。
• 测试时扩展不足：仅靠增加采样数 K 会遭遇收益递减，且没有在证明种群中进行交叉、变异等进化搜索，难以应对需多步推理的难题。

该问题兼具理论深度与工程价值。数学证明要求绝对逻辑自洽，微小笔误或概念混淆即导致全盘错误；竞赛题目更需复杂策略组合与创造性洞察，LLM 常因幻觉或短视规划而失败。工业现实中对可靠推理决策的需求（如代码合规验证、硬件设计）使得高精度证明能力成为 AI 落地的关键瓶颈。

类比软件持续集成：单一代码提交往往无法通过全部测试，需依赖自动化测试、错误定位、针对性补丁与迭代加固，才能构建稳定版本——这与证明的生成-验证-修复-排名循环高度一致。

核心洞察

• MaxProof 将证明生成、验证与修复三种角色统一于单一模型内，并引入群体级锦标赛搜索：这与常规自一致性或 best-of-N 不同，模型在测试时自主扮演生成、精炼、排序多角色，通过生成-验证-修复循环与锦标赛选择，持续提升证明质量。其核心突破在于用同一模型完成闭环质量提升，而非依赖外部验证器或静态重排序，从而在少样本约束下逼近人类金牌水平。
• 通过「纵深防御式生成验证器」主动抑制假阳性，MaxProof 解决了数学证明中验证可靠性难题：传统打分模型或规则验证易误判，而该工作将验证重新定义为「错误发现」任务，并利用证明训练中产生的错误数据训练验证器，使其能在保持低误报率的同时提供精细诊断，进而驱动迭代修复。这一设计使验证信噪比显著优于基于困惑度或规则的方法，是证明类任务规模化测试时计算的关键使能器。

方法

训练阶段：防御性深度生成验证器下的多能力融合

MaxProof 依赖 MiniMax-M3 模型，该模型通过一个防御性深度生成验证器（defense-in-depth generative verifier）统一习得三种证明相关子能力：

1. Proof Expert（证明生成器）：采用长时程强化学习，使用 CISPO 算法与标准差阈值过滤，基于防御性验证器提供的稠密奖励，在平衡的技巧分布数据上训练，避免奖励破解。
2. Verifier Expert（验证器）：训练目标从分数预测转向对齐的错误定位，直接指出证明步骤中的逻辑漏洞，训练数据来源自 Proof Expert 验证时产生的高质量判别样本。
3. Fixer Expert（修补器）：基于拒绝采样微调（rejection-sampling fine-tune），利用 Proof Expert RL 产生的失败案例作为训练语料，学习接收原始证明与验证器批判，输出修补后的证明。

三个专家能力最终合并到单一的 M3 模型中，在测试时通过不同的提示模板调用不同角色。

测试时缩放：MaxProof 种群级搜索循环

在测试时，MaxProof 按以下流程运行：

• 输入：一个数学证明题。
• 种群初始化：使用 Proof Expert 生成多个候选证明(gen_N)。
• 循环迭代（共 MaxRound 轮）：
  • 保守适应度评估：Verifier Expert 对每个候选证明打分，采用保守策略降低假阳性。
  • 多样化父证明选择：根据适应度及多样性指标选出父证明。
  • 精炼：对每个父证明并行执行两种改进：
    • PATCH：Fixer Expert 根据验证批判局部修补。
    • REWRITE：Proof Expert 基于父证明与批判重写。
  • 种群更新：合并精炼后证明与部分旧种群。
  • 早期停止：若检测到种群证明无改进可能，提前终止。
• 最终选择：在剩余种群中通过锦标赛选择（tournament selection）决出最优证明作为最终输出。

输出：一个经多轮群体搜索与竞争筛选的最终证明文本。

与同类方法的差异：不同于常见的 Best-of-N 采样或结果奖励模型（ORM），MaxProof 将生成式验证与证明修补封装进一个闭环的种群演化过程，利用防御性深度验证降低误判，并通过多样性保持与迭代精炼突破单一证明的瓶颈，更接近人类专家反复打磨证明的思维方式。

实验

实验设计

评估聚焦 MaxProof 在顶尖竞赛级数学证明上的端到端表现。直接将 M3 模型视作生成器、验证器、修复器和排序器，在推理时构建候选证明种群，通过锦标赛选择 (tournament selection) 迭代精炼，最终输出单一最优证明。两个高难度数据集 IMO 2025 和 USAMO 2026 各含 42 道开放式证明题，需完整推理链。

关键发现

IMO 2025 得分 35/42，USAMO 2026 得分 36/42，均显著超越人类金牌阈值 (IMO 金牌通常约 32 分)。这展示了群体级测试时缩放 (population-level test-time scaling) 的巨大潜力：不重新训练，仅通过更智能的搜索与自洽验证，即可将强模型推至竞赛顶尖水平。单题分析显示，多项证明需经过多轮 PATCH 与 REWRITE 精炼，验证器在多数情况下能成功过滤错误步骤。

与基线对比

与常见 best@K 采样不同，MaxProof 追求 pass@1 高质量输出。相比单一生成器直接采样，框架的保守适应度 (conservative fitness)、多样化父代选择 (diverse parent selection) 和早停机制 (population-level early stop) 有效规避了 reward hacking，使搜索在保持正确性的前提下高效收敛。虽然未给出直接对比的模型基线，但分数绝对值表明：在推理时，系统性地组合验证、修复与排序，相较于仅靠生成器单独工作，能带来数十分点的提升，填补了单次生成与人类顶尖证明者间的差距。

行业影响

落地场景

MaxProof 的群体级测试时扩展框架可直接嵌入高精度数学推理产品，如在线教育平台的自动证明批改与自适应辅导系统、科研领域的交互式定理证明助手，以及金融工程中的复杂衍生品定价模型校验工具。在上述场景中，系统需从大量候选解中筛选出可靠证明，MaxProof 的生成-验证-修复循环与锦标赛选择机制恰好提供了低误判率的自动化决策。

商业价值

该方案通过降低人工专家复核成本创造直接收益：竞赛级题目证明人工批阅单价高，MaxProof 可将一次通过率从 best@K 的随机性提升至稳定的 pass@1 效果，大幅减少返工。对教育企业而言，这意味着以更低的边际成本提供即时、高质量的解题反馈，改善用户留存与付费转化。对金融与安全关键领域，低假阳性验证减少错误证明引发的潜在损失，直接提升风控能力。

与现有产品 / 工作流的接口

MaxProof 可封装为无状态推理 API，输入问题描述与格式要求，输出经过群体搜索后的最终证明及验证分数。集成方式轻量：

• 在现有数学题库管道中，作为后处理微服务，对候选答案进行重排序与逐出；
• 在交互式证明编辑器中，作为“一键求精”按钮背后的异步计算资源，对用户草稿进行循环修复。

具体用例

• 教育科技：大型开放课程平台（如 edX）的数学作业自动评分系统，使用 MaxProof 对学习者提交的证明进行多轮验证与修复建议，生成可解释的评语，替代纯静态规则引擎。
• 企业服务：智能合约审计公司（如 CertiK）将 MaxProof 集成进形式化验证流程，对合约性质（如不变式）生成机器证明，并通过群体搜索降低漏报，加速审计周期，减少安全事件赔偿风险。

局限

• **验证器可靠性边界**：论文设计的 **defense-in-depth generative verifier** 通过多重防御降低误报率，但在极端复杂或新颖的证明结构中仍可能出现隐藏的漏报（假阴性）或判定偏差。训练数据虽然引入了 trick balance 和对抗案例，但验证器本身由语言模型构成，其误差分布与生成模型高度相关，可能形成系统性盲区。工程上需警惕此类耦合风险，在部署时需额外监控验证器与生成器的一致性。
• **计算效率与扩展成本**：**MaxProof** 在测试时采用群体级搜索与锦标赛选择，本质是用大量采样换取质量，计算开销远超单次生成。论文未提供 token 预算与性能的 Pareto 分析，对实际部署的性价比缺乏指导。在实时交互或资源受限场景下，这种暴力搜索策略的实用性受限，且 search budget 与 proof quality 的 scaling law 尚未刻画。
• **评估生态单一且泛化性存疑**：实验仅在 **IMO 2025** 和 **USAMO 2026** 两项竞赛的 42 道题上验证超越人类金牌线，题目数量有限且领域高度集中。未在形式化证明（如 Lean/Coq）、开放域数学问答或代码推理等任务上测试，无法判断能力是否迁移。此外，竞赛题目有明确答案导向，与现实世界开放问题中证明逻辑的探索性存在差异，方法的鲁邦性有待更广泛验证。