StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs
  through Knowledge-Reasoning Fusion
Authors: name: Yutong Wu, name: Di Huang, name: Ruosi Wan, name: Yue Peng, name: Shijie Shang, name: Chenrui Cao, name: Lei Qi, name: Rui Zhang, name: Zidong Du, name: Jie Yan, name: Xing Hu

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.