stepfun-ai/StepFun-Formalizer

stepfun-ai/StepFun-Formalizer

Description: StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion

Language: Python

License: Apache-2.0

Stars: 30

Forks: 3

Open issues: 0

Created: 2025-08-19T03:34:06Z

Pushed: 2025-08-19T03:34:42Z

Default branch: master

Fork: no

Archived: no

README:

StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion

Introduction

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.

Method

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

Evalaution Results

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

License

Both the code repository and the model weights are released under the Apache License (Version 2.0).

Citation

@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},
}