OProver让数学定理证明自动迭代修正，提升准确率。
OProver: A Unified Framework for Agentic Formal Theorem Proving
- 用检索编译验证的证明和编译反馈，自动修复失败证明
- 在5个基准上最高达93.3%的通过率，优于现有开源模型
- 适合需要高精度自动证明的研究者和工具开发者
近期形式化定理证明进展得益于大规模证明生成与验证器感知训练，但代理式证明仅在推理时出现，未融入训练。我们提出OProver，一个面向Lean 4的统一代理式形式化证明框架，通过检索编译验证的证明和利用Lean编译器反馈，迭代修正失败的证明尝试。OProver采用持续预训练后接迭代微调：每次迭代运行代理式证明，将新验证的证明存入OProofs与检索记忆库，用修复轨迹作为监督微调数据，未解决难题用于强化学习。OProofs由公开Lean资源、大规模证明合成及代理式证明轨迹构建，包含177万条Lean命题、686万条编译验证的证明，以及包含检索上下文、失败尝试、反馈与修复的序列化轨迹。在五个基准测试中，OProver-32B在MiniF2F（Pass@32: 93.3%）、ProverBench（58.2%）和PutnamBench（11.3%）取得最佳表现，在MathOlympiad（22.8%）和ProofNet（33.2%）排名第二，超越所有先前开源全证明生成器。
原文摘要 · Abstract (English)
Recent progress in formal theorem proving has benefited from large-scale proof generation and verifier-aware training, but agentic proving is rarely integrated into prover training, appearing only at inference time. We present OProver, a unified framework for agentic formal theorem proving in Lean 4, in which failed proof attempts are iteratively revised using retrieved compiler verified proofs and Lean compiler feedback. OProver is trained through continued pretraining followed by iterative post-training: each iteration runs agentic proving, indexes newly verified proofs into OProofs and the retrieval memory, uses repair trajectories as SFT data, and uses unresolved hard cases for RL. OProofs is built from public Lean resources, large-scale proof synthesis, and agentic proving traces, containing 1.77M Lean statements, 6.86M compiler-verified proofs, and serialized trajectories with retrieved context, failed attempts, feedback, and repairs. Across five benchmarks, OProver-32B attains the best Pass@32 on MiniF2F (93.3%), ProverBench (58.2%), and PutnamBench (11.3%), and ranks second on MathOlympiad (22.8%) and ProofNet (33.2%) more top placements than any prior open-weight whole-proof prover.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。