license: apache-2.0
datasets:
- internlm/Lean-Workbook
- internlm/Lean-Github
- AI-MO/NuminaMath-CoT
language:
- en
base_model:
- Qwen/Qwen2.5-Math-7B
pipeline_tag: text-generation
library_name: transformers
tags:
- lean4
- theorem-proving
- formal-mathematics
BFS-Prover Tactic Generator
This repository contains the latest tactic generator model checkpoint from BFS-Prover, a state-of-the-art theorem proving system. 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 tactic 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
| Prover System | Search Method | Critic Model | Tactic Budget | Score |
|---|---|---|---|---|
| BFS-Prover | BFS | No | Accumulative | 72.95% |
| BFS-Prover | BFS | No | 2048×2×600 | 70.83% ± 0.89% |
| HunyuanProver | BFS | Yes | 600×8×400 | 68.4% |
| InternLM2.5-StepProver | BFS | Yes | 256×32×600 | 65.9% |
| DeepSeek-Prover-V1.5* | MCTS | No | 32×16×400 | 63.5% |
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])