Update README.md

README.md

@@ -60,17 +60,22 @@ from transformers import AutoModelForCausalLM, AutoTokenizer
 model = AutoModelForCausalLM.from_pretrained("bytedance-research/BFS-Prover")
 tokenizer = AutoTokenizer.from_pretrained("bytedance-research/BFS-Prover")
 
-# Input format example:
+# 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
+prompt = state + sep  # Creates "h : x = y + 2 ⊢ x - 1 = y + 1:::"
+
 inputs = tokenizer(prompt, return_tensors="pt")
 outputs = model.generate(**inputs)
 tactic = tokenizer.decode(outputs[0], skip_special_tokens=True).split(sep)[1]
+print(tactic)
 
-# Example input-output:
-# Input state: "h : x = y + 2 ⊢ x - 1 = y + 1"
-# Model output: "{input state}:::simp [h]"
+# Complete example:
+# Input state:  "h : x = y + 2 ⊢ x - 1 = y + 1"
+# Full prompt:  "h : x = y + 2 ⊢ x - 1 = y + 1:::"
+# Model output: "h : x = y + 2 ⊢ x - 1 = y + 1:::simp [h]"
 # Final tactic: "simp [h]"
 ```