m-a-p/OProver-32B
m-a-p/OProver-32B is a 32 billion parameter model developed by m-a-p, designed as a unified framework for agentic formal theorem proving in Lean 4. It excels at multi-round refinement loops, utilizing retrieval of prior proofs and iterative revision based on Lean 4 compiler feedback. This model achieves state-of-the-art performance among open-weight whole-proof provers on benchmarks like MiniF2F, ProverBench, and PutnamBench.
Loading preview...
OProver-32B: Agentic Formal Theorem Proving
OProver-32B is a 32 billion parameter model developed by m-a-p, specifically engineered for agentic formal theorem proving within the Lean 4 environment. It operates on a multi-round refinement loop, where it retrieves compiler-verified proofs, generates proof attempts, and iteratively revises them using Lean 4 compiler feedback. This agentic approach, including retrieval and feedback signals, is deeply integrated into its training policy.
Key Capabilities & Differentiators
- State-of-the-art Performance: OProver-32B achieves leading Pass@32 scores on several Lean 4 benchmarks, including 93.3 on MiniF2F, 58.2 on ProverBench, and 11.3 on PutnamBench. It also secures second-best results on MathOlympiad (22.8) and ProofNet (33.2).
- Integrated Agentic Proving: Unlike models where agentic features are bolted on, OProver-32B's policy inherently includes retrieval, multi-turn compiler feedback, and iterative repair. Ablation studies show compiler feedback is a dominant driver of its performance.
- Co-evolving Prover and Corpus: The model's development involves an iterative process where agentic rollouts generate new verified proofs, which are then added to the OProofs dataset and re-indexed for retrieval. Repair trajectories also contribute to SFT data, and unresolved cases provide RL signals, leading to monotonic performance growth across training rounds.
- Comprehensive Training: The model undergoes continued pretraining on a 65B-token mixture of formal Lean, code, mathematics, and long-CoT data, followed by iterative post-training involving agentic proving, Supervised Fine-Tuning (SFT), and GSPO Reinforcement Learning (RL).
When to Use This Model
OProver-32B is ideal for researchers and developers focused on automated formal theorem proving in Lean 4. Its strengths lie in its ability to generate and refine proofs iteratively, leveraging compiler feedback and a rich corpus of prior proofs. It is particularly well-suited for complex mathematical and logical reasoning tasks requiring high accuracy and verification.