Update README.md

README.md

@@ -33,9 +33,25 @@ This repository contains the latest tactic generator model checkpoint from BFS-P
   - Autoformalized NuminaMath-CoT dataset
 
 ## Performance
+BFS-Prover achieves state-of-the-art performance on the MiniF2F test benchmark. Here's a detailed comparison:
 
-When integrated into the full BFS-Prover system, this tactic generator model achieved
-72.54% success rate on MiniF2F test set accumulatively.
+### MiniF2F Test Benchmark Results
+
+| 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%** |
+| 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
 
 ## Usage