OProver 是一个面向 Lean 4 的智能体形式定理证明统一框架，通过迭代训练结合已验证证明和编译器反馈来改进证明生成。该框架采用持续预训练和迭代后训练，每次迭代运行智能体证明、将新验证的证明索引到 OProofs 和检索记忆、使用修复轨迹作为 SFT 数据、使用未解决的困难案例进行强化学习。OProofs 包含 177 万条 Lean 语句、686 万个编译器验证的证明以及序列化轨迹。在五个基准测试中，OProver-32B 在 MiniF2F (93.3%)、ProverBench (58.2%) 和 PutnamBench (11.3%) 上取得最佳 Pass@32 成绩，在 MathOlympiad (22.8%) 和 ProofNet (33.2%) 上排名第二，整体表现优于任何先前的开源全证明证明器。
核心要点
- OProver 是首个将智能体证明过程集成到训练中的统一框架，而不仅限于推理时使用。
- 采用持续预训练 + 迭代后训练策略，每次迭代包含智能体证明、索引、SFT 和强化学习。
- OProofs 数据集包含 177 万条 Lean 语句、686 万个编译器验证的证明和序列化修复轨迹。
- OProver-32B 在 MiniF2F 上达到 93.3% Pass@32，在 ProverBench 上 58.2%，在 PutnamBench 上 11.3%。
- 在 MathOlympiad 和 ProofNet 上排名第二，整体开源全证明证明器中表现最优。
正文
摘要
OProver 是一个面向 Lean 4 的智能体形式定理证明统一框架，通过迭代训练结合已验证证明和编译器反馈来改进证明生成。
引言
形式定理证明的最新进展得益于大规模证明生成和验证器感知训练，但智能体证明很少被集成到证明器训练中，仅在推理时出现。本文提出 OProver，一个面向 Lean 4 的智能体形式定理证明统一框架，其中失败的证明尝试会使用检索到的编译器验证证明和 Lean 编译器反馈进行迭代修正。
方法
OProver 通过持续预训练和迭代后训练进行训练：每次迭代运行智能体证明，将新验证的证明索引到 OProofs 和检索记忆，使用修复轨迹作为监督微调（SFT）数据，并使用未解决的困难案例进行强化学习（RL）。
数据集
OProofs 由公开的 Lean 资源、大规模证明合成和智能体证明轨迹构建而成，包含 177 万条 Lean 语句、686 万个编译器验证的证明，以及序列化轨迹，其中包含检索到的上下文、失败尝试、反馈和修复。
实验结果
在五个基准测试中，OProver-32B 取得了以下 Pass@32 成绩： - MiniF2F: 93.3%（最佳） - ProverBench: 58.2%（最佳） - PutnamBench: 11.3%（最佳） - MathOlympiad: 22.8%（第二） - ProofNet: 33.2%（第二）
整体上，OProver 在更多基准测试中取得最高排名，优于任何先前的开源全证明证明器。
关联概念
- 形式定理证明
- Lean 4
- 智能体系统
- 强化学习
- 监督微调
- 编译器验证
可操作项
可访问 GitHub 仓库 (https://github.com/multimodal-art-projection/OProver) 获取代码和数据集，尝试复现 OProver 的训练流程，或使用 OProofs 数据集进行自己的证明生成实验。
原文: OProver: A Unified Framework for Agentic Formal Theorem Proving
自动加工于 2026-05-20 08:06