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

TL;DR

This paper introduces StepFun-Formalizer, a large language model trained with a novel pipeline that combines formal knowledge mastery and reasoning abilities, significantly improving autoformalization accuracy for mathematical statements.

Contribution

It presents ThinkingF, a data synthesis and training pipeline that enhances both formal knowledge and reasoning in LLMs for autoformalization tasks.

Findings

Achieved state-of-the-art BEq@1 scores of 40.5% on FormalMATH-Lite.

Developed datasets with formal knowledge and reasoning trajectories.

Models exhibit strong formal knowledge and reasoning capabilities.

Abstract

Autoformalization aims to translate natural-language mathematical statements into a formal language. While LLMs have accelerated progress in this area, existing methods still suffer from low accuracy. We identify two key abilities for effective autoformalization: comprehensive mastery of formal-language domain knowledge, and reasoning capability of natural language problem understanding and informal-formal alignment. Without the former, a model cannot identify the correct formal objects; without the latter, it struggles to interpret real-world contexts and map them precisely into formal expressions. To address these gaps, we introduce ThinkingF, a data synthesis and training pipeline that improves both abilities. First, we construct two datasets: one by distilling and selecting large-scale examples rich in formal knowledge, and another by generating informal-to-formal reasoning trajectories guided by expert-designed templates. We then apply SFT and RLVR with these datasets to further fuse and refine the two abilities. The resulting 7B and 32B models exhibit both comprehensive formal knowledge and strong informal-to-formal reasoning. Notably, StepFun-Formalizer-32B achieves SOTA BEq@1 scores of 40.5% on FormalMATH-Lite and 26.7% on ProverBench, surpassing all prior general-purpose and specialized models.