StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion
We introduce StepFun-Formalizer, a family of large language models designed to translate natural-language mathematical problems into formal statements in Lean 4. Through the fusion of formal knowledge and informal-to-formal reasoning capability, StepFun-Formalizer achieves strong performance on autoformalization tasks. Evaluated with BEq verification on mainstream benchmarks including FormalMATH-Lite, ProverBench, and CombiBench, StepFun-Formalizer matches or exceeds all prior general-purpose and specialized autoformalization models of comparable scale. Please refer to our paper for more details.
Figure 1: A case study to demonstrate the impact of formal knowledge and informal-to-formal reasoning capability on autoformalization models. It shows that general-purpose models without formal knowledge make mistakes in code implementation, while specialized ones without reasoning capability struggle with problem understanding and informal-formal alignment. StepFun-Formalizer improves autoformalization performance by combining these two capabilities.
Figure 2: The illustration of our method. It shows the construction of the knowledge and reasoning datasets (① and ②), as well as the training process including SFT and RL (③ and ④).
Tabel 1: BEq@1 and BEq@16 (%) results of StepFun-Formalizer and baselines on three benchmarks. See src/eval_benchmarks.py for the evaluation code.
| Model | Download |
|---|---|
| StepFun-Formalizer-7B | 🤗HuggingFace |
| StepFun-Formalizer-32B | 🤗HuggingFace |
Both the code repository and the model weights are released under the Apache License (Version 2.0).
@misc{stepfunformalizer2025,
title={StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion},
author={Yutong Wu and Di Huang and Ruosi Wan and Yue Peng and Shijie Shang and Chenrui Cao and Lei Qi and Rui Zhang and Zidong Du and Jie Yan and Xing Hu},
year={2025},
eprint={2508.04440},
archivePrefix={arXiv},
primaryClass={cs.CL},
url={https://arxiv.org/abs/2508.04440},
}