Markus N. Rabe

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

2023

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 …