BFS-Prover
| Property | Value |
|---|---|
| Base Model | Qwen2.5-Math-7B |
| License | Apache 2.0 |
| Paper | arXiv:2502.03438 |
| Best Performance | 72.95% on MiniF2F |
What is BFS-Prover?
BFS-Prover is a cutting-edge automatic theorem proving system developed by ByteDance Research that leverages large language models for generating mathematical proofs in Lean4. Built upon Qwen2.5-Math-7B, it implements a Best-First Search (BFS) approach to navigate proof states efficiently, achieving state-of-the-art performance without requiring a critic model.
Implementation Details
The model employs a two-stage training approach: Supervised Fine-Tuning (SFT) on state-tactic pairs, followed by Direct Preference Optimization (DPO) using compiler feedback. Training data is sourced from Mathlib, Lean-Github repositories, Lean-Workbook, and the AutoFormalized NuminaMath-CoT dataset.
- Best-First Search implementation without requiring complex MCTS
- Direct tactic generation from proof states
- Efficient state-space exploration
Core Capabilities
- State-of-the-art performance on MiniF2F test benchmark (72.95%)
- Generates tactics for transforming proof states in Lean4
- Handles complex mathematical theorems efficiently
- Simple integration through standardized input format
Frequently Asked Questions
Q: What makes this model unique?
BFS-Prover achieves superior performance using a simpler architecture without requiring a critic model, making it more efficient than competitors like HunyuanProver and DeepSeek-Prover-V1.5.
Q: What are the recommended use cases?
The model is specifically designed for automatic theorem proving in Lean4, particularly useful for mathematicians and computer scientists working on formal verification and mathematical proof automation.
