Laurel: Unblocking Automated Verification with Large Language Models
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866909523160072192 |
|---|---|
| author | Mugnier, Eric Gonzalez, Emmanuel Anaya Jhala, Ranjit Polikarpova, Nadia Zhou, Yuanyuan |
| author_facet | Mugnier, Eric Gonzalez, Emmanuel Anaya Jhala, Ranjit Polikarpova, Nadia Zhou, Yuanyuan |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_16792 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Laurel: Unblocking Automated Verification with Large Language Models Mugnier, Eric Gonzalez, Emmanuel Anaya Jhala, Ranjit Polikarpova, Nadia Zhou, Yuanyuan Logic in Computer Science Artificial Intelligence 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. |
| title | Laurel: Unblocking Automated Verification with Large Language Models |
| topic | Logic in Computer Science Artificial Intelligence |
| url | https://arxiv.org/abs/2405.16792 |