|
|
---
|
|
|
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.
|
|
|
|
