Instructions to use ByteDance-Seed/BFS-Prover-V1-7B with libraries, inference providers, notebooks, and local apps. Follow these links to get started.

Libraries

How to use ByteDance-Seed/BFS-Prover-V1-7B with Transformers:

# Use a pipeline as a high-level helper
from transformers import pipeline

pipe = pipeline("text-generation", model="ByteDance-Seed/BFS-Prover-V1-7B")
messages = [
    {"role": "user", "content": "Who are you?"},
]
pipe(messages)

# Load model directly
from transformers import AutoTokenizer, AutoModelForCausalLM

tokenizer = AutoTokenizer.from_pretrained("ByteDance-Seed/BFS-Prover-V1-7B")
model = AutoModelForCausalLM.from_pretrained("ByteDance-Seed/BFS-Prover-V1-7B")
messages = [
    {"role": "user", "content": "Who are you?"},
]
inputs = tokenizer.apply_chat_template(
	messages,
	add_generation_prompt=True,
	tokenize=True,
	return_dict=True,
	return_tensors="pt",
).to(model.device)

outputs = model.generate(**inputs, max_new_tokens=40)
print(tokenizer.decode(outputs[0][inputs["input_ids"].shape[-1]:]))

Inference
Notebooks
Google Colab
Kaggle
Local Apps

vLLM

How to use ByteDance-Seed/BFS-Prover-V1-7B with vLLM:

Install from pip and serve model

# Install vLLM from pip:
pip install vllm
# Start the vLLM server:
vllm serve "ByteDance-Seed/BFS-Prover-V1-7B"
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:8000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "ByteDance-Seed/BFS-Prover-V1-7B",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Use Docker

docker model run hf.co/ByteDance-Seed/BFS-Prover-V1-7B

SGLang

How to use ByteDance-Seed/BFS-Prover-V1-7B with SGLang:

Install from pip and serve model

# Install SGLang from pip:
pip install sglang
# Start the SGLang server:
python3 -m sglang.launch_server \
    --model-path "ByteDance-Seed/BFS-Prover-V1-7B" \
    --host 0.0.0.0 \
    --port 30000
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:30000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "ByteDance-Seed/BFS-Prover-V1-7B",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Use Docker images

docker run --gpus all \
    --shm-size 32g \
    -p 30000:30000 \
    -v ~/.cache/huggingface:/root/.cache/huggingface \
    --env "HF_TOKEN=<secret>" \
    --ipc=host \
    lmsysorg/sglang:latest \
    python3 -m sglang.launch_server \
        --model-path "ByteDance-Seed/BFS-Prover-V1-7B" \
        --host 0.0.0.0 \
        --port 30000
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:30000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "ByteDance-Seed/BFS-Prover-V1-7B",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Docker Model Runner
How to use ByteDance-Seed/BFS-Prover-V1-7B with Docker Model Runner:
```
docker model run hf.co/ByteDance-Seed/BFS-Prover-V1-7B
```
Browse Quantizations to use this model in llama.cpp, Ollama, LM Studio, or any compatible app.

🚀 BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving

State-of-the-art tactic generation model in Lean4

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 here. 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.

📑 Paper: BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving

💻 Code: GitHub Repository

✨ 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

The model expects Lean4 tactic states in the format "{state}:::"
::: serves as a special indicator to signal the model to generate a tactic for the given state.
The model will echo back the input state followed by the generated tactic.

# 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")
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}
}