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

• URL: http://arxiv.org/abs/2508.04440v1
• Date: Wed, 06 Aug 2025 13:28:22 GMT
• Title: StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion
• Authors: Yutong Wu, Di Huang, Ruosi Wan, Yue Peng, Shijie Shang, Chenrui Cao, Lei Qi, Rui Zhang, Zidong Du, Jie Yan, Xing Hu,
• Abstract summary: We identify two key abilities for effective autoformalization.<n>We introduce ThinkingF, a data synthesis and training pipeline that improves both abilities.<n>The resulting 7B and 32B models exhibit both comprehensive formal knowledge and strong informal-to-formal reasoning.
• Score: 30.51794514312176
• License: http://creativecommons.org/licenses/by-sa/4.0/
• 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.

Related papers

• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [68.00108157244952]
  Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes are neither reliable nor scalable.<n>A promising yet largely uncharted alternative is formal language-based reasoning.<n>Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes.
  arXiv  Detail & Related papers  (2025-07-22T08:13:01Z)
• FMC: Formalization of Natural Language Mathematical Competition Problems [12.86616278136374]
  We propose an autoformalization pipeline based on large language models with error feedback.<n>We curate an Olympiad-level dataset aligning natural language problems with Lean formalizations.<n>We show that few-shot learning, error feedback, and increasing sampling numbers enhance the autoformalization process.
  arXiv  Detail & Related papers  (2025-07-15T12:52:47Z)
• PEIRCE: Unifying Material and Formal Reasoning via LLM-Driven Neuro-Symbolic Refinement [13.042323420379187]
  PEIRCE is a neuro-symbolic framework designed to unify material and formal inference through an iterative conjecture-criticism process.<n>We demonstrate its capabilities in the domain of natural language explanation generation.
  arXiv  Detail & Related papers  (2025-04-05T09:04:47Z)
• Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency [22.86318578119266]
  We introduce a novel framework that scores and selects the best result from k autoformalization candidates based on symbolic equivalence and semantic consistency.<n>Our experiments on the MATH and miniF2F datasets demonstrate that our approach significantly enhances autoformalization accuracy.
  arXiv  Detail & Related papers  (2024-10-28T11:37:39Z)
• Large Language Models with Controllable Working Memory [64.71038763708161]
  Large language models (LLMs) have led to a series of breakthroughs in natural language processing (NLP) What further sets these models apart is the massive amounts of world knowledge they internalize during pretraining. How the model's world knowledge interacts with the factual information presented in the context remains under explored.
  arXiv  Detail & Related papers  (2022-11-09T18:58:29Z)
• Autoformalization with Large Language Models [22.86710743804944]
  A successful autoformalization system could advance the fields of formal verification, program synthesis, and artificial intelligence. We show large language models provide new prospects towards this goal. Our methodology results in a new state-of-the-art result on the MiniF2F theorem proving benchmark, improving the proof rate from $29.6%$ to $35.2%$.
  arXiv  Detail & Related papers  (2022-05-25T09:53:30Z)
• A Latent-Variable Model for Intrinsic Probing [93.62808331764072]
  We propose a novel latent-variable formulation for constructing intrinsic probes. We find empirical evidence that pre-trained representations develop a cross-lingually entangled notion of morphosyntax.
  arXiv  Detail & Related papers  (2022-01-20T15:01:12Z)
• Semi-supervised Formality Style Transfer using Language Model Discriminator and Mutual Information Maximization [52.867459839641526]
  Formality style transfer is the task of converting informal sentences to grammatically-correct formal sentences. We propose a semi-supervised formality style transfer model that utilizes a language model-based discriminator to maximize the likelihood of the output sentence being formal. Experiments showed that our model outperformed previous state-of-the-art baselines significantly in terms of both automated metrics and human judgement.
  arXiv  Detail & Related papers  (2020-10-10T21:05:56Z)
• Leap-Of-Thought: Teaching Pre-Trained Models to Systematically Reason Over Implicit Knowledge [96.92252296244233]
  Large pre-trained language models (LMs) acquire some reasoning capacity, but this ability is difficult to control. We show that LMs can be trained to reliably perform systematic reasoning combining both implicit, pre-trained knowledge and explicit natural language statements. Our work paves a path towards open-domain systems that constantly improve by interacting with users who can instantly correct a model by adding simple natural language statements.
  arXiv  Detail & Related papers  (2020-06-11T17:02:20Z)
• Data Annealing for Informal Language Understanding Tasks [66.2988222278475]
  We propose a data annealing transfer learning procedure to bridge the performance gap on informal language tasks. It successfully utilizes a pre-trained model such as BERT in informal language.
  arXiv  Detail & Related papers  (2020-04-24T09:27:09Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.