Update README.md
Browse files
README.md
CHANGED
|
@@ -20,4 +20,4 @@ base_model:
|
|
| 20 |
|
| 21 |
<!-- Provide a quick summary of what the model is/does. -->
|
| 22 |
|
| 23 |
-
Based on Qwen2.5-7b and trained on our LeanStatement_SFT dataset, our model achieves **state-of-the-art** performance in formal mathematics verification, with a **pass@1 compilation success rate** of 94.1% (459/488) on MiniF2F and 75.4% (282/374) on ProofNet benchmarks as of December 2024. These results demonstrate the effectiveness of scaling laws in mathematical formalization using the Lean theorem prover.
|
|
|
|
| 20 |
|
| 21 |
<!-- Provide a quick summary of what the model is/does. -->
|
| 22 |
|
| 23 |
+
Based on Qwen2.5-7b and trained on our LeanStatement_SFT dataset, our model achieves **state-of-the-art** performance in formal mathematics verification, with a **pass@1 compilation success rate** of 94.1% (459/488) on MiniF2F and 75.4% (282/374) on ProofNet benchmarks as of December 2024(while our PPO model achieves 95.3% on MiniF2F and 76.0% on Proofnet). These results demonstrate the effectiveness of scaling laws in mathematical formalization using the Lean theorem prover.
|