> A unified framework for agentic formal theorem proving in Lean 4. — 📄 Paper: OProver: A Unified Framework for Agentic Formal Theorem Proving (arXiv) — 📚 Collection: m-a-p/OProver — 📦 Dataset: m-a-p/OProofs OProver treats theorem proving as a multi-round refinement loop. Given a target theorem, the prover retrieves top-k compiler-verified proofs from a memory of prior proofs, generates a proof attempt, runs the Lean 4 compiler, and—on failure—revises the attempt using the compiler feedback in the next round. The same retrieval and feedback signals are baked into training, so the training-time interface matches the proving-time interaction. — State-of-the-art among open-weight whole-proof provers. OProver-32B attains the best Pass@32 on MiniF2F (93.3), ProverBench (58.2), and PutnamBench (11.3), and the second-best on MathOlympiad (22.8) and ProofNet (33.2). Even OProver-8B beats Goedel-Prover-V2-32B on all five benchmarks despite having 4× fewer parameters. — Agentic proving is in the policy, not bolted on. Retrieval, multi-turn compiler feedback, and iterative repair are all part of the trained policy. Ablations show feedback is the dominant driver: removing it costs OProver-32B…
Модальности:
Генерация текста
Области применения:
Диалог / чат
Задача: Генерация текста
Автор: m-a-p
Теги: qwen3, lean4, theorem-proving, formal-mathematics, agentic, retrieval-augmented, conversational, en
Лайков: 4 | Загрузок: 106
Описание основано на материалах HuggingFace. Перевод выполнен автоматически.
