Autoformalization with Large Language Models

By Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Norman Rabe, Charles Staats, Mateja Jamnik, Christian Szegedy. 2022

324 citations recorded by the source corpus.

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\%$.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Information Systems, Natural Language Processing, Program Analysis & Verification

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Information Systems

In Natural Language Processing

In Program Analysis & Verification

Citations in the corpus

Augmented Language Models: a Survey (2023, methodology): “…al., 2019), or solve the sub-problems sequentially, where the solution to the next sub-problem depends on the answer to the previous ones (Yang et al., 2022a; Zhou et al., 2022; Drozdov et al., 2022; Dua et al., 2022; Khot et al., 2022; Wang et al., 2022a; Wu et al., 2022b; Mishra and Nouri, 2022).”
Llemma: An Open Language Model For Mathematics (2023, methodology): “This includes synthesizing proofs via tactic prediction (Polu & Sutskever, 2020; Han et al., 2022; Lample et al., 2022; Jiang et al., 2022), autoformalization (Wu et al., 2022; Jiang et al., 2023), and integrated tools (Welleck & Saha, 2023).”
PAL: Program-aided Language Models (2022, background): “…a wide range of reasoning tasks, including commonsense (Wei et al., 2021; Sanh et al., 2021; Madaan et al., 2022), mathematical (Lewkowycz et al., 2022; Wu et al., 2022; Mishra et al., 2022), and symbolic reasoning (Yao et al., 2022; Ahn et al., 2022), using few-shot prompting (Brown et al., 2020).”
Reasoning with Language Model Prompting: A Survey (2022, background): “, 2022), collaborating LMs and codes to tackle specific tasks has recently sprung up (Wang et al., 2022e; Cheng et al., 2022; Wu et al., 2022b).”
A Survey of Large Language Models (2023, unknown): “help LLMs generate more accurate results [143, 144].”
Teaching Algorithmic Reasoning via In-context Learning (2022, background): “In addition to this class of benchmarks, formal mathematics in the form of theorem-proofs (Rabe et al., 2020; Li et al., 2020; Polu and Sutskever, 2020; Welleck et al., 2021; Jiang et al., 2022; Wu et al., 2022) has been considered extensively.”
A Survey of Deep Learning for Mathematical Reasoning (2022, unknown): “Recent work (Wu et al., 2021d; Krishna et al., 2021; Ri and Tsuruoka, 2022; Anderson and Farrell, 2022; Wu et al., 2022c) shows that pre-training on data that is fully synthetically generated—synthetic pre-training can actually provide substantial gains.”
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics (2023, methodology): “Language-model-based theorem provers and autoformalization systems have typically been evaluated on benchmarks consisting of competition and olympiad-style problems [Zheng et al., 2022, Wu et al., 2022a].”
Neurosymbolic Program Synthesis (unknown): “As for specification, LLMs have been successfully used in the autoformalization of informal mathematical statements [46].”
Language Models of Code are Few-Shot Commonsense Learners (2022, methodology): “Our work is similar in spirit to Wu et al. (2022), and seeks to leverage the dual abilities of Code-LLMs for text and symbolic reasoning.”
Baldur: Whole-Proof Generation and Repair with Large Language Models (2023, methodology): “LLMs have shown promise for autoformalization of specifications, and automatically generated proofs of the resulting autofor-malized specifications have been used to improve a neural theorem prover on a widely used benchmark suite in Isabelle/HOL [101].”
CRANE: Reasoning with constrained LLM generation (2025, unknown): “…systems that interact with traditional software tools like Python interpreters (OpenAI, 2024; Chen et al., 2023) for code generation (Suresh et al., 2024a;b; Jiang et al., 2024), logical solvers (Pan et al., 2023; Olaus-* son et al., 2023), and theorem provers (Wu et al., 2022; Yang et al., 2023).”