ByteDance-Seed/BFS-Prover-V1-7B
ByteDance-Seed/BFS-Prover-V1-7B is a 7.6 billion parameter tactic generation model developed by ByteDance-Seed, based on Qwen2.5-Math-7B. It is specifically fine-tuned for automatic theorem proving within the Lean4 proof assistant, generating tactics from proof states. The model achieves state-of-the-art performance on the MiniF2F test benchmark, notably without requiring a separate critic model, making it suitable for scalable theorem proving applications.
Loading preview...
BFS-Prover-V1-7B: State-of-the-Art Lean4 Tactic Generation
BFS-Prover-V1-7B is a 7.6 billion parameter model from ByteDance-Seed, designed for automatic theorem proving in Lean4. This model serves as the core tactic generator within the broader BFS-Prover system, which employs a scalable Best-First Tree Search approach. It is built upon the Qwen2.5-Math-7B base model and has undergone Supervised Fine-Tuning (SFT) on state-tactic pairs, followed by Direct Preference Optimization (DPO) using compiler feedback.
Key Capabilities & Features
- Specialized Tactic Generation: Given a Lean4 proof state, the model generates the next tactic to advance the proof.
- High Performance: Achieves a score of 72.95% on the MiniF2F test benchmark, outperforming other systems like HunyuanProver and InternLM2.5-StepProver.
- Efficiency: Notably, it achieves leading performance without relying on a separate critic model (value function), simplifying the overall proving system.
- Training Data: Trained on a diverse dataset including Mathlib, Lean-Github repositories, Lean-Workbook, and the autoformalized NuminaMath-CoT dataset.
When to Use This Model
- Automated Theorem Proving: Ideal for integrating into systems that require automated generation of Lean4 tactics.
- Research in Proof Assistants: Useful for researchers exploring advanced methods in formal verification and AI-assisted mathematics.
- Lean4 Development: Can assist Lean4 users by suggesting tactics for complex proof states.
For more details, refer to the BFS-Prover paper.