Update README.md

README.md

@@ -1,3 +1,94 @@
----
-license: apache-2.0
----
+# BFS-Prover
+
+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.
+
+## 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
+
+## 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
+
+## Usage
+
+```python
+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
+)
+```
+
+## Required Environment
+
+- Python 3.8+
+- Lean4
+- LeanDojo
+- transformers
+- torch
+
+## Limitations
+
+- 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
+
+## Citation
+
+```bibtex
+@article{bfs-prover2024,
+  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}
+}
+```
+
+## Contributors
+
+Key Contributors:
+- Ran Xin (Seed Foundation Code, ByteDance)
+- Chenguang Xi (Seed Foundation Code, ByteDance)
+- Jie Yang (Applied Machine Learning, ByteDance)
+- Feng Chen (Stanford University)
+
+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)