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
• 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

• Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases [32.96018876882992]
  We argue for theory-level autoformalization: formalizing complete theories, including all their inter-dependencies, as structured libraries.<n>We examine the significance of this shift, address alternative views, identify open challenges, and propose three promising paths forward.
  arXiv  Detail & Related papers  (2026-07-14T21:58:52Z)
• Shaping Schema via Language Representation as the Next Frontier for LLM Intelligence Expanding [88.11781604392606]
  This paper defines language representation as the linguistic and symbolic constructs used to map and model the real world.<n>We argue that shaping schemas through advanced language representation is the next frontier for expanding Large Language Models.
  arXiv  Detail & Related papers  (2026-05-10T02:42:29Z)
• FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean [7.11696910077237]
  FormalScience is a human-in-the-loop agentic pipeline to produce textitsyntactically correct and textitsemantically aligned formal proofs of informal reasoning for low economic cost.<n>We construct FormalPhysics, a dataset of 200 physics problems and solutions (primarily quantum mechanics and electromagnetism) along with their Lean4 formal representations.<n>We evaluate open-source models and proprietary systems on a statement autoformalisation task on our dataset via zero-shot prompting, self-refinement with error feedback, and a novel multi-stage agentic approach.
  arXiv  Detail & Related papers  (2026-04-24T20:47:22Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  We propose a Reflective Autoformalization method that integrates semantic consistency evaluation into the autoformalization process.<n>This enables the model to iteratively generate formal statements, assess its semantic fidelity, and self-correct identified errors.<n>Experiments show that ReForm achieves an average improvement of 22.6 percentage points over the strongest baselines.
  arXiv  Detail & Related papers  (2025-10-28T16:22:54Z)
• Automated Formalization via Conceptual Retrieval-Augmented LLMs [19.328918823576153]
  CRAMF is a Concept-driven Retrieval-Augmented Mathematical Formalization framework.<n>We introduce a framework for automatically constructing a concept-definition knowledge base from Mathlib4.<n>Experiments on miniF2F, ProofNet, and our newly proposed AdvancedMath benchmark show that CRAMF can be seamlessly integrated into LLM-based autoformalizers.
  arXiv  Detail & Related papers  (2025-08-09T10:54:25Z)
• 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.