Hugging Face Overview
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.