ByteDance-Seed / BFS-Prover-V2-32B

This repository contains the latest tactic generator model checkpoint from BFS-Prover-V2, a state-of-the-art step-level theorem proving system in Lean4. While the full BFS-Prover-V2 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: Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers

✨ Model Details

• Base Model: Qwen2.5-32B
• Training Approach: Multi-stage expert iteration with best-first tree search
• Training Data Sources:
  • Mathlib (via LeanDojo)
  • Lean-Github repositories
  • Autoformalized NuminaMath datasets

📈 Performance

BFS-Prover-V2 achieves 95.08% and 41.4% on miniF2F and ProofNet test sets respectively, when integrated with the full inference system.

⚙️ 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-Seed/BFS-Prover-V2-32B")
tokenizer = AutoTokenizer.from_pretrained("ByteDance-Seed/BFS-Prover-V2-32B")
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: "calc x - 1 = (y + 2) - 1 := by rw [h]
#                             _ = y + 1 := by ring"

📚 Citation

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

@article{xin2025bfsproverv2,
  title={Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers},
  author={Xin, Ran and Zheng, Zeyu and Nie, Yanchen and Yuan, Kun and Xiao, Xia},
  journal={arXiv preprint arXiv:2509.06493},
  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] )
• Zeyu Zheng ( [email protected] )