OProver 深度拆解：当大模型学会"试错-反思-修正"，形式化定理证明进入智能体时代

论文：OProver: A Unified Framework for Agentic Formal Theorem Proving
作者：M-A-P
链接：https://arxiv.org/abs/2605.17283

一、问题的本质：训练与推理的"精神分裂"

形式化定理证明（Formal Theorem Proving）是 AI 数学能力的天花板。Lean 4、Coq 这些证明助手要求每一步都严格符合逻辑规则，任何一个类型不匹配、未知标识符、策略应用失败，都会被编译器无情驳回。

现有方法的共同困境：训练时学的是"正确答案"，推理时却要处理"错误反馈"。

就像一个人只背过标准答案，从没练过错题分析——上了考场遇到不会的，只能干瞪眼。现有方法虽然会在推理时加入检索（RAG）和编译器反馈（错误信息），但这些能力只是"外挂"，模型本身从未在训练数据中学过"如何读懂错误、如何修正"。

"What is missing is therefore not more verified proofs, but corpora that explicitly preserve how proofs are constructed, fail, and get repaired."
—— 缺失的不是更多验证通过的证明，而是显式保留证明如何构建、失败和修复的语料。

二、OProver 的解法：把"试错过程"变成训练数据

OProver 的核心洞察极其简洁：如果编译器反馈是推理时的关键信号，为什么不把它也纳入训练？

不是让模型"背答案"，而是让模型"学解题过程"——包括那些失败的尝试、编译器的报错、以及基于报错进行的修正。

架构全景：一个多轮精炼循环

目标定理 s
    ↓
检索 top-k 相似证明 R_t（动态记忆库）
    ↓
上一轮尝试 p_{t-1} + 编译器反馈 f_{t-1}
    ↓
策略 π 生成新一轮证明 p_t
    ↓
Lean 4 编译器验证
    ↓
通过？→ 输出最终证明
不通过？→ 回到开头，继续迭代（最多 T 轮）

关键设计：紧凑交互状态

这里最精妙的是"仅保留最近一轮"。直觉上应该保留完整历史，但实验证明：局部修正信号最相关。同时，这也保证了训练时和推理时的输入格式完全一致——训练-推理一致性是模型泛化的关键。

三、OProofs：一个"会犯错"的数据集

现有数据集（如 LeanDojo、Goedel-Prover）只保留验证通过的证明。OProver 团队构建的 OProofs 是反直觉的：它专门收集失败和修复的过程。

规模：

• 177 万条 Lean 语句
• 686 万条编译器验证证明
• 107 万条智能体证明轨迹（含失败→反馈→修复的完整链条）

这意味着模型训练时，不仅看到"正确答案长什么样"，还看到"常见的错误类型有哪些"、"编译器报错通常意味着什么"、"基于报错应该往哪个方向修正"。

四、两阶段训练：从"领域适应"到"协同进化"

阶段一：持续预训练（CPT）

用 65B token 的混合数据做领域适应：

• 30% Lean 形式化数据
• 20% 代码（OpenCoder）
• 40% 数学（Nemotron-Math-4-Plus）
• 10% 长思维链（ProLong-64K）

获得基础模型 OProver-Base。

阶段二：迭代后训练（K 轮循环）—— 这是精髓

对每轮 k = 0,1,2,...:
    
    1. 用当前证明器 π_k 在定理池上多轮证明，动态检索，编译器验证
    
    2. 新验证的证明 P^+_k → 加入数据集 D_{k+1}
    
    3. 提取修复样本：
       (目标定理, 检索上下文, 上轮尝试, 编译器反馈) → 修正证明
       → 做 SFT 训练
    
    4. 选择难题 → 做 RL 训练（GSPO，Group Sequence Policy Optimization）
       - 每定理采样 n 条多轮轨迹
       - 轮级奖励：验证通过则高分，否则低分
       - 同一定理的 n×R 轮池化为单组做相对优势归一化
    
    5. 更新数据集 D_{k+1} = D_k ∪ P^+_k
    
    6. 更新检索记忆库 M_{k+1} = Index(D_{k+1})

这个循环的核心是正反馈：

• 模型越强 → 验证通过的证明越多 → 检索记忆库越丰富 → 后续证明有更多参考 → 模型更强

这是"证明器"和"语料库"的共同进化，不是静态数据喂静态模型。

五、实验结果：32B 密集模型击败 560B MoE

主结果（Pass@32）

注意：LongCat-Flash-Prover 是 560B MoE（27B 激活参数），总参数量是 OProver-32B 的 17 倍。OProver 在 3/5 基准上击败它，参数效率碾压。

迭代后训练效果（消融）

每轮都在提升，没有饱和——协同演化循环有效。

消融：编译器反馈 vs 检索

编译器反馈贡献约 75-80% 的增益，检索贡献约 20-25%。这意味着：读懂错误、学会修正，比"查资料"更重要。

六、深层洞察：为什么 OProver 有效？

1. 关闭了"训练-推理鸿沟"

传统方法：训练时只优化"生成正确证明"，推理时却要"读错误信息→修正→再试"。这是两个不同的任务分布。

OProver：训练时就让模型学习"(定理, 检索, 错误尝试, 编译器反馈) → 修正证明"，推理时完全一致。

2. 反馈是"过程监督"，不是"结果监督"

现有方法的过程监督（如 PRM）通常需要人工标注每一步是否正确。OProver 的巧妙之处：编译器就是免费的、自动的过程监督器。每一步尝试都能拿到编译器的明确反馈（通过/不通过+具体错误），不需要人工标注。

3. 协同演化打破了数据瓶颈

形式化证明的数据瓶颈是公认难题。OProver 的解决方式不是"找更多数据"，而是"让模型自己生产数据"——新验证的证明加入检索库，修复轨迹加入训练集，形成自我增强循环。

七、局限性与真正的问题

绝对性能仍低

PutnamBench 仅 11.3%，意味着最难的竞赛题 89% 仍做不出来。这不是 OProver 的错，是整个领域的现状。

测试时扩展的递减回报

预算从 128 → 256，增益仅 0.5-0.9 点。说明在最难问题上，"多试几次"的天花板已现，需要根本性策略创新。

最难问题的根本困境

"当单链成功率极低时（5-11%），深度迭代不如广度探索。"

迭代修复的前提是"接近正确"——当你离正确答案很远时，局部修正是无效的。最难的问题可能需要从头重构策略而非基于错误微调。

八、定位与意义

OProver 处于两个范式的交汇点：

• 全证明生成（端到端，一次出完整证明）
• 智能体证明（多轮交互，试错迭代）

它保留了前者的端到端优势（避免逐步策略的搜索爆炸），引入了后者的交互能力（突破单轮生成的天花板）。

关键创新不是"多轮迭代"这个想法本身（之前也有人做），而是将多轮迭代训练进策略，而非仅作为推理时的包装——并配套了完整的数据基础设施（OProofs）和训练流程（协同演化）。

32B 密集模型击败 560B MoE，说明在形式化定理证明这个领域，算法设计比参数规模更重要。这是值得整个行业深思的信号。

参考文献

• OProver: https://arxiv.org/abs/2605.17283
• M-A-P 团队：https://github.com/multimodal-art-projection
• Goedel-Prover-V2: https://arxiv.org/abs/2502.07052
• LongCat-Flash-Prover: https://arxiv.org/abs/2502.1358
• DeepSeek-Prover-V2: https://arxiv.org/abs/2504.07028

#OProver #形式化定理证明 #Lean4 #数学推理 #智能体 #AI论文 #M-A-P #小凯