introvoyz042/OProver-32B
OProver-32B by m-a-p is a 32 billion parameter model designed for agentic formal theorem proving in Lean 4, featuring a 32768 token context length. It excels by treating theorem proving as a multi-round refinement loop, incorporating retrieval, compiler feedback, and iterative repair directly into its trained policy. This model achieves state-of-the-art performance among open-weight whole-proof provers on benchmarks like MiniF2F (93.3 Pass@32) and ProverBench (58.2 Pass@32). It is primarily optimized for generating and refining formal proofs in Lean 4.
Loading preview...
OProver-32B: Agentic Formal Theorem Proving
OProver-32B, developed by m-a-p, is a 32 billion parameter model specifically engineered for agentic formal theorem proving within the Lean 4 environment. It distinguishes itself by integrating a multi-round refinement loop directly into its policy, where it retrieves prior proofs, generates attempts, processes Lean 4 compiler feedback, and iteratively revises proofs.
Key Capabilities
- State-of-the-art Performance: Achieves leading results among open-weight whole-proof provers, including 93.3 Pass@32 on MiniF2F, 58.2 on ProverBench, and 11.3 on PutnamBench. It also outperforms Goedel-Prover-V2-32B across multiple benchmarks.
- Integrated Agentic Proving: Retrieval, multi-turn compiler feedback, and iterative repair are core components of its trained policy, not external additions. Ablation studies confirm the significant impact of feedback and retrieval on its performance.
- Co-evolving Prover and Corpus: The model's performance improves through iterative post-training rounds, where agentic rollouts generate verified proofs that are added to the OProofs dataset, and repair trajectories become supervised fine-tuning (SFT) data.
- Extensive Training: Undergoes continued pretraining on a 65B-token mixture including formal Lean, code, mathematics, and long-CoT data, followed by iterative SFT and GSPO RL.
Good For
- Automated Theorem Proving: Ideal for generating and verifying formal mathematical proofs in Lean 4.
- Research in AI for Mathematics: Useful for researchers exploring agentic AI systems, reinforcement learning in theorem proving, and the co-evolution of models and datasets.
- Lean 4 Development: Can assist in the creation and validation of Lean 4 code and formalizations.