# Autoformalization with Large Language Models

Preprint · Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, Christian Szegedy

- Archive id: arxiv:2205.12615
- Published: 2022-05-25
- arXiv: https://arxiv.org/abs/2205.12615
- Citations: 62
- Source URL: https://arxiv.org/abs/2205.12615
- PDF: https://arxiv.org/pdf/2205.12615
- Provenance: arxiv+openalex

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

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

Topics: [AI for Mathematics & Formal Proof](https://space-kitty.com/topics/ai-mathematics)

Cited in dossiers:
- [AI for Mathematics & Formal Proof: State of the Field (October 2026)](https://space-kitty.com/dossiers/ai-mathematics)

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.