DafnyBench: A Benchmark for Formal Software Verification
summary
DafnyBench is a scraped benchmark of 750 programs and ~53,000 LOC that tests whether LLMs (GPT‑4, Claude 3, etc.) can auto-generate the missing Dafny annotations; the best model and prompt hit ~68% success on standalone files. Iterative repair using verifier error messages improves results up to about four attempts then plateaus; larger programs and multi‑step proofs drop success sharply. Captured error categories (verification logic, code logic, altered specs, syntax) drive analysis, and tooling includes a Dafny Autopilot VS Code extension and verilib.org for dataset growth.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:29Creating DafnyBench from GitHub
- 3:35Benchmark task and criteria
- 4:19Initial LLM results
- 5:44Model reflection and improvement
- 7:32Performance versus complexity
- 8:56Error types and limitations
- 11:24Data contamination challenges
- 12:48Dafny autopilot extension
- 15:16VeriLib.org expanding benchmarks
- 16:41Q&A
related talks
16mDafnyPro: LLM-Assisted Automated Verification for Dafny Programs
18mSpecification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs
15mLaurel: Unblocking Automated Verification with Large Language Models
20mCLOVER: Closed-Loop Verifiable Code Generation
01h 01mDiscussion
18mToward Repository-Level Program Verification with Large Language Models
30mExploring the Verifiability of Code Generated by GitHub Copilot
53mSemantics-based program manipulation in the age of LLMs