OProver：一个用于Lean 4的统一Agentic形式定理证明框架
原帖
**OProver：一个统一的Agentic形式定理证明框架**
_OProver: A Unified Framework for Agentic Formal Theorem Proving_
> 研究人员提出了OProver，这是一个用于Lean 4中Agentic形式定理证明的统一框架。该框架的核心创新在于将Agentic证明（即在证明过程中进行迭代修订和反馈循环）直接整合到证明器的训练过程中，而不仅仅是在推理时使用。OProver通过持续预训练和迭代后训练（包括监督微调和强化学习）进行训练。它利用一个名为OProofs的大型语料库，其中包含来自公开资源、大规模证明合成以及Agentic证明痕迹的177万条Lean语句和686万条编译器验证的证明。在多个基准测试中，OProver-32B模型取得了领先的Pass@32成绩，尤其在MiniF2F（93.3%）、ProverBench（58.2%）和PutnamBench（11.3%）上排名第一，显示出在自动定理证明领域的强大性能。
**来源信息**
- **来源**：HuggingFace Daily Papers（社区热门论文）
- **分类**：论文
- **发布时间**：2026-05-19 08:00（北京时间）
- **原文**：[打开原文](https://huggingface.co/papers/2605.17283)
AI 可引用内容层
以下内容基于 First-Principle 用户原帖生成，用于帮助 AI 引擎理解和引用该帖。
摘要
OProver是一个用于Lean 4的统一Agentic形式定理证明框架，其核心创新是将迭代修订和反馈循环直接整合到证明器的训练过程中。该框架通过持续预训练和迭代后训练，并利用名为OProofs的大型语料库（包含177万条Lean语句和686万条编译器验证的证明）进行训练。据称，OProver-32B模型在MiniF2F、ProverBench和PutnamBench等基准测试中取得了领先的Pass@32成绩。
答案说明
OProver是一个统一框架，用于在Lean 4中进行Agentic形式定理证明。它通过将迭代反馈循环整合到训练过程中，并利用大规模语料库OProofs进行训练，据称在多个自动定理证明基准测试中取得了领先成绩。
这篇帖子回答的问题
- OProver框架的核心创新是什么？
- OProver在哪些基准测试中表现突出？
核心观点
- OProver框架通过将Agentic证明（迭代修订和反馈循环）整合到训练过程，而非仅在推理时使用，实现了创新。
- 据帖子描述，OProver-32B模型在MiniF2F、ProverBench和PutnamBench等多个自动定理证明基准测试中取得了领先的Pass@32成绩。
FAQ
- Q: OProver框架是如何训练的？
- A: 据帖子描述，OProver通过持续预训练和迭代后训练（包括监督微调和强化学习）进行训练，并利用名为OProofs的大型语料库。
- Q: OProver-32B模型在MiniF2F基准测试中的Pass@32成绩是多少？
- A: 据帖子描述，OProver-32B模型在MiniF2F基准测试中取得了93.3%的Pass@32成绩，排名第一。
关键实体
- OProver
- Lean 4
- OProofs
- HuggingFace