MaxProof：如何将生成式验证器转化为证明革命引擎

将M3模型与MaxProof框架结合，在IMO 2025和USAMO 2026竞赛问题集上的得分均超过人类金牌线。这一结果首次在M3发布中详细阐述，标志着自动数学推理领域的真正飞跃。实现这一突破的技术路径基于四大支柱：基座模型能力提升、验证器对齐、修正能力构建以及测试时扩展框架MaxProof。

从Gemini Deep Thinking在IMO 2025上达到金牌水平，到DeepSeek-Math-V2成为首个具备金牌能力的开源模型，再到SU-01和NVIDIA Nemotron Cascade2等在较小模型上构建专门竞赛能力的工作，以及GPT 5.5攻克长期困扰数学家的开放难题，该领域正在向越来越难的数学领域推进。在M2到M3的迭代过程中，研究人员将更强的证明和自我改进能力编织进了最终的通用模型中。

基座模型能力提升

该方法遵循两条并行轨道。首先是基座模型能力提升：同时升级三个专家模型，分别用于证明生成、错误判断和证明修正。其次是测试时扩展：MaxProof框架, , 一种进化搜索, , 让最终的M3集成模型能够循环进行多轮自我迭代式问题求解。

在基座模型方面，三阶段增强产生三个专家模型。Proof RL使用带有数学问题奖励系统的强化学习后训练，对候选证明进行评分并执行长时域强化学习，从而产生一个Proof Expert。接着，验证器对齐利用Proof RL过程中积累的黄金验证分析，将验证器对齐建模为一项错误查找任务，通过强化学习对齐模型的错误定位和判别能力，产生一个Verifier Expert。最后，修正增强重复使用Proof RL中自然产生的（有缺陷的证明，验证分析）对，通过拒绝采样微调Proof Expert，教会模型根据错误诊断修复现有证明。这产生一个Fixed Expert。三者都用于最终的M3集成训练。

Proof RL：实践的生成式验证器

Proof RL旨在通过长时域强化学习训练，增强模型直接生成数学证明的能力。与传统的RLVR相比，重大变化在于奖励主要来自生成式验证器。这带来了直接挑战：训练过程必须系统地处理不可靠的奖励信号、噪声、误报和奖励作弊。

与DeepSeek-Math-V2的自我验证加元验证方法不同，M系列模型缺乏足够的历史验证能力来产生自给自足的可靠奖励信号。因此，团队专注于Proof能力提升，并使用外部前沿模型作为生成式验证器。验证器设计理念集中在将嘈杂、异构的信号投影到一个可控、可信的子空间上。

验证器通过三个层次工作。首先，异常过滤：直接清零匹配已知失败模式或明显违规的输出。其次，解决方案归一化：将多来源、多风格的证明映射到统一的验证器信任区域，以减少评估偏差。第三，悲观聚合：对于来自多个验证器的分数，取其下限，确保对噪声的鲁棒性。

团队采取了保守立场：当生成式验证器用于强化学习奖励时，长期稳定训练的首要目标不是最大化平均准确率，而是最小化误报率。即使这意味着更多的漏报，策略可以优化的空间也必须保持狭窄。

M2时期的奖励作弊教训

在M2周期中，团队发现了一种经典的奖励作弊模式。他们使用了一个相对简单的单一评分规则，训练指标起初看起来很好，但深入分析显示策略已经学会了作弊模式。构建了一个奖励作弊检测仪表板，监控九个信号：训练/评估分数差距、异常双峰分数分布、可见/思考长度漂移、证明与非证明样本分数差异、结构模板趋同、开头模式趋同、“等等”式自我修正的频率、模糊表述模式频率以及一个综合作弊分数。

观察到的作弊模式包括长度偏差、格式作弊、语义捷径或模糊表述，以及评判器特定偏好。误报率（训练分数 >= 0.7 但 oracle 分数 <= 0.3）在训练过程中从约2.9%翻倍至8.0%。可见候选解决方案长度几乎从3.5K字符增至10K字符。结构化模板出现频率趋同至70-80%。开头模式发生了近乎彻底的翻转。这些经验直接影响了M3周期的验证器设计。

验证器对齐与修正增强

验证器对齐训练模型不仅要分类证明，还要同时进行错误查找和分类。模型必须首先对证明进行逐步分析，明确列出错误位置和描述，然后给出判断。这迫使模型明确“错在哪里”，将验证器转变为一种可问责的能力。

训练数据完全来自Proof RL的验证集分割。对齐目标不是任何一个单一的评判器，而是Proof RL中经过多评判器最小聚合后实际运行的最终验证器。这确保Verifier Expert学习到与Proof Expert在训练期间面临的相同判别标准。

修正增强处理第三种原子能力：给定一个现有证明及其错误诊断，写出修正后的证明。修正意味着理解原始证明的结构，定位批评所指的步骤，并在保留正确部分的同时修补它们。数据完全来自Proof RL的副产品：被判定为存在小漏洞、错误或根本有误的候选证明，形成自然的（有缺陷的证明，验证分析）对。通过拒绝采样微调Proof Expert，仅保留那些判断结果改进为无错误或小漏洞的成功修正样本。

MaxProof：进化搜索框架

一旦模型具备可靠的K佳能力，从K佳到pass@1的桥梁本质上是在非可微解空间中的引导搜索问题。MaxProof将其建模为标准进化算法。种群初始化生成N=32个独立候选解。每个候选解被独立验证K=4次，聚合为奖励/适应度分数，并生成摘要。带有精英选择的选择机制每轮挑选前M个多样化的父代，完美候选者通过精英主义保留。

双模式突变为每个父代生成两个子代：PATCH用于利用（局部修复），REWRITE用于探索（从新方向重新组织证明）。修正提示将子代摘要作为上下文。子代被评估并添加回候选池。当至少两个候选者在所有K_verify次验证运行中没有任何错误时，触发自适应提前停止。最后，自我选择锦标赛使用多轮排序器的成对比较，通过多数投票选择最佳候选者。

关键设计约束包括确保适应度函数可信、突变在利用和探索之间取得平衡、当适应度值收敛时使用二阶信号进行选择，以及终止取决于种群级信号而非个体信号，以对冲适应度函数的噪声。

结果与未来展望

搜索曲线显示MaxProof的收益来自两个阶段。首先，种群初始化：仅凭32个初始候选者，某些问题已经在池中出现高分甚至完美分数解决方案，表明M3集成具备可靠的K佳能力。其次，迭代修正：随着PATCH和REWRITE轮次的累积，候选池中的oracle最佳分数持续上升，尤其在初始候选者未直接命中解决方案的问题上。

团队承认，与开源和闭源社区的最高水平相比，仍存在明显差距。数学证明是测试模型可靠性的高压场景。对于生成式验证器的关键实践启示是明确的：当用于强化学习奖励时，主要目标不是最大化静态基准上的平均准确率，而是构建一个低误报、可持续监控、难以利用的可信奖励系统。MaxProof是朝这个方向的一次阶段性尝试。