Update README.md

README.md

@@ -1,94 +1,64 @@
-# BFS-Prover
+# BFS-Prover Tactic Generator
 
-BFS-Prover is a scalable automatic theorem prover that leverages Best-First Tree Search (BFS) to navigate proof search spaces efficiently. This model achieves state-of-the-art performance on the MiniF2F test benchmark with a score of 72.95%, demonstrating that properly scaled BFS can match or exceed the performance of more complex search methods.
+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 competitive performance on formal mathematics tasks.
 
 ## Model Details
 
-- **Architecture**: Based on Qwen2.5-Math-7B
-- **Task**: Automatic theorem proving in Lean4
-- **Training**: Trained through expert iteration with SFT and DPO
-- **License**: apache-2.0
-- **Framework**: LeanDojo for Lean4 integration
-
-## Key Features
-
-1. **Expert Iteration with Self-Filtering**
-   - Strategic filtering of problems solvable by beam search
-   - Progressive focusing on harder theorems
-   - Continuous policy improvement through iterative training
-
-2. **Direct Preference Optimization (DPO)**
-   - Leverages compiler feedback for policy refinement
-   - Uses positive and negative tactic pairs for learning
-   - Improves sampling efficiency during proof search
-
-3. **Length-Normalized BFS**
-   - Incorporates path length normalization
-   - Enables effective exploration of deeper proof paths
-   - Balances between shallow and deep reasoning
+- 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
 
-- **MiniF2F Test Score**: 72.95% (accumulative)
-- **Single Run Score**: 70.83% ± 0.89%
-- **Search Configuration**:
-  - Temperature: 1.1
-  - Expansion width: 2
-  - Length normalization factor: 0.5
+When integrated into the full BFS-Prover system, this tactic generator model achieved
+72.54% success rate on MiniF2F test set accumulatively.
 
 ## Usage
 
 ```python
+# Example code for loading and using the tactic generator model
 from transformers import AutoModelForCausalLM, AutoTokenizer
 
-# Load tokenizer and model
-model_name = "bytedance-research/BFS-Prover"
-tokenizer = AutoTokenizer.from_pretrained(model_name)
-model = AutoModelForCausalLM.from_pretrained(model_name)
-
-# For memory-efficient loading
-model = AutoModelForCausalLM.from_pretrained(
-    model_name,
-    device_map="auto",    # Automatic device mapping
-    load_in_8bit=True     # Or load_in_4bit=True for more memory savings
-)
-```
+model = AutoModelForCausalLM.from_pretrained("path/to/bfsprover-tactic-generator")
+tokenizer = AutoTokenizer.from_pretrained("path/to/bfsprover-tactic-generator")
 
-## Required Environment
-
-- Python 3.8+
-- Lean4
-- LeanDojo
-- transformers
-- torch
+# Input format example: 
+prompt = f"{Lean4 TacticState}" + ":::"
+inputs = tokenizer(prompt, return_tensors="pt")
+outputs = model.generate(**inputs)
+tactic = tokenizer.decode(outputs[0])
+```
 
-## Limitations
+## System Requirements
 
-- Based on a 7B parameter model, which may limit capture of complex mathematical patterns
-- Context window constraints may affect handling of extensive proof states
-- Trade-off between model size and inference speed in tree search
+- Compatible with Hugging Face Transformers library
+- Recommended: 16GB+ GPU memory for inference
 
 ## Citation
 
+If you use this model in your research, please cite our paper:
+
 ```bibtex
-@article{bfs-prover2024,
+@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},
-  year={2024}
+  journal={arXiv preprint arXiv:2502.03438},
+  year={2025}
 }
 ```
 
-## Contributors
+## License
+
+https://choosealicense.com/licenses/apache-2.0/
 
-Key Contributors:
-- Ran Xin (Seed Foundation Code, ByteDance)
-- Chenguang Xi (Seed Foundation Code, ByteDance)
-- Jie Yang (Applied Machine Learning, ByteDance)
-- Feng Chen (Stanford University)
+## Contact
 
-Additional Contributors:
-- Hang Wu (Applied Machine Learning, ByteDance)
-- Xia Xiao (Seed Foundation Code, ByteDance)
-- Yifan Sun (Seed Foundation Code, ByteDance)
-- Shen Zheng (Seed Foundation Code, ByteDance)
-- Kai Shen (Seed Foundation Code, ByteDance)
+For questions and feedback about the tactic generator model, please contact:
+- Ran Xin (ran.xin@bytedance.com)
+- Kai Shen (shen.kai@bytedance.com)