Baldur: Whole-Proof Generation and Repair with Large Language Models

By Emily First, Markus Norman Rabe, Talia Ringer, Yuriy Brun. 2023

195 citations recorded by the source corpus.

Formally verifying software is a highly desirable but labor-intensive task. Recent work has developed methods to automate formal verification using proof assistants, such as Coq and Isabelle/HOL, e.g., by training a model to predict one proof step at a time and using that model to search through the space of possible proofs. This paper introduces a new method to automate formal verification: We use large language models, trained on natural language and code and fine-tuned on proofs, to generate whole proofs at once. We then demonstrate that a model fine-tuned to repair generated proofs further increasing proving power. This paper: (1) Demonstrates that whole-proof generation using transformers is possible and is as effective but more efficient than search-based techniques. (2) Demonstrates that giving the learned model additional context, such as a prior failed proof attempt and the ensuing error message, results in proof repair that further improves automated proof generation. (3) Establishes, together with prior work, a new state of the art for fully automated proof synthesis. We reify our method in a prototype, Baldur, and evaluate it on a benchmark of 6,336 Isabelle/HOL theorems and their proofs, empirically showing the effectiveness of whole-proof generation, repair, and added context. We also show that Baldur complements the state-of-the-art tool, Thor, by automatically generating proofs for an additional 8.7% of the theorems. Together, Baldur and Thor can prove 65.7% of the theorems fully automatically. This paper paves the way for new research into using large language models for automating formal verification.

Subfields: Artificial Intelligence, Information Systems, Software, LLM Agents & Tool Use

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Information Systems

In Software

In LLM Agents & Tool Use

Kaiyu Yang

Citations in the corpus

Llemma: An Open Language Model For Mathematics (2023, neutral): “Due to high computational costs of search, language models applied to this domain have traditionally been small, but recent work has demonstrated promise in the use of larger models (First et al., 2023; Jiang et al., 2023).”
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models (2023, methodology): “All existing LLM-based provers pretrain on datasets specific to math and coding [14–20].”
Can Transformers Learn to Solve Problems Recursively? (2023, background): “But how sturdy are these foundations? At the core of many of these tools are transformer-based large language models [4, 5, 13].”