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——一个旨在同时提升这两项能力的数据合成与训练流程。首先，我们构建了两个数据集：一个通过提炼和筛选富含形式知识的大规模样例得到，另一个则通过专家设计的模板引导生成从非形式到形式的推理轨迹。随后，我们利用这些数据集应用监督微调和基于验证器的强化学习，以进一步融合并精炼这两项能力。由此得到的7B和32B模型同时展现出全面的形式知识和强大的非形式到形式推理能力。值得注意的是，StepFun-Formalizer-32B在FormalMATH-Lite上取得了40.5%的BEq@1分数，在ProverBench上取得了26.7%的BEq@1分数，均达到当前最优水平，超越了所有先前的通用模型与专用模型。