Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Yutong Wu, Di Huang, Ruosi Wan, Yue Peng, Shijie Shang, Chenrui Cao, Lei Qi, Rui Zhang, Zidong Du, Jie Yan, Xing Hu

TL;DR

StepFun-Formalizer introduces ThinkingF, a data-synthesis and training pipeline that fuses formal-language domain knowledge with informal-to-formal reasoning to advance autoformalization. By distilling vast formal-knowledge data, synthesizing reasoning trajectories via a template, and applying two-stage supervised fine-tuning followed by reinforcement learning with a verifiable BEq reward, it yields 7B and 32B models that achieve state-of-the-art BEq scores on FormalMATH-Lite and ProverBench ($40.5\%$ and $26.7\%$ at BEq@1 respectively). The work demonstrates that both knowledge and reasoning datasets contribute to improvements, with template-guided reasoning providing substantial gains over direct distillation of general reasoning. The results show strong in-domain performance and competitive out-of-domain generalization, suggesting practical benefits for training verifiable theorem-proving systems and broad autoformalization tasks. The approach also underscores the value of verifiable rewards in steering LLMs toward correct formal translations and long-context reasoning across domains.

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.

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

TL;DR

StepFun-Formalizer introduces ThinkingF, a data-synthesis and training pipeline that fuses formal-language domain knowledge with informal-to-formal reasoning to advance autoformalization. By distilling vast formal-knowledge data, synthesizing reasoning trajectories via a template, and applying two-stage supervised fine-tuning followed by reinforcement learning with a verifiable BEq reward, it yields 7B and 32B models that achieve state-of-the-art BEq scores on FormalMATH-Lite and ProverBench ( and at BEq@1 respectively). The work demonstrates that both knowledge and reasoning datasets contribute to improvements, with template-guided reasoning providing substantial gains over direct distillation of general reasoning. The results show strong in-domain performance and competitive out-of-domain generalization, suggesting practical benefits for training verifiable theorem-proving systems and broad autoformalization tasks. The approach also underscores the value of verifiable rewards in steering LLMs toward correct formal translations and long-context reasoning across domains.

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.

Paper Structure

This paper contains 56 sections, 5 equations, 19 figures, 10 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Large Language Models for Autoformalization.
  4. Reasoning-Enhanced Large Language Models.
  5. Problem Statement
  6. Method
  7. Knowledge Distillation With Selection
  8. Informal Problem Preparation
  9. Formal Statement Generation and Selection
  10. Informal-to-Formal Reasoning Data Synthesis
  11. Template Design for Reasoning
  12. Synthesizing reasoning trajectories upon existing human-annotated data.
  13. Two-Stage Supervised Fine-tuning
  14. Reinforcement Learning With Verifiable Reward
  15. Experiments
  16. ...and 41 more sections

Figures (19)

  • 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.
  • Figure 2: Categorical analysis for errors in autoformalization model. "Kimina-Auto" refers to Kimina-Autoformalizer. It illustrates the proportion of two error types in autoformalization, both of which are mitigated in StepFun-Formalizer.
  • Figure 3: The illustration of ThinkingF method. Our method mainly consists of the construction process for knowledge and reasoning dataset (Section \ref{['sec:data_synthesis_1']} and \ref{['sec:data_synthesis_2']}), and the model training process (Section \ref{['sec:sft']} and \ref{['sec:rl']}).
  • Figure 4: The prompts and examples in the template-guided reasoning construction framework. (a) The task description for autoformalization. (b) Understanding of natural language problems. (c) An example of concept analysis in problem understanding. (d) Analysis of converting informal math objects into formal language. (e) An example of mapping concepts to Lean in informal-to-formal analysis.
  • Figure 5: The proportion (%) of provable formal statements among 10K problems from NuminaMath-1.5 in each domain.
  • ...and 14 more figures

Theorems & Definitions (2)

  • Definition 3.1: LLM-based Autoformalization
  • Definition 3.2: Bidirectional Extended Definitional Equivalence, BEq