Update README.md

README.md

@@ -18,7 +18,8 @@ tags:
 
 # BFS-Prover Tactic Generator
 
-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.
+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 state-of-the-art performance on formal mathematics tasks. Given a tactic state in Lean4, the model generates a tactic that transforms the current proof state into a new state, progressively working towards completing the proof.
+
 
 ## Model Details
 
@@ -39,19 +40,16 @@ BFS-Prover achieves state-of-the-art performance on the MiniF2F test benchmark.
 
 | Prover System | Search Method | Critic Model | Tactic Budget | Score |
 |---------------|---------------|--------------|---------------|--------|
-| BFS-Prover (Accumulative) | BFS | No | - | **72.95%** |
-| BFS-Prover (This Work) | BFS | No | 2048×2×600 | **70.83% ± 0.89%** |
+| 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% |
 
-*Note: DeepSeek-Prover-V1.5 uses whole-proof generation method; tactic budget decomposed for comparison.
 
 ### Key Advantages
-- Achieves better performance without requiring a critic model
-- Uses simpler search method (BFS) compared to MCTS
-- Shows strong scaling with increased search passes
-- Benefits from DPO training using compiler feedback
+- Achieves better performance without requiring a critic model (value function)
+- Combined with simpler search method (BFS) rather than MCTS
 
 ## Usage
 
@@ -59,20 +57,22 @@ BFS-Prover achieves state-of-the-art performance on the MiniF2F test benchmark.
 # Example code for loading and using the tactic generator model
 from transformers import AutoModelForCausalLM, AutoTokenizer
 
-model = AutoModelForCausalLM.from_pretrained("path/to/bfsprover-tactic-generator")
-tokenizer = AutoTokenizer.from_pretrained("path/to/bfsprover-tactic-generator")
+model = AutoModelForCausalLM.from_pretrained("bytedance-research/BFS-Prover")
+tokenizer = AutoTokenizer.from_pretrained("bytedance-research/BFS-Prover")
 
-# Input format example: 
-prompt = f"{Lean4 TacticState}" + ":::"
+# Input format example:
+state = "h : x = y + 2 ⊢ x - 1 = y + 1" 
+sep = ":::"
+prompt = state + sep
 inputs = tokenizer(prompt, return_tensors="pt")
 outputs = model.generate(**inputs)
-tactic = tokenizer.decode(outputs[0])
-```
+tactic = tokenizer.decode(outputs[0], skip_special_tokens=True).split(sep)[1]
 
-## System Requirements
-
-- Compatible with Hugging Face Transformers library
-- Recommended: 16GB+ GPU memory for inference
+# Example input-output:
+# Input state: "h : x = y + 2 ⊢ x - 1 = y + 1"
+# Model output: "{input state}:::simp [h]"
+# Final tactic: "simp [h]"
+```
 
 ## Citation