Laurel: Unblocking Automated Verification with Large Language Models

TL;DR

Laurel leverages large language models with specialized prompts to automatically generate assertions, significantly improving automated proof verification in Dafny by reducing manual effort and increasing success rates.

Contribution

This paper introduces Laurel, a novel tool that uses domain-specific prompting techniques with LLMs to automatically generate assertions for program verification, enhancing automation in proof systems.

Findings

Laurel achieves over 56.6% success in generating required assertions.

The techniques improve LLM effectiveness with minimal attempts.

Laurel reduces manual effort in proof verification.

Abstract

Program verifiers such as Dafny automate proofs by outsourcing them to an SMT solver. This automation is not perfect, however, and the solver often requires hints in the form of assertions, creating a burden for the proof engineer. In this paper, we propose Laurel, a tool that alleviates this burden by automatically generating assertions using large language models (LLMs). To improve the success rate of LLMs in this task, we design two domain-specific prompting techniques. First, we help the LLM determine the location of the missing assertion by analyzing the verifier's error message and inserting an assertion placeholder at that location. Second, we provide the LLM with example assertions from the same codebase, which we select based on a new proof similarity metric. We evaluate our techniques on our new benchmark DafnyGym, a dataset of complex lemmas we extracted from three real-world Dafny codebases. Our evaluation shows that Laurel is able to generate over 56.6\% of the required assertions given only a few attempts, making LLMs an affordable tool for unblocking program verifiers without human intervention.