Proof Automation with Large Language Models

TL;DR

This paper introduces PALM, a generate-then-repair method that enhances LLM-based formal proof generation, significantly increasing success rates and proving theorems beyond previous capabilities.

Contribution

The paper presents PALM, a novel approach combining LLMs with symbolic repair techniques to improve formal proof automation in interactive theorem provers.

Findings

PALM outperforms existing methods in theorem proving success rates.

PALM proves 1270 theorems beyond current approaches.

The approach is effective across different LLMs.

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.