ByteDance-Seed
/

BFS-Prover

@@ -16,13 +16,13 @@ tags:
 - 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 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.
 **📄 Paper: [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://arxiv.org/abs/2502.03438)**
-## Model Details
 - Base Model: Qwen2.5-Math-7B
 - Training Approach:
@@ -34,7 +34,7 @@ This repository contains the latest tactic generator model checkpoint from BFS-P
   - 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
@@ -48,11 +48,11 @@ BFS-Prover achieves state-of-the-art performance on the MiniF2F test benchmark.
 | 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.
@@ -80,7 +80,7 @@ print(tactic)
 # Final tactic: "simp [h]"
 ```
-## Citation
 If you use this model in your research, please cite our paper:
@@ -93,11 +93,11 @@ If you use this model in your research, please cite our paper:
 }
 ```
-## License
 https://choosealicense.com/licenses/apache-2.0/
-## Contact
 For questions and feedback about the tactic generator model, please contact:
 - Ran Xin ([email protected])

 - 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 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.
 **📄 Paper: [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://arxiv.org/abs/2502.03438)**
+## ✨ Model Details
 - Base Model: Qwen2.5-Math-7B
 - Training Approach:
   - 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
 | 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.
 # Final tactic: "simp [h]"
 ```
+## 📚 Citation
 If you use this model in your research, please cite our paper:
 }
 ```
+## 📄 License
 https://choosealicense.com/licenses/apache-2.0/
+## 📧 Contact
 For questions and feedback about the tactic generator model, please contact:
 - Ran Xin ([email protected])