Update README.md

README.md

@@ -52,6 +52,9 @@ BFS-Prover achieves state-of-the-art performance on the MiniF2F test benchmark.
 - Combined with simpler search method (BFS) rather than MCTS
 
 ## Usage
+The model expects tactic states in the format `"{state}:::"`, where `:::` 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.
+
 
 ```python
 # Example code for loading and using the tactic generator model
@@ -59,10 +62,6 @@ from transformers import AutoModelForCausalLM, AutoTokenizer
 
 model = AutoModelForCausalLM.from_pretrained("bytedance-research/BFS-Prover")
 tokenizer = AutoTokenizer.from_pretrained("bytedance-research/BFS-Prover")
-
-# Input format: the model expects tactic states in the format f"{state}:::"
-# The model will echo back the input state followed by the generated tactic
-
 state = "h : x = y + 2 ⊢ x - 1 = y + 1" 
 sep = ":::"
 prompt = state + sep  # Creates "h : x = y + 2 ⊢ x - 1 = y + 1:::"