Hugging Face Overview
BFS-Prover: A Specialized Tactic Generator for Lean4
BFS-Prover is a 7.6 billion parameter model from ByteDance-Seed, built upon the Qwen2.5-Math-7B base, and is a core component of a larger theorem proving system. It is specifically fine-tuned to generate Lean4 tactics from given proof states, aiming to automate the process of formal mathematical proof construction.
Key Capabilities & Features
- State-of-the-art Performance: Achieves a score of 72.95% on the MiniF2F test benchmark, outperforming other systems like HunyuanProver and DeepSeek-Prover-V1.5.
- Efficient Design: Notably, it reaches high performance without relying on a separate critic model (value function), simplifying its architecture compared to many other provers.
- Training Methodology: Utilizes Supervised Fine-Tuning (SFT) on state-tactic pairs and Direct Preference Optimization (DPO) with compiler feedback.
- Comprehensive Training Data: Trained on diverse Lean4-specific datasets including Mathlib (via LeanDojo), Lean-Github repositories, Lean-Workbook, and the autoformalized NuminaMath-CoT dataset.
- Context Length: Supports a substantial context length of 131,072 tokens, allowing for complex proof states.
Ideal Use Cases
- Automatic Theorem Proving: Best suited for automating proof steps within the Lean4 theorem prover.
- Formal Verification: Can assist in formal verification tasks by generating valid tactics to advance proof goals.
- Mathematical Research: Supports researchers and mathematicians in constructing and verifying complex proofs in Lean4.