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.