Hugging Face Overview
BFS-Prover-V2-32B: Advanced Step-Level Theorem Prover
BFS-Prover-V2-32B is a 32.8 billion parameter model from ByteDance-Seed, specifically engineered for step-level theorem proving within the Lean4 formal verification system. It is built on the Qwen2.5-32B base model and introduces novel approaches to scale both training and inference for neural theorem proving.
Key Capabilities and Innovations
- Multi-stage Expert Iteration: Employs an adaptive tactic-level data filtering and periodic retraining framework to overcome performance plateaus during long-term post-training.
- Planner-Enhanced Multi-Agent Tree Search: Utilizes a hierarchical reasoning system to significantly scale performance during inference.
- State-of-the-Art Performance: Achieves 95.08% on the miniF2F test set (with planner) and 41.4% on the ProofNet test set, setting new benchmarks for step-level provers.
- Specialized Training Data: Trained on diverse sources including Mathlib (via LeanDojo), Lean-Github repositories, autoformalized NuminaMath datasets, and Goedel-Pset.
Usage and Integration
The model expects Lean4 tactic states as input, formatted with a ::: separator to trigger tactic generation. It is designed to integrate with systems like LLMLean for practical application in formal mathematics. The model's primary function is to generate appropriate tactics for given Lean4 states, aiding in automated proof construction.