Source-linked AI summary
Autoformalization in the Era of Large Language Models: A Survey
Ke Weng, Lun Du, Sirui Li, Wangyue Lu, Haozhe Sun, Hengyu Liu, Tiancheng Zhang
TL;DR
Formalizing informal mathematics remains labor-intensive, and LLM-generated mathematical solutions raise a need for correctness checks. This survey reviews autoformalization across mathematical tasks and workflows, including its potential role in formal verification of LLM outputs.
Problem
Formalizing informal mathematical reasoning remains labor-intensive, while LLMs can produce complex solutions whose correctness needs verification.
Source: §1 · p. 1Method
The survey reviews autoformalization across mathematical domains and difficulty levels, workflow, models, datasets, and formal verification of LLM outputs.
Source: §1 · p. 2Results
The survey synthesizes recent work on mathematical theorem proving and the potential combination of autoformalization with formal verification of LLM outputs.
Source: §1 · p. 2Takeaways & Limitations
Autoformalization offers a potential way to translate LLM outputs into verifiable representations, supporting trustworthiness in tasks requiring rigorous reasoning.
Source: §1 · p. 1
Abstract
from arXiv · showhide
Autoformalization, the process of transforming informal mathematical propositions into verifiable formal representations, is a foundational task in automated theorem proving, offering a new perspective on the use of mathematics in both theoretical and applied domains. Driven by the rapid progress in artificial intelligence, particularly large language models (LLMs), this field has witnessed substantial growth, bringing both new opportunities and unique challenges. In this survey, we provide a comprehensive overview of recent advances in autoformalization from both mathematical and LLM-centric perspectives. We examine how autoformalization is applied across various mathematical domains and levels of difficulty, and analyze the end-to-end workflow from data preprocessing to model design and evaluation. We further explore the emerging role of autoformalization in enhancing the verifiability of LLM-generated outputs, highlighting its potential to improve both the trustworthiness and reasoning capabilities of LLMs. Finally, we summarize key open-source models and datasets supporting current research, and discuss open challenges and promising future directions for the field.
1 Introduction
Formalization remains labor-intensive, while LLMs can produce complex mathematical solutions whose correctness needs formal verification. This survey reviews autoformalization in mathematical theorem proving and its potential role in verifying LLM outputs.
1 Introduction
- Autoformalization targets the labor-intensive translation of informal mathematical reasoning into machine-verifiable formal language.Precision is required at every logical step.Source: §1 · p. 1
- LLM progress on mathematical problems underscores the need for formal verification of generated solutions.The passage reports silver-medal-level IMO performance by AlphaProof and a 25.2% Frontier Mathematics result for GPT-o3.Source: §1 · p. 1
- Autoformalization also applies beyond mathematics by translating informal specifications or correctness claims into formal logic or verifiable code contracts.The passage discusses possible applications in algorithm design, software engineering, security auditing, and scientific computing.Source: §1 · p. 1
- The survey reviews mathematical theorem proving and explores combining autoformalization with formal verification of LLM outputs.Its coverage includes foundations, open-source models and datasets, workflow, mathematical domains and difficulty, and future directions.Source: §1 · p. 2
2 Background
Autoformalization links mathematical formalization with formal verification of LLM-generated content. The section frames mathematical tasks by domain, difficulty, and workflow, and describes formalization as a response to costly manual effort and potentially unsound model outputs.
2 Background
- Autoformalization supports machine-verified proofs while offering a framework for grounding LLM outputs in formal logic.The section describes machine learning and formal systems as mutually supporting formalization and verification.Source: §2 · p. 2
2.1 Autoformalization in Mathematics
- Landmark formalizations illustrate the time burden: the Four Color Theorem took nearly five years, while Kepler’s Conjecture required more than a decade.Source: §2.1 · pp. 2–3
- The survey organizes mathematical autoformalization by problem domain, difficulty, and workflow, including preprocessing, modeling, post-processing, and evaluation.Difficulty ranges from high school to undergraduate and graduate-level reasoning.Source: §2.1 · p. 3
2.2 Autoformalization in LLM Output Formal Verification
- LLMs can produce factually incorrect or logically unsound outputs that are difficult to distinguish from valid reasoning.Source: §2.2 · p. 3
- Autoformalization can translate LLM outputs into formal representations, enabling symbolic reasoning and supporting correctness and reliability.The passage mentions first-order logic and Peano arithmetic as formal systems used in this work.Source: §2.2 · p. 4
3 Foundations of Progress: Techniques and Corpora
The section catalogs open-source methods, models, and datasets, and describes task categories and dataset elements used in autoformalization and theorem proving.
3 Foundations of Progress: Techniques and Corpora
- The survey collects open-source code, model parameters, and datasets, with tables describing works, benchmarks, and dataset resources.The tables identify benchmark roles and summarize dataset addresses, sizes, and descriptions.Source: §3 · p. 4
- The task taxonomy includes formal proof generation, data construction, evaluation, autoformalization, informalization, retrieval-augmented generation, and AST transformation.Source: §3 · p. 4
- Dataset elements distinguish informal and formal problem statements from informal and formal solutions.Informal statements and solutions are expressed in natural language or standard mathematical writing; formal statements and solutions use formal languages and theorem-proving tools.Source: §3 · p. 5
4 Workflow for Autoformalization and Theorem proof
The section uses open-source methods and recent research to frame an overall autoformalization workflow and examine its mechanisms across workflow links.
4 Workflow for Autoformalization and Theorem proof
- The survey builds its workflow analysis on open-source method models and recent research progress in autoformalization.Source: §4 · p. 5
- The workflow framework is intended to reveal autoformalization processes across different links.Source: §4 · p. 5
- The analysis examines the mechanisms and concerns involved in those workflow links.Source: §4 · p. 5
4.1 Data preprocessing
Data preprocessing addresses scarcity by improving the quality of available examples and expanding their quantity. The survey describes filtering, corpus expansion, and synthetic data generation as complementary approaches.
4.1 Data preprocessing
- Autoformalization data are scarce, motivating preprocessing strategies that improve quality and increase quantity.The survey identifies filtering low-quality data and adding more examples as two approaches.Source: §4.1 · p. 5
Enhanced data quality
- Model scoring and hypothesis rejection filter generated Lean4 examples judged poor or provably false, aiming to preserve logical and semantic consistency.Statements rated “fair” or “poor” are filtered; examples successfully proved despite being intended as false propositions are also removed.Source: Enhanced data quality · p. 5
Increase data quantity
- Quantity can be increased by adding formal languages, expanding repository searches, and synthesizing data.These approaches are presented as ways to address data scarcity during preprocessing.Source: Increase data quantity · p. 5
- GPT-4-generated informalizations of Isabelle and Lean4 corpora yield diverse natural-language outputs, and ablations indicate that multiple formal languages are essential for training.The approach relies on the observation that informalization is easier than formalization.Source: Increase data quantity · p. 5
- Lean4 GitHub repositories and 10,000 historical Mathlib4 commits supply expanded training data, with large-scale training reported to improve performance across mathematical problem domains.The commit-based work builds a file-level dataset from real-world commits.Source: Increase data quantity · p. 5
- Synthetic parallel corpora can be built from Mathlib concepts, informal problem statements, and teacher-generated formal proofs; disproving assumptions nearly doubles the corpus.A student model is then iteratively trained with reinforcement learning on the resulting corpus.Source: Increase data quantity · p. 5
4.2 Method
The survey reviews rule-based and LLM-based autoformalization, then describes postprocessing and evaluation methods for aligning informal inputs with formal outputs. Its examples address language flexibility, translation gaps, and distinct syntactic and semantic checks.
Rule-based Autoformalization
- Rule-based systems use explicit logical, syntactic, and semantic rules, often paired with controlled natural language; GF can parse mathematical text into abstract syntax and linearize it as Lean expressions.Examples include Mizar, NaProche, ForTheL, MathNat, and VerboseLean; the GF framework GLIF is described in.Source: Rule-based Autoformalization · pp. 5–6
LLM-based Autoformalization
- LLMs offer greater flexibility for natural-language details, and translation with fewer than five examples has been reported, although large-scale training data remains a concern.The survey also reports a 70% accuracy for informal competition-level problems versus 30% for formal ones under the same model.Source: LLM-based Autoformalization · p. 6
- Informal-to-formal translation must bridge semantic ambiguity and omitted logical steps; one cited ablation favors two-stage code and math training over simultaneous training.The simultaneous-training condition is reported as worse than direct mathematical-reasoning training, with the authors speculating that the 1.3B model could not assimilate both data types together.Source: LLM-based Autoformalization · p. 6
- Back-translation creates informal training data from formal corpora; a small-scale dataset is reported to outperform MMA and ProofNet using 1/150 of their tokens.The survey describes single-model, teacher-student, and regex-based approaches; the regex method is more interpretable but limited to simpler translations.Source: LLM-based Autoformalization · p. 6
Postprocessing
- Postprocessing targets mismatches between formal statements and informal inputs, including self-contradictory hypotheses, alignment, and proof-logic errors caused by incorrect tactics.The described approaches include hypothesis rejection, contrastive alignment, and tool or guess correction.Source: Postprocessing · pp. 6–7
Evaluatation
- Evaluation must check both formal-language type-checking and semantic equivalence, since passing a type check alone does not establish correspondence to the natural-language statement.The survey describes symbolic-equivalence and proof-feedback approaches alongside similarity, alignment, and semantic-scoring methods.Source: Evaluatation · p. 7
4.3 Therom Proof
The survey reviews tactic-level search and end-to-end proof generation as complementary developments in theorem proving. It describes new data and training strategies alongside benchmark results, with methods spanning local proof search and holistic generation.
4.3 Therom Proof
- Tactic-level methods strengthen local search and sample efficiency, while the survey presents end-to-end generation as integrating natural-language reasoning with formal proof.It frames tactic-level reasoning and search as foundational to navigating the formal proof space.Source: §4.3 · pp. 7–8, Whole-Proof Generation Methods · p. 8
Tactic Step Proving Methods
- 72.95% pass rate on Lean4 MiniF2F is reported for Bfs-prover, which uses breadth-first tree search and expert iteration.The survey says simple BFS search can be competitive under appropriately scaled conditions.Source: Tactic Step Proving Methods · p. 8
- 65% pass rate on MiniF2F and 17.0% of Lean-Workbook-Plus questions proved are reported for an expert-iteration method using critic-guided exercise selection.The approach aims to deepen search and guide exploration toward deeper proofs.Source: Tactic Step Proving Methods · p. 8
- 68.4% pass rate on benchmarks such as MiniF2F is reported for a method combining synthetic training data with guided tree search.The work also releases 30,000 synthetic proof instances pairing natural-language questions, formalized Lean statements, and proofs.Source: Tactic Step Proving Methods · p. 8
Whole-Proof Generation Methods
- Using a continuously expanded dataset of statements older Prover models failed to solve, supervised fine-tuning produced Goedel-Prover-SFT, which achieved 57.6% success on MiniF2F, 7.6% above the previous optimal model.Source: Whole-Proof Generation Methods · p. 8
- 80.7% pass rate on MiniF2F is reported for a structured formal reasoning model based on Qwen2.5-72B and large-scale reinforcement learning.The survey also reports high sampling efficiency under very low sampling conditions and a positive correlation between model size and performance.Source: Whole-Proof Generation Methods · p. 8
- 59.8% pass rate on MiniF2F is reported after continuous training on mixed data and reinforcement learning using Lean 4 compiler feedback as a reward.The method is described as improving existing proof models, including those in [Xin et al., 2024b] and.Source: Whole-Proof Generation Methods · p. 8
- 88.9% pass rate on the MiniF2F test set and 49 PutnamBench problems solved are reported for a method combining subgoal decomposition with reinforcement learning.DeepSeek V3 decomposes problems into subgoals, whose solved proofs are combined with step-wise reasoning for cold-start training.Source: Whole-Proof Generation Methods · p. 8
5 Taxonomy of Autoformalization for Mathematical Problems
The survey organizes mathematical autoformalization by problem domain and difficulty, emphasizing that different domains require adaptation to their semantic structures, input modalities, and reasoning demands. It distinguishes geometry and topology, algebra and number theory, complex or frontier problems, and increasing levels of mathematical abstraction.
5 Taxonomy of Autoformalization for Mathematical Problems
- The taxonomy classifies autoformalization by mathematical domain and problem difficulty, from high-school to graduate-level reasoning.The survey also introduces abstraction level as a dimension for analyzing mathematical problems.Source: §5 · pp. 8–9
5.1 Domain of Mathematical Problem
- Different mathematical subfields pose distinct challenges, so autoformalization must adapt to their semantic structures, input modalities, and reasoning paradigms.The survey highlights graphical reasoning in geometry and symbolic manipulation in algebra.Source: §5.1 · p. 9
Geometry and Topology Problems
- Geometry and topology problems combine text with graph information; formalization must encode implicit graphical attributes and align diagram elements with their textual meanings.The cited Euclidean-geometry approach uses a formalized system called E to extract graphical rules and model diagram reasoning.Source: Geometry and Topology Problems · p. 9
Algebra and Number Theory Problems
- Algebra and number theory formalization centers on converting variables, equations, and operation rules into symbolic logic while resolving nested structures and implicit operations.The survey contrasts these text-based challenges with geometry’s need for cross-modal alignment.Source: Algebra and Number Theory Problems · p. 9
Complex Systems and Frontier Problems
- Complex-system and frontier problems include PDE-control specifications formalized with signal temporal logic and LLMs; the cited benchmark results also show a substantial gap from human mathematical experts.The survey reports GPT-o3 at 25.2% on Frontier Math and other LLMs at 2%.Source: Complex Systems and Frontier Problems · p. 9
5.2 Difficulty Level of Mathematical Problems
- Difficulty levels rise with proof length, strategy count and type, and abstraction; high-school problems are typically structured competition problems with relatively short proofs.MiniF2F is described as containing mostly high-school Olympiad problems with clear structure and limited steps.Source: §5.2 · p. 9, High School Level · p. 9
Undergraduate Level
- Undergraduate datasets span classical fields and range from 371 Lean 3 examples in ProofNet to theorem collections that represent progression toward longer, more abstract proofs.ProofNet includes formal theorems, natural-language statements, and proofs; FormL4 draws theorems from Mathlib4 and generates informal descriptions.Source: Undergraduate Level · pp. 9–10
Graduate Level
- Graduate-level tasks draw on research papers or advanced monographs and require abstract concepts, complex proof strategies, and reasoning with incomplete context.The survey describes arXiv2Formal as containing 50 research-level theorems and Herald as a corpus of advanced mathematical proof pairs.Source: Graduate Level · p. 10
5.3 Abstraction Level of Mathematical Problems
Problem difficulty is indicated by proof length and tactic count, while abstraction provides a complementary dimension. Across educational stages, the treatment of functions shifts from procedures to logical definitions and structural properties of spaces.
5.3 Abstraction Level of Mathematical Problems
- Proof length and tactic count indicate difficulty across educational levels, while abstraction offers a complementary way to distinguish problems.The section illustrates abstraction through the concept of a group, which captures shared structure across instances such as symmetries.Source: §5.3 · p. 10
Procedural Abstraction in High School Mathematics
- High school mathematics treats functions procedurally, relying on concrete examples and techniques such as computing a quadratic’s discriminant or differentiating to show monotonicity.Functional properties are often verified by direct algebraic manipulation tied to numerical values.Source: Procedural Abstraction in High School… · p. 10
Logical Abstraction in University Mathematics
- University mathematics raises abstraction from numerical procedures to rigorous definitions and logical derivations, as in the formal treatment of limits.The limit shifts from numerical approximation toward symbolic logic, decoupled from concrete numerical values.Source: Logical Abstraction in University… · p. 10
Structural Abstraction in Graduate Mathematics
- Graduate mathematics treats functions as elements of abstract spaces and reasons about properties such as completeness, compactness, and duality.Examples include Lp spaces of p-integrable functions and ℓp spaces of p-summable sequences.Source: Structural Abstraction in Graduate… · p. 10
6 Connecting LLM Outputs and Formal Verification via Autoformalization
Autoformalization links informal LLM outputs to formal representations that verification frameworks can check. The section surveys code-validation approaches alongside applications in medicine and LLM output verification.
6 Connecting LLM Outputs and Formal Verification via Autoformalization
- Autoformalization translates informal LLM outputs into formal representations suitable for verification using frameworks such as first-order or higher-order logic.The section describes this translation as a bridge between LLM reasoning and formal verification.Source: §6 · p. 11
6.1 Code validation
- Generated code remains difficult to verify, despite its importance for execution; software failures in the US are estimated to cost trillions of dollars annually.The section identifies code verification as traditional research content in formal verification of LLM outputs.Source: §6.1 · p. 11
Non-interactive validation
- Non-interactive validation includes static analysis and dependency graphs, as well as generated assertions and two-phase specification refinement through verifier dialogue and mutation [Ma et al., 2024].Dependency graphs encode control-flow, state, and type dependencies; assertions check expected outputs or program states.Source: Non-interactive validation · p. 11
- Loopy generates candidate loop invariants with an LLM, verifies them using a symbolic tool such as Frama-C, and repairs incorrect candidates [Kamath et al., 2023].Invariants describe properties that hold at each loop iteration, enabling local checks of loop correctness.Source: Non-interactive validation · p. 11
LLM interactive verification
- Interactive verification uses validator feedback to filter programs; examples include translating Dafny code to Verus with tree search [Aggarwal et al., 2024] and prompting optimization from static-analysis dependencies [Liao et al., 2025].The section also describes interactive theorem provers based on first-order or higher-order logic and type systems.Source: LLM interactive verification · p. 11
6.2 Medicine Domain
- In medicine, binary relations represent associations among disease, gene, and drug terms, while biomedical ontologies serve as criteria for checking term identity [Hamed et al., 2025].Terms absent from an ontology are classified as unverified.Source: §6.2 · p. 12
6.3 LLM output verification
- LLM output-verification work includes self-validation used to filter or reweight data and SymGen’s symbolic references linking natural-language text to structured data fields [Hennigen et al., 2023].SymGen references support data-source traceability and subsequent formal verification and maintenance.Source: §6.3 · p. 12
7 Open Challenges and Future Dirctions
The survey identifies data scarcity, generalization, and system design as challenges for autoformalization, alongside a longer-term goal of creative mathematical reasoning.
7 Open Challenges and Future Dirctions
- Autoformalization lacks large, diverse parallel corpora of aligned informal and formal mathematics, with LeanWorkbook at 4.8MB cited as a small resource.The survey points to scalable collection, synthetic data, and human-in-the-loop annotation as possible ways to address this scarcity.Source: §7 · p. 12
- Future systems should formalize larger, more abstract theories and generalize compositionally across domains with minimal supervision rather than rely on costly full retraining [Wu et al., 2022].The survey also calls for tighter integration with formal verification frameworks.Source: §7 · p. 12
- More interactive, modular systems could combine LLMs with symbolic reasoning, proof assistants, and logic-based verifiers to provide more controllable and interpretable outputs.Users could guide or verify parts of the process as needed.Source: §7 · p. 12
- The long-term vision is creative mathematical reasoning: systems that verify proofs, propose conjectures, explore ideas, and assist mathematicians in discovering research directions.The survey says progress will require work across language understanding, formal logic, mathematical modeling, and human-AI collaboration.Source: §7 · p. 12
8 Different with Other Survey
This survey extends prior work on autoformalization models by examining the broader workflow and the role of formal verification for LLMs. It approaches the topic through both mathematical problems and LLM verification.
8 Different with Other Survey
- Building on prior classifications of rule-based and neural or LLM-based methods [Yang et al., 2024], the survey examines the full workflow, including preprocessing, post-processing, and result verification.It contrasts this scope with prior surveys focused on classifying and describing model methods [Yang et al., 2024; Li et al., 2024b].Source: §8 · pp. 12–13
- The survey also examines autoformalization for formal verification of LLMs, emphasizing its potential relevance to credibility and reasoning capabilities.It distinguishes this focus from work centered on formal theorem-proving development [Blaauwbroek et al., 2024].Source: §8 · p. 13