ByteDance-Seed/BFS-Prover-V2-7B
BFS-Prover-V2-7B by ByteDance-Seed is a 7.6 billion parameter step-level theorem proving system for Lean4, built upon the Qwen2.5-Math-7B base model. It utilizes a multi-stage expert iteration framework and best-first tree search for training, and is designed to generate Lean4 tactics from given tactic states. This model achieves strong performance on theorem proving benchmarks like miniF2F, making it suitable for automated theorem proving and formal verification tasks.
Loading preview...
BFS-Prover-V2-7B: Advanced Step-Level Theorem Prover
BFS-Prover-V2-7B is a 7.6 billion parameter model developed by ByteDance-Seed, specifically engineered for step-level theorem proving within the Lean4 formal verification system. It is based on the Qwen2.5-Math-7B architecture 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 scale performance during inference.
- State-of-the-Art Performance: Achieves 82.4% on the miniF2F-test benchmark, setting a new standard 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 Application
This model is designed to generate Lean4 tactics given a specific tactic state. Users provide an input in the format "{state}:::", and the model outputs the corresponding tactic. This makes BFS-Prover-V2-7B highly effective for automated theorem proving, assisting in formal verification, and accelerating the development of mathematical proofs within the Lean4 environment.