Autoformalization with Large Language Models

2022/05/25 by Yuhuai Wu, Wu, Yuhuai, Albert Q. Jiang +11 · 34 citations
Computer Science · #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Machine Learning (cs.LG) #Mathematics, Computing, and Information Processing #Software Engineering (cs.SE) #Software Engineering Research

paper · pdf · doi:10.48550/arxiv.2205.12615

openalex publication_date 2022/05/25 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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

Cited by

• Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
• Translating Informal Proofs into Formal Proofs Using a Chain of States
• AutoICE: Automatically Synthesizing Verifiable C Code via LLM-driven Evolution
• When Do Symbolic Solvers Enhance Reasoning in Large Language Models?
• IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch
• Spark-Prover-X1: Formal Theorem Proving Through Diverse Data Training
• Towards Autoformalization of LLM-generated Outputs for Requirement Verification
• A Neurosymbolic Approach to Natural Language Formalization and Verification
• Synergy over Discrepancy: A Partition-Based Approach to Multi-Domain LLM Fine-Tuning
• miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward
• Reasoning Planning for Language Models
• RLMEval: Evaluating Research-Level Neural Theorem Proving
• Simulation to Rules: A Dual-VLM Framework for Formal Visual Planning
• MedRule-KG: A Knowledge-Graph--Steered Scaffold for Mathematical Reasoning with a Lightweight Verifier
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization
• ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings
• TopoAlign: A Framework for Aligning Code to Math via Topological Decomposition
• ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization
• Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers
• StatEval: A Comprehensive Benchmark for Large Language Models in Statistics
• Lean Finder: Semantic Search for Mathlib That Understands User Intents
• Autoformalizer with Tool Feedback
• Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph
• Aristotle: IMO-level Automated Theorem Proving
• ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity
• Abductive Logical Rule Induction by Bridging Inductive Logic Programming and Multimodal Large Language Models
• Can Large Language Models Autoformalize Kinematics?
• Handling Open-Vocabulary Constructs in Formalizing Specifications: Retrieval-Augmented Parsing with Expert Knowledge
• Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem
• Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs
• FormaRL: Enhancing Autoformalization with no Labeled Data
• Requirements Development and Formalization for Reliable Code Generation: A Multi-Agent Vision
• Automated Formalization via Conceptual Retrieval-Augmented LLMs
• Thinking Machines: Mathematical Reasoning in the Age of LLMs

Related

• Autoformalization in the Era of Large Language Models: A Survey
• Towards a Common Framework for Autoformalization
• Multilingual Mathematical Autoformalization
• FMC: Formalization of Natural Language Mathematical Competition Problems
• Lean-ing on Quality: How High-Quality Data Beats Diverse Multilingual Data in AutoFormalization