论文页面 - OProver：统一智能体式形式化定理证明框架

来源：https://huggingface.co/papers/2605.17283

摘要

OProver 是一个面向 Lean 4 的统一智能体式形式化定理证明框架，通过迭代训练、验证过的证明与编译器反馈，显著提升了证明生成能力。

近年来，形式化定理证明取得了长足进步，这得益于大规模证明生成（https://huggingface.co/papers?q=proof%20generation）与验证器感知训练（https://huggingface.co/papers?q=verifier-aware%20training）的推动。然而，智能体式证明很少被整合到证明器训练中，通常仅在推理时出现。我们提出 OProver——一个统一的 Lean 4（https://huggingface.co/papers?q=Lean%204）智能体式形式化定理证明（https://huggingface.co/papers?q=agentic%20formal%20theorem%20proving）框架，在该框架中，失败的证明尝试会利用检索到的编译器验证证明及 Lean 编译器反馈进行迭代修正。OProver 的训练包括持续预训练（https://huggingface.co/papers?q=continued%20pretraining）以及后续的迭代后训练（https://huggingface.co/papers?q=iterative%20post-training）：每次迭代执行智能体式证明，将新验证的证明索引至 OProofs 与检索记忆，将修复轨迹用作 SFT 数据（https://huggingface.co/papers?q=SFT%20data），并对未解决的难题进行强化学习。OProofs 由公开的 Lean 资源、大规模证明合成（https://huggingface.co/papers?q=proof%20synthesis）以及智能体式证明轨迹构建而成，包含 177 万条 Lean 语句、686 万条编译器验证证明（https://huggingface.co/papers?q=compiler-verified%20proofs）以及序列化轨迹（含检索上下文、失败尝试、反馈与修复）。在五个基准测试中，OProver-32B 在 MiniF2F（93.3%）、ProverBench（58.2%）和 PutnamBench（11.3%）上取得了最佳 Pass@32 成绩，在 MathOlympiad（22.8%）和 ProofNet（33.2%）上排名第二，且其顶级排名数量超过以往任何开源全证明证明器。

查看 arXiv 页面（https://arxiv.org/abs/2605.17283）查看 PDF（https://arxiv.org/pdf/2605.17283）GitHub1（https://github.com/multimodal-art-projection/OProver）添加到收藏（https://huggingface.co/login?next=%2Fpapers%2F2605.17283）

在您的智能体中获取此论文：

hf papers read 2605.17283

没有最新的 CLI？curl -LsSf https://hf.co/cli/install.sh | bash

引用本论文的模型0

没有模型链接本论文

请在模型 README.md 中引用 arxiv.org/abs/2605.17283，以从本页面链接模型。

引用本论文的数据集0

没有数据集链接本论文

请在数据集 README.md 中引用 arxiv.org/abs/2605.17283，以从本页面链接数据集。

引用本论文的 Spaces0

没有 Space 链接本论文

请在 Space README.md 中引用 arxiv.org/abs/2605.17283，以从本页面链接 Space。

包含本论文的收藏集1