Laurel: Unblocking Automated Verification with Large Language Models
summary
Laurel uses large language models to auto-generate missing Dafny assertions and reports a >56.6% success rate on a new DafnyGym benchmark of lemmas extracted from three real-world codebases (Dafny standard library, CEDAR, DNE VMC). Two domain-specific prompts drive results: an assertion placeholder located from the SMT error message and retrieved examples via a proof similarity metric (hierarchical text/token/line distance). Baselines (naive prompting or error-only) stay under ~15%; the placeholder doubles success and similarity adds ~30 percentage points.
AI-written summary · about
chapters (9)
- 0:00Laurel introduction
- 0:26Partial automation problems in Daphne
- 3:14LLMs for assertion generation
- 5:23Laurel’s assertion generation
- 7:09Assertion location selection
- 8:30Proof similarity measurement
- 10:41Laurel on DVG dataset
- 13:32Results and future work
- 14:14User study on Daphne
related talks
15mLaurel: Unblocking Automated Verification with Large Language Models
16mDafnyPro: LLM-Assisted Automated Verification for Dafny Programs
18mSpecification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs
16mLemur: Integrating Large Language Models in Automated Program Verification
18mToward Repository-Level Program Verification with Large Language Models
01h 01mDiscussion
22mTowards Verified Code Reasoning by LLMs
29mLies, damned lies and large language models