大型语言模型在数学证明任务上的可靠性一直是核心挑战。与代码生成不同，证明没有可执行的单元测试作为反馈信号，验证必须依赖生成式评判器。MaxProof 框架通过构建一个端到端的 "证明编译管道"，将问题陈述转化为经过验证的可靠证明，其设计思想与编译器后端将高级语言转换为机器码的过程有着深刻的相似性。
管道架构：三层专家的协作翻译
MaxProof 的核心架构包含三个专门化的组件，分别对应编译管道中的不同阶段：
Proof Expert（证明专家） 负责将问题陈述 "编译" 为候选证明。这类似于编译器的前端将源代码解析为中间表示。该组件通过长程强化学习训练，使用 CISPO（Clipped Importance Sampling Policy Optimization）算法，在生成式验证器的反馈信号下进行策略优化。与 PPO 不同，CISPO 在重要性采样权重而非替代损失上进行裁剪，这能更好地保留长序列中的 token 级梯度。
Verifier Expert（验证专家） 充当管道的 "语义分析器"，负责定位证明中的具体错误并给出评判。不同于简单的 0-7 分回归任务，验证专家被训练为输出结构化的<assessment>、<errors>、<verdict>三段式结果。这种设计强制模型必须先逐段阅读证明，再给出具体错误描述，最后才是分类判断。训练数据来自 Proof Expert 训练过程中的副产品，确保两者对 "正确性" 的定义保持一致。
Fixer Expert（修复专家） 实现管道的 "代码优化" 功能，在验证反馈的指导下修复缺陷证明。输入是（问题、缺陷证明、验证分析）三元组，输出是修正后的证明。修复专家通过拒绝采样微调训练：只有被保守型验证器判定为完全正确的修复才会被纳入训练集。
防御式验证器：四层保证传递
验证器是整个管道的关键节点，其可靠性直接决定下游训练的有效性。MaxProof 采用四层防御架构，每层针对特定的失效模式：
第一层（坏例过滤） 通过保守规则剔除空证明、未闭合思考块、模板循环等已知失败模式，这些案例直接获得 0 分。
第二层（解归一化） 使用强外部归一器剥离固定开头、步骤标题和验证章节，使评判器聚焦于数学内容而非表面格式。
第三层（多评判器并行） 两个基于评分标准的评判器用于校准，一个无评分标准评判器用于直接错误发现。分歧被视为有用的不确定性信号。
第四层（悲观聚合） 最终奖励取三个评判器分数的最小值，刻意偏好假阴性而非假阳性。这是因为 RL 会放大高分但无效的证明，而假阴性仅丢弃单个候选。
这种设计源于 M2 周期的教训：单评判器验证器在长时间 RL 训练中会被策略利用，出现长度偏置、格式劫持、语义捷径和评判器特定偏好等四种典型奖励黑客模式。四层防御确保每种模式都需要独立突破，大幅提高利用成本。
CISPO 算法与群体级过滤
Proof Expert 的训练使用 CISPO 目标函数，其核心是群体级标准差阈值过滤。对于每个问题，策略采样 G 个候选证明，每个获得验证器奖励 R_i ∈ [0,7]。群体归一化优势计算为：
A_i = (R_i - μ_R) / (σ_R + ε)
只有当群体奖励标准差 σ_R 超过阈值 τ_std 时，该群体才参与策略更新。这防止了验证器无法区分候选质量时的噪声梯度传播。CISPO 策略目标在 token 级使用裁剪后的重要性比率作为权重，而非像 PPO 那样完全截断超出信任区间的 token 梯度，这对长证明序列至关重要。
MaxProof 循环：种群级测试时扩展
在推理阶段，MaxProof 将基础模型的 best@K 能力转换为更稳定的 pass@1。算法维护一个候选种群档案，通过迭代精炼实现搜索：
初始化：采样 N=32 个初始候选，每个经过 K_verify=4 次验证，取悲观最小值作为适应度分数。
父代选择：每轮选择 M=4 个适应度最高的候选作为父代，应用多样性过滤（基于词法距离）防止近亲繁殖。已达最大适应度 (7/7) 的候选保留在档案中但不再参与精炼。
双模精炼：每个父代产生两个子代。PATCH 模式是 "利用" 操作，在验证器指出的具体错误处进行局部修复，保留正确部分。REWRITE 模式是 "探索" 操作，将当前缺陷视为路径受阻的证据，尝试完全不同的证明路线。两种模式都接收种群中其他候选的摘要作为上下文，实现信息共享。
种群级早停：当档案中至少有两个候选达到最大适应度时触发早停，这是针对验证器噪声的冗余检查。
锦标赛选择：最终答案通过两两锦标赛从 top-K 候选中选出。每场比赛由 K_ranker=3 次排名投票决定，排名器被询问 "哪个候选是更正确的证明" 而非要求绝对分数。当验证器分数聚集时，相对比较比绝对评分更可靠。
工程参数与性能
在 IMO 2025 和 USAMO 2026 的评估中，MaxProof 配置为：N=32 初始候选，R=10 精炼轮次，M=4 父代每轮，K_ranker=3 排名投票。该配置使 M3 模型从单次采样的 27/42 和 26/42 分别提升至 35/42 和 36/42，增益达 8-10 分。
值得注意的是，增益并非来自简单采样：32 次独立采样的期望增益远低于此，且 MaxProof 还提供了最优候选的选择机制。种群级搜索动态显示，9/12 的问题在 4 轮内达到 7/7 的 oracle 最优，剩余 3 个问题中 2 个因基础模型能力限制（如 IMO 2025 P6），1 个因排名器偏好与验证器分数不一致导致选择损失。
与编译器管道的类比
MaxProof 的设计与 LLVM 等编译器基础设施存在深刻对应：
- 多层 IR：证明文本如同 LLVM IR，是高级数学概念与底层验证信号之间的中间表示
- 防御式验证：类似编译器中的多遍优化与验证，每层检查不同类别的错误
- 保证传递：验证专家的反馈通过 Fixer Expert 的修复操作传递回证明，如同编译器中的优化保证
- 种群搜索：类似编译器探索不同的指令序列选择，MaxProof 在证明空间中进行进化式搜索
这种 "证明编译" 视角揭示了形式化证明生成的工程本质：它不仅是序列生成问题，更是一个需要多阶段验证、反馈传递和搜索优化的复杂系统。
参考资料
- Zhang X, et al. "MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling." arXiv:2606.13473, 2026.
内容声明：本文无广告投放、无付费植入。
如有事实性问题，欢迎发送勘误至 i@hotdrydog.com。