File size: 939 Bytes
cfd755b |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 |
---
license: apache-2.0
datasets:
- SJTULean/LeanStatement_SFT
language:
- zho
- eng
- fra
- spa
- por
- deu
- ita
- rus
- jpn
- kor
- vie
- tha
- ara
result:
dataset:
type: Formalizer Lean
name: miniF2F
metrics:
- name: pass@1
type: pass@1
value: 0.9406
verified: false
base_model:
- Qwen/Qwen2.5-7B-Instruct
---
# LeanFormalizer_SFT
<!-- Provide a quick summary of what the model is/does. -->
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.
|