OProver 是一个面向 Lean 4 的智能体形式定理证明统一框架，通过迭代训练（持续预训练 + 迭代后训练）结合已验证证明和编译器反馈来改进证明生成。其核心组件 OProofs 包含 177 万条 Lean 语句、686 万个编译器验证的证明及序列化轨迹。在五个基准测试中，OProver-32B 在 MiniF2F (93.3%)、ProverBench (58.2%) 和 PutnamBench (11.3%) 上取得最佳 Pass@32 成绩，并在 MathOlympiad (22.8%) 和 ProofNet (33.2%) 上排名第二，优于所有先前开源全证明证明器。
核心要点
- OProver 将智能体证明（agentic proving）集成到训练中，而不仅限于推理阶段，通过迭代修订失败证明尝试。
- 训练流程：持续预训练 → 迭代后训练，每轮运行智能体证明、索引新验证证明、使用修复轨迹作为 SFT 数据、用未解决难题进行强化学习。
- OProofs 数据集：来自公共 Lean 资源、大规模证明合成和智能体证明轨迹，含 177 万条语句、686 万个编译器验证证明及序列化轨迹。
- OProver-32B 在 MiniF2F 上 Pass@32 达 93.3%，ProverBench 58.2%，PutnamBench 11.3%，均为最佳。
- 在 MathOlympiad (22.8%) 和 ProofNet (33.2%) 上排名第二，整体表现优于所有先前开源全证明证明器。
正文
摘要
近期形式定理证明的进展受益于大规模证明生成和验证器感知训练，但智能体证明（agentic proving）很少被集成到证明器训练中，仅出现在推理阶段。我们提出 OProver，一个面向 Lean 4 的智能体形式定理证明统一框架，其中失败的证明尝试通过检索编译器验证的证明和 Lean 编译器反馈进行迭代修订。OProver 通过持续预训练后接迭代后训练进行训练：每轮迭代运行智能体证明，将新验证的证明索引到 OProofs 和检索记忆中，使用修复轨迹作为监督微调（SFT）数据，并使用未解决的难题进行强化学习（RL）。OProofs 基于公共 Lean 资源、大规模证明合成和智能体证明轨迹构建，包含 177 万条 Lean 语句、686 万个编译器验证的证明，以及序列化轨迹（含检索上下文、失败尝试、反馈和修复）。在五个基准测试中，OProver-32B 在 MiniF2F (93.3%)、ProverBench (58.2%) 和 PutnamBench (11.3%) 上取得最佳 Pass@32 成绩，在 MathOlympiad (22.8%) 和 ProofNet (33.2%) 上排名第二，其顶级排名数量超过任何先前开源全证明证明器。
延伸摘要
近期形式定理证明的进展受益于大规模证明生成和验证器感知训练，但智能体证明很少被集成到证明器训练中，仅出现在推理阶段。我们提出 OProver，一个面向 Lean 4 的智能体形式定理证明统一框架，其中失败的证明尝试通过检索编译器验证的证明和 Lean 编译器反馈进行迭代修订。OProver 通过持续预训练后接迭代后训练进行训练：每轮迭代运行智能体证明，将新验证的证明索引到 OProofs 和检索记忆中，使用修复轨迹作为 SFT 数据，并使用未解决的难题进行 RL。OProofs 基于公共 Lean 资源、大规模证明合成和智能体证明轨迹构建，包含 177 万条 Lean 语句、686 万个编译器验证的证明，以及序列化轨迹（含检索上下文、失败尝试、反馈和修复）。在五个基准测试中，OProver-32B 在 MiniF2F (93.3%)、ProverBench (58.2%) 和 PutnamBench (11.3%) 上取得最佳 Pass@32 成绩，在 MathOlympiad (22.8%) 和 ProofNet (33.2%) 上排名第二，其顶级排名数量超过任何先前开源全证明证明器。
关联概念
- Lean 4
- 形式定理证明
- 智能体证明
- 编译器反馈
- 强化学习
- 监督微调
- 持续预训练
- 证明合成
可操作项
可动手实践：1. 访问 GitHub 仓库 https://github.com/multimodal-art-projection/OProver 获取代码和数据集。2. 尝试使用 OProver 框架在 Lean 4 中运行定理证明任务。3. 参考 OProofs 数据集构建自己的证明检索系统。4. 基于 OProver 的训练流程（持续预训练 + 迭代后训练）复现或改进证明器。
原文: OProver: A Unified Framework for Agentic Formal Theorem Proving
自动加工于 2026-05-20 11:28