Autoformalization with Large Language Models

TL;DR

This paper demonstrates that large language models can effectively autoformalize a significant portion of mathematical problems, improving theorem proving performance and advancing the field of automated formalization.

Contribution

It shows that LLMs can accurately translate natural language mathematics into formal specifications, achieving state-of-the-art results in theorem proving benchmarks.

Findings

LLMs can correctly autoformalize 25.3% of problems.

Autoformalization improves neural theorem prover performance.

State-of-the-art proof rate of 35.2% on MiniF2F.

Abstract

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