Laurel: Unblocking Automated Verification with Large Language Models
summary
Laurel is a tool that generates missing Dafny assertions with LLMs by (1) inserting an assertion placeholder at the SMT error location and (2) supplying exemplar assertions selected by a proof similarity metric from the same codebase. Implemented atop Dafny and evaluated on a new benchmark of lemmas from three real-world Dafny projects (Dafny standard library, Cedar, VMC), it reaches a 56.6% success rate overall, doubles success versus naive prompts, and hits ~25% on first try using GPT-4/4o.
AI-written summary · about
chapters (8)
- 0:00Automated verification intro
- 1:24Assertion challenges in Daphne
- 3:36LLMs for assertion generation
- 6:46Assertion placement with placeholders
- 8:12Similar assertions as examples
- 10:59Limitations and future work
- 12:01AI impact on verification
- 12:45Q&A
related talks
18mLaurel: Unblocking Automated Verification with Large Language Models
16mDafnyPro: LLM-Assisted Automated Verification for Dafny Programs
23mdafny-annotator: AI-Assisted Verification of Dafny Programs
15mDafny as Verification-Aware Intermediate Language for Code Generation
18mDafnyBench: A Benchmark for Formal Software Verification
18mSpecification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs
16mLemur: Integrating Large Language Models in Automated Program Verification
22mTowards Verified Code Reasoning by LLMs