LeanFormalizer_SFT
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.
- Downloads last month
- 14
Inference Providers
NEW
This model is not currently available via any of the supported Inference Providers.
The model cannot be deployed to the HF Inference API:
The model has no library tag.