Laurel: Generating Dafny Assertions Using Large Language Models
CoRR(2024)
Abstract
Dafny is a popular verification language, which automates proofs by
outsourcing them to an SMT solver. This automation is not perfect, however, and
the solver often requires guidance in the form of helper assertions creating a
burden for the proof engineer. In this paper, we propose Laurel, a tool that
uses large language models (LLMs) to automatically generate helper assertions
for Dafny programs. 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
lemma similarity metric. We evaluate our techniques on a dataset of helper
assertions we extracted from three real-world Dafny codebases. Our evaluation
shows that Laurel is able to generate over 50
assertions given only a few attempts, making LLMs a usable and affordable tool
to further automate practical program verification.
MoreTranslated text
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined