StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs
  through Knowledge-Reasoning Fusion
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.
6894a81a741a16f544fbd0e1
Yutong Wu
claimed_verified
2025-08-08T16:21:07.039Z
64e42be971139393aa3dd90a
https://cdn-avatars.huggingface.co/v1/production/uploads/64e42be971139393aa3dd90a/j6KqGXqspeSx1Z4QA6hr4.jpeg
Yutong Wu
user
wyt2000
6894a81a741a16f544fbd0e2
Di Huang
6894a81a741a16f544fbd0e3
Ruosi Wan
6894a81a741a16f544fbd0e4
Yue Peng
6894a81a741a16f544fbd0e5
Shijie Shang
6894a81a741a16f544fbd0e6
Chenrui Cao
claimed_verified
2025-08-08T16:21:03.477Z
662a5f2e2d1a003cd7c4e137
/avatars/ca44ec3a968d612cb185005329d56732.svg
Chenrui Cao
user
DesertEagle185
6894a81a741a16f544fbd0e7
Lei Qi
6894a81a741a16f544fbd0e8
Rui Zhang
6894a81a741a16f544fbd0e9
Zidong Du
6894a81a741a16f544fbd0ea
Jie Yan
6894a81a741a16f544fbd0eb
Xing Hu
StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs
  through Knowledge-Reasoning Fusion
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.
ThinkingF, a data synthesis and training pipeline, enhances autoformalization by improving formal knowledge and informal-to-formal reasoning, achieving state-of-the-art results in formalization tasks.
LLMs autoformalization formal-language domain knowledge natural language problem understanding informal-formal alignment data synthesis training pipeline SFT RLVR FormalMATH-Lite ProverBench StepFun-Formalizer