Source-linked AI summary
Autoformalization with Large Language Models
Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, Christian Szegedy
TL;DR
The paper addresses whether LLMs can translate natural-language mathematics into formal specifications despite scarce formal mathematics and aligned training data. It uses in-context LLM autoformalization and feeds resulting theorems into neural theorem-prover training. LLMs produced perfect formalizations for a significant subset of evaluated problems, while expert iteration raised MiniF2F test success to 35.2%.
Problem
Formal mathematics and aligned natural-language/formal data are scarce, leaving the feasibility of LLM-based autoformalization unclear despite its potential value for formal verification and automated reasoning.
Method
The paper prompts LLMs with example formalizations, evaluates generated Isabelle statements, and uses successful autoformalized theorems as training data for neural theorem-prover expert iteration.
Results
35.2% MiniF2F test success was achieved after two expert iterations, while 38 of 150 randomly evaluated formalizations were perfect.
Takeaways & Limitations
Autoformalized statements are generally possible with LLMs and can provide useful training data for improving automated neural provers.
Takeaways & Limitations
The static-model approach is limited to fairly small pieces of formal mathematics because whole large theories exceed current LLM context windows.
Abstract
from arXiv · showhide
Autoformalization is the process of automatically translating from natural language mathematics to formal specifications and proofs. A successful autoformalization system could advance the fields of formal verification, program synthesis, and artificial intelligence. While the long-term goal of autoformalization seemed elusive for a long time, we show large language models provide new prospects towards this goal. We make the surprising observation that LLMs can correctly translate a significant portion ($25.3\%$) of mathematical competition problems perfectly to formal specifications in Isabelle/HOL. We demonstrate the usefulness of this process by improving a previously introduced neural theorem prover via training on these autoformalized theorems. 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\%$.
1 Introduction
Autoformalization aims to translate natural-language mathematics into formal languages, but scarce aligned data makes its feasibility unclear. This work finds that LLMs can perform substantial autoformalization and improve neural theorem proving.
- Autoformalization automatically translates natural-language mathematics into a formal language.
- Successful autoformalization could reduce formalization costs and connect automated reasoning fields with mathematics written in natural language.
- Formal mathematics data is scarce, and almost no aligned natural-language/formal-mathematics data exists for training.
- LLMs produced 38 perfect formalizations among 150 randomly selected formalizations evaluated manually.
- Fine-tuning a neural theorem prover on autoformalized theorems increased MiniF2F test success to 35.2%.
2 Related Work
Prior work addressed theorem-proving data scarcity through alternative learning signals, synthetic formulas, and translation methods. This paper differs by using self-supervised LLMs to autoformalize theorems rather than relying on synthetic generated data.
- Earlier machine-learning approaches guided theorem provers and interactive proof assistants, with DeepMath initiating renewed interest.
- Researchers addressed data scarcity using reinforcement learning, hindsight experience replay, and synthetic formulas.
- Prior supervised autoformalization relied on synthetic natural-looking data generated by the Mizar theorem prover.
- This work uses models trained through self-supervised language modeling rather than models trained specifically for autoformalization.
3 Background
Interactive theorem provers provide automatically checkable formal statements and proofs, but complex formalization remains laborious. LLM in-context learning offers a way to specify autoformalization through examples.
- Interactive theorem provers enable formal statements and proofs to be checked automatically for correctness.
- Formalizing complex mathematical and computer-science results with interactive theorem provers typically requires many years of specialist work.
- Automation of logic has reached commercial applications mainly in narrow domains such as chip design and operating-system driver verification.
- LLMs are trained to predict the next word from arbitrary text and can generate high-quality text after training on hundreds of billions of words.
- In-context learning lets LLMs learn tasks from patterns in the current input context.
- Autoformalization can be specified by providing a few example formalizations as prompts.
4 Autoformalization for Mathematical Competition Problems
The section evaluates LLM autoformalization of mathematical competition problems into Isabelle using few-shot prompts, case studies, BLEU comparisons, and manual failure analysis. Results show strong but scale- and definition-sensitive performance, including perfect formalizations and systematic failure modes.
- Method: LLMs are prompted to translate English mathematical statements into Isabelle code, treating autoformalization as machine translation between natural language and formal mathematics.The study focuses on competition problems, where Isabelle libraries often already contain the required background theory and definitions.
- Case Studies: Few-shot examples can provide concepts indirectly: after seeing an example explaining a line, Codex correctly formalizes a previously failed linear-function problem.The added example is tangentially related and does not mention “linear function” explicitly.
- BLEU for Model Comparisons: BLEU scores consistently improve as PaLM scales from 8B to 540B for both subjects, while Codex scores higher than PaLM.The authors suggest Codex’s stronger performance may relate to its greater exposure to formal data during training.
- Human Evaluation of Failure Cases: 38 of 150 Codex translations are perfect, yielding a 25.3% success rate; common failures involve misaligned definitions, factorial notation, and function application.Examples include failing to map “greatest possible value” to Isabelle’s Greatest/Max and !n to fact n.
5 Autoformalization for Neural Theorem Proving
The paper combines LLM-generated formal problem statements with expert iteration to improve neural theorem proving. Starting from Thor, it uses verified proofs from autoformalized theorems as additional training data and achieves higher miniF2F proof success rates.
- 5.1 Expert Iteration with Autoformalization: The method uses LLMs to autoformalize theorems, then uses successful proof searches to kick off an expert-iteration self-improvement cycle.The prover repeatedly searches for proofs, collects verified successes, and uses them as new training data.
- 5.2 Neural Theorem Provers: Thor is initialized as the base Isabelle neural theorem prover, trained on the PISA dataset containing 2.49 million proof steps.Proof search uses Sledgehammer in Isabelle with a 30 second timeout.
- 5.3 Result: Codex produces 3363 syntactically correct autoformalized theorems from 3908 MATH training problems, which are then used for expert iteration.The problems cover algebra, intermediate algebra, and number theory.
- 5.3 Result: The first expert iteration increases miniF2F success rates from 28.3% to 36.1% on validation and from 29.9% to 34.0% on test.These gains are reported relative to the base model M0.
- 5.3 Result: A second iteration raises miniF2F success rates to 37.3% on validation and 35.2% on test, exceeding the previous state of the art by 5.6%.Successful proofs from all iterations are deduplicated by problem statement before training.
6 An Outlook on Autoformalizing Advanced Mathematics
The paper examines autoformalization beyond competition problems, where advanced mathematical statements require more contextual definition alignment. In this setting, informalization from Isabelle to natural language achieves higher reported success than formalization.
- 6.1 Autoformalization: from Natural Language to Isabelle: Advanced mathematical statements add contextual information that obscures alignment between informal and formal definitions.The paper treats theorem statements rather than full proofs, so definition alignment is the main challenge.
- 6.1 Autoformalization: from Natural Language to Isabelle: A typical failure confuses products of numbers, sets, and topological spaces, omitting the index-set context needed for the correct Isabelle conclusion.The correct conclusion is compact_space (product_topology X I), with I introduced in the fixes and assumes sections.
- 6.2 Informalization: from Isabelle to Natural Language: The authors argue that stronger informalization performance supports backtranslation-style algorithms for advanced mathematics.Informal statements are easier for humans to comprehend and can be aligned with formal statements to create data.
- 6.2 Informalization: from Isabelle to Natural Language: Among 38 advanced formal statements, Codex produced 36 reasonably coherent informalizations, including 29 judged more-or-less correct.The reported 76% success rate exceeds the 25% formalization success rate used for comparison.
7 Discussion
The discussion presents autoformalization as generally possible with LLMs and as a source of training data for neural theorem provers. It also identifies context-window and theory-size constraints that limit current systems.
- Promise of Autoformalization with LLMs: Automated formalization is generally possible even with language models not trained specifically for the task.The paper frames this as evidence for the promise of autoformalization with LLMs.
- Promise of Autoformalization with LLMs: Autoformalized statements can provide training data that improves the reasoning capabilities of automated neural provers.This connects formalization with a potential feedback loop between formalization and formal reasoning.
- Limitations and future directions: Current systems are limited to fairly small pieces of formal mathematics because whole large theories exceed available context windows.Formalizing entire theories, including their definitions, requires new research ideas such as retrieval-augmented or continuous-training approaches.
- Discussion: The examples translate diverse competition problems into Isabelle statements involving algebra, geometry, functions, complex numbers, modular arithmetic, and number theory.The supplied examples include both natural-language prompts and corresponding Isabelle assumptions and conclusions.
B.1 Case Study 1
This case study reports model outputs for translating mathematical statements into Isabelle. The examples include both structurally correct formalizations and outputs with syntactic errors.
- B.1 Case Study 1: PaLM 540B generally recovered the structure of the target formalization but made syntactical errors.The passage describes the model output directly.
- B.1 Case Study 1: One target statement asks for an Isabelle formalization proving that no function on non-negative integers satisfies f(f(n)) = n + 1987.The corresponding formal target concludes false under that assumption.
- B.1 Case Study 1: The case-study materials compare outputs from PaLM models of different sizes on natural-language mathematical prompts.The supplied examples include congruence reasoning and logarithmic equations.
B.3 Case Study 3
This case study shows that a tangential example explaining how to formalize a line enables Codex to formalize a linear-function problem perfectly. The result highlights the role of few-shot examples in aligning informal concepts with Isabelle representations.
- B.3 Case Study 3: Codex perfectly formalized the linear-function problem after receiving an additional example showing how to formalize a line.The additional example states a linear relation through formal assumptions and a conclusion.
- B.3 Case Study 3: The added prompt example was only tangentially related and did not mention the phrase “linear function.”It nevertheless supplied enough information for the model to understand the intended formalization.
C.1 Perfect Translations
The examples show LLMs translating diverse natural-language mathematics into Isabelle statements that preserve assumptions, definitions, and conclusions. The formalizations cover algebra, geometry, number theory, sequences, and complex numbers.
- The translations formalize elementary geometry, including line intersections, distances, and coordinate-based movement.Examples encode geometric constraints and derive the stated answers in Isabelle.
- The examples encode algebraic problems involving polynomial iteration, functional equations, and integer division.Formal statements preserve equations, divisibility operations, quotient and remainder conditions, and cardinality conclusions.
- The translations represent complex-number equations and solution sets, including fourth roots and integer-norm constraints.The Isabelle statements use complex arithmetic, disjunctions, and membership of norms in the integers.
- A sequence problem is translated using a universally quantified summation condition and a conclusion about the initial term.The Isabelle statement expresses the recurrence-like identity for every n ≥ 2.
- Number-theoretic formalizations capture perfect-square divisors, modular arithmetic, decimal digits, and divisor-count definitions.The examples use cardinality, divisibility, modular reduction, and least/greatest operators to express the problems.
C.2 Incorrect Translations
Incorrect translations arise from missing assumptions, type and syntax errors, omitted definitions, misapplied functions, and failures to align natural-language concepts with Isabelle.
- Type errors can change a finite natural-number summation into an invalid real-interval interpretation.The corrected statement requires explicit conversion using of_int N; otherwise the displayed sum evaluates to 0 rather than 8204.
- Some translations omit specialized definitions, such as the requirement that factors be three-digit palindromes.The resulting assumptions constrain the factor range and product but do not encode palindromicity.
- Syntactic mistakes include operator-precedence errors that alter the meaning of an arithmetic expression.The correction places parentheses around 3 ^2 in the expression for x.
- The failures include omitted or incorrect assumptions, such as dropping a divisor condition, a function-mapping condition, or a universal quantifier.Examples include the Brouwer statement, the custom operation Z, and an incorrectly modeled smallest-divisible integer problem.
- The inspected Brouwer translation omits the critical requirement that f maps S to itself.It also uses a real normed vector space rather than the stated Euclidean or Banach-space setting.
D.2 Informalization
Informalization translates Isabelle statements from topology, analysis, and complex analysis back into natural-language mathematical claims. The examples include standard definitions, compactness results, continuity, connectedness, and winding-number theorems.
- Codex outputs natural-language statements for standard topological definitions and closure properties.Examples cover openness, continuous maps, compactness, closed subsets, and compact images under continuous functions.
- The outputs express connectedness through separation conditions and preservation under unions of connected sets.They describe equivalent formulations involving nonempty separated subsets and families of connected sets.
- Codex verbalizes complex-analysis results involving winding numbers, holomorphic functions, and dense images.Examples include homotopy invariance, simple closed-path winding values, Casorati–Weierstrass behavior, and limits near isolated points.
- The model correctly informalizes Brouwer’s fixed-point theorem as a continuous map from a compact convex set to itself having a fixed point.This output matches the formal assumptions listed for compactness, convexity, continuity, nonemptiness, and image containment.
- Additional outputs state Jordan-curve separation, product-topology connectedness, and a series identity from the standard Isabelle libraries.These examples extend informalization beyond elementary topology into geometric topology and analysis.