bytedance-research / BFS-Prover

BFS-Prover Tactic Generator

This repository contains the latest tactic generator model checkpoint from BFS-Prover, a state-of-the-art theorem proving system in Lean4. While the full BFS-Prover system integrates multiple components for scalable theorem proving, we are releasing the core tactic generation model that achieved state-of-the-art performance on formal mathematics tasks. Given a proof state in Lean4, the model generates a tactic that transforms the current proof state into a new state, progressively working towards completing the proof.

Model Details

• Base Model: Qwen2.5-Math-7B
• Training Approach:
  • Supervised Fine-Tuning (SFT) on state-tactic pairs
  • Direct Preference Optimization (DPO) using compiler feedback
• Training Data Sources:
  • Mathlib (via LeanDojo)
  • Lean-Github repositories
  • Lean-Workbook
  • Autoformalized NuminaMath-CoT dataset

Performance

BFS-Prover achieves state-of-the-art performance on the MiniF2F test benchmark. Here's a detailed comparison:

MiniF2F Test Benchmark Results

Key Advantages

• Achieves better performance without requiring a critic model (value function)
• Combined with simpler search method (BFS) rather than MCTS

Usage

# Example code for loading and using the tactic generator model
from transformers import AutoModelForCausalLM, AutoTokenizer

model = AutoModelForCausalLM.from_pretrained("bytedance-research/BFS-Prover")
tokenizer = AutoTokenizer.from_pretrained("bytedance-research/BFS-Prover")

# Input format: the model expects tactic states in the format f"{state}:::"
# The model will echo back the input state followed by the generated tactic

state = "h : x = y + 2 ⊢ x - 1 = y + 1" 
sep = ":::"
prompt = state + sep  # Creates "h : x = y + 2 ⊢ x - 1 = y + 1:::"

inputs = tokenizer(prompt, return_tensors="pt")
outputs = model.generate(**inputs)
tactic = tokenizer.decode(outputs[0], skip_special_tokens=True).split(sep)[1]
print(tactic)

# Complete example:
# Input state:  "h : x = y + 2 ⊢ x - 1 = y + 1"
# Full prompt:  "h : x = y + 2 ⊢ x - 1 = y + 1:::"
# Model output: "h : x = y + 2 ⊢ x - 1 = y + 1:::simp [h]"
# Final tactic: "simp [h]"

Citation

If you use this model in your research, please cite our paper:

@article{xin2025bfs,
  title={BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving},
  author={Xin, Ran and Xi, Chenguang and Yang, Jie and Chen, Feng and Wu, Hang and Xiao, Xia and Sun, Yifan and Zheng, Shen and Shen, Kai},
  journal={arXiv preprint arXiv:2502.03438},
  year={2025}
}

License

https://choosealicense.com/licenses/apache-2.0/

Contact

For questions and feedback about the tactic generator model, please contact:

• Ran Xin ( [email protected] )
• Kai Shen ( [email protected] )