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

**Authors:** Emily First, Markus N. Rabe, Talia Ringer, Yuriy Brun  
**arXiv:** [2303.04910](https://arxiv.org/abs/2303.04910)  
**Date:** 2023-03-08  
**Summary page:** https://www.summarizepaper.com/en/paper/2303.04910v2/

## Key points

- Introduction of a novel method for automating formal verification in software properties
- Proposal of leveraging large language models trained on natural language text, code, and fine-tuned on proofs
- Generation of whole proofs for theorems at once instead of step-by-step generation
- Combination of proof generation model with a fine-tuned repair model to fix issues in generated proofs
- Demonstration that whole-proof generation using transformers is as effective as search-based techniques without costly search operations
- Introduction of additional context to the learned model, such as prior failed proof attempts and associated error messages, leading to improved proof repair and automated proof generation
- Establishment of a new state-of-the-art for fully automated proof synthesis
- Development and evaluation of a prototype called Baldur on a benchmark comprising 6,336 Isabelle/HOL theorems and their corresponding proofs
- Comparison with an existing tool called Thor, showing that Baldur can automatically generate proofs for an additional 8.7% of the theorems compared to Thor
- Achievement of full automation in proving 65.7% of the considered theorems by combining Baldur and Thor
- Opening up new avenues for utilizing large language models in automating formal verification and streamlining software development processes.

## Summary

The paper titled "Baldur: Whole-Proof Generation and Repair with Large Language Models" introduces a novel method for automating formal verification in software properties. The task of formally verifying software properties is highly desirable but requires significant manual effort. Previous work has explored the use of proof assistants like Coq and Isabelle/HOL to automate formal verification by training models to predict individual proof steps and searching through possible proofs. In this paper, the authors propose a new approach that leverages large language models trained on natural language text, code, and fine-tuned on proofs. Instead of generating proofs one step at a time, their method enables the generation of whole proofs for theorems at once. To further enhance the proving power, they combine this proof generation model with a fine-tuned repair model to fix any issues in the generated proofs. The main contributions of this research are as follows
(1) The demonstration that whole-proof generation using transformers is not only feasible but also as effective as search-based techniques without requiring costly search operations. (2) The introduction of additional context to the learned model, such as prior failed proof attempts and associated error messages, which leads to improved proof repair and automated proof generation. (3) The establishment of a new state-of-the-art for fully automated proof synthesis. To validate their approach, the authors develop a prototype called Baldur and evaluate it on a benchmark comprising 6,336 Isabelle/HOL theorems and their corresponding proofs. Through empirical analysis, they demonstrate the effectiveness of whole-proof generation, repair capabilities, and added context. Additionally, they compare Baldur with an existing tool called Thor and show that Baldur can automatically generate proofs for an additional 8.7% of the theorems compared to Thor. Together,BaldurandThorachieve full automation in proving 65.7% of the considered theorems. This research opens up new avenues for utilizing large language models in automating formal verification. By leveraging the capabilities of these models, the labor-intensive task of formal verification can be significantly streamlined, leading to more efficient software development processes.