Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Proof Automation with Large Language Models

Minghai Lu, Benjamin Delaware, Tianyi Zhang

TL;DR

Formal proof automation in Coq remains costly due to the need for precise low-level proof steps. This work identifies common LLM errors in formal proofs through a formative study and introduces PALM, a generate-then-repair framework that combines retrieval-augmented proof generation with targeted symbolic repairs and backtracking. PALM substantially outperforms state-of-the-art baselines on the CoqGym benchmark and generalizes across LLMs of varying sizes, with ablations showing the importance of premise retrieval, repair mechanisms, and backtracking. The approach offers a practical path to scalable, model-agnostic formal verification by integrating LLM-driven generation with rigorous symbolic tooling.

Abstract

Interactive theorem provers such as Coq are powerful tools to formally guarantee the correctness of software. However, using these tools requires significant manual effort and expertise. While Large Language Models (LLMs) have shown promise in automatically generating informal proofs in natural language, they are less effective at generating formal proofs in interactive theorem provers. In this paper, we conduct a formative study to identify common mistakes made by LLMs when asked to generate formal proofs. By analyzing 520 proof generation errors made by GPT-3.5, we found that GPT-3.5 often identified the correct high-level structure of a proof, but struggled to get the lower-level details correct. Based on this insight, we propose PALM, a novel generate-then-repair approach that first prompts an LLM to generate an initial proof and then leverages targeted symbolic methods to iteratively repair low-level problems. We evaluate PALM on a large dataset that includes more than 10K theorems. Our results show that PALM significantly outperforms other state-of-the-art approaches, successfully proving 76.6% to 180.4% more theorems. Moreover, PALM proves 1270 theorems beyond the reach of existing approaches. We also demonstrate the generalizability of PALM across different LLMs.

Proof Automation with Large Language Models

TL;DR

Formal proof automation in Coq remains costly due to the need for precise low-level proof steps. This work identifies common LLM errors in formal proofs through a formative study and introduces PALM, a generate-then-repair framework that combines retrieval-augmented proof generation with targeted symbolic repairs and backtracking. PALM substantially outperforms state-of-the-art baselines on the CoqGym benchmark and generalizes across LLMs of varying sizes, with ablations showing the importance of premise retrieval, repair mechanisms, and backtracking. The approach offers a practical path to scalable, model-agnostic formal verification by integrating LLM-driven generation with rigorous symbolic tooling.

Abstract

Interactive theorem provers such as Coq are powerful tools to formally guarantee the correctness of software. However, using these tools requires significant manual effort and expertise. While Large Language Models (LLMs) have shown promise in automatically generating informal proofs in natural language, they are less effective at generating formal proofs in interactive theorem provers. In this paper, we conduct a formative study to identify common mistakes made by LLMs when asked to generate formal proofs. By analyzing 520 proof generation errors made by GPT-3.5, we found that GPT-3.5 often identified the correct high-level structure of a proof, but struggled to get the lower-level details correct. Based on this insight, we propose PALM, a novel generate-then-repair approach that first prompts an LLM to generate an initial proof and then leverages targeted symbolic methods to iteratively repair low-level problems. We evaluate PALM on a large dataset that includes more than 10K theorems. Our results show that PALM significantly outperforms other state-of-the-art approaches, successfully proving 76.6% to 180.4% more theorems. Moreover, PALM proves 1270 theorems beyond the reach of existing approaches. We also demonstrate the generalizability of PALM across different LLMs.
Paper Structure (30 sections, 15 figures, 4 tables, 2 algorithms)

This paper contains 30 sections, 15 figures, 4 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Interactive Theorem Proving in Coq
  4. Hammers
  5. Formative Study
  6. Approach
  7. The Overall Algorithm
  8. Premise Retrieval
  9. Prompt Design
  10. Repair Mechanisms
  11. Backtracking
  12. Evaluation
  13. Comparison baselines
  14. Benchmark construction
  15. Results
  16. ...and 15 more sections

Figures (15)

  • Figure 1: A Coq theorem stating that natural number addition is commutative, and a proof of this statement.
  • Figure 2: Proof state after the execution of each tactic in the proof of addition's commutativity.
  • Figure 3: apply H causes a wrong theorem application: "Unable to unify 'm=n' with 'n=m' ".
  • Figure 4: Overview of PALM.
  • Figure 5: rewrite H2 fails with: "Found no subterm matching 'b' in the current goal".
  • ...and 10 more figures