Dafny as Verification-Aware Intermediate Language for Code Generation
summary
Prototype guides an LLM to emit Dafny as opaque IR which is verified and then compiled to Python, preserving a proof and added unit tests. The system converges on a candidate for 144 of 164 HumanEval tasks and achieves an 88% pass rate comparable to direct generation, while reducing subtle correctness bugs the LLM originally produced. Implementation uses prompt engineering, Dafny verifier feedback loops, and the Dafny compiler to produce compiled Python with extra tests.
AI-written summary · about
chapters (12)
- 0:00Verified code generation intro
- 0:26LLM code gen challenges
- 1:52Dafny in synthesis research
- 2:34Prototype workflow
- 4:42Live demo
- 6:51Direct vs Dafny solutions
- 7:55HumanEval results
- 9:20Implementation details
- 11:33Dafny verifier feedback
- 12:35Compiler output generation
- 13:18Future work limits
- 15:06Q&A
related talks
16mDafnyPro: LLM-Assisted Automated Verification for Dafny Programs
15mLaurel: Unblocking Automated Verification with Large Language Models
18mSpecification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs
01h 01mDiscussion
20mCLOVER: Closed-Loop Verifiable Code Generation
22mTowards Verified Code Reasoning by LLMs
53mSemantics-based program manipulation in the age of LLMs
32mCan We Trust AI-Generated Code?