metadata
license: apache-2.0
datasets:
- SJTULean/LeanStatement_SFT
- SJTULean/LeanStatement_RL
language:
- zho
- eng
- fra
- spa
- por
- deu
- ita
- rus
- jpn
- kor
- vie
- tha
- ara
metrics:
- accuracy
base_model:
- Qwen/Qwen2.5-7B-Instruct
Through PPO using a reward model trained on merely 5% of the LeanStatement_RL dataset, our model achieved enhanced performance, reaching a pass@1 compilation success rate of 95.3% (465/488) on MiniF2F and 76.0% (284/374) on ProofNet benchmarks. Combined with our SFT results, these findings establish a new state-of-the-art in mathematics formalization as of December 2024.