Update README.md

README.md

@@ -44,8 +44,8 @@ Additionally, the model demonstrates strong generalization to undergraduate-leve
 ```python
 # Example code for loading and using the tactic generator model
 from transformers import AutoModelForCausalLM, AutoTokenizer
-model = AutoModelForCausalLM.from_pretrained("ByteDance-Seed/BFS-Prover-V2-32B")
-tokenizer = AutoTokenizer.from_pretrained("ByteDance-Seed/BFS-Prover-V2-32B")
+model = AutoModelForCausalLM.from_pretrained("ByteDance-Seed/BFS-Prover-V2-7B")
+tokenizer = AutoTokenizer.from_pretrained("ByteDance-Seed/BFS-Prover-V2-7B")
 
 # imo_1964_p2 from miniF2F
 state = """a b c : ℝ
@@ -68,7 +68,7 @@ outputs = model.generate(**inputs)
 tactic = tokenizer.decode(outputs[0], skip_special_tokens=True).split(sep)[1]
 print(tactic)
 
-# Generated tactic: "nlinarith [sq_nonneg (a - b), sq_nonneg (c - a), sq_nonneg (b - c)]"
+# Generated tactic: "nlinarith [sq_nonneg (c - a), sq_nonneg (b - a), sq_nonneg (c - b), h₀.1, h₀.2.1, h₀.2.2, h₁.le, h₂.le, h₃.le]"
 ```
 
 ## 📚 Citation