Toward Automated, Contamination-free Dafny Benchmark Generation
summary
TACoDafny automates converting task descriptions (first 200 LeetCode problems) into Dafny programs plus contracts by prompting LMs to produce implementations, generating positive and negative test cases against Python ground truth, and iterating until tests pass. The pipeline yields 76 Dafny programs with contracts, of which 51 have model-count = 1 strong specifications, uses model counting to assess spec strength, and measures verification success with K = 20 interactions where the best model verifies about 40% solved within 20 iterations.
AI-written summary · about
chapters (12)
- 0:00Automated Dafny benchmark intro
- 1:48Dafny verification and codegen
- 3:11Benchmark generation pipeline
- 6:03Generating test cases
- 8:10Evaluating spec strength
- 9:33Contamination-free design
- 10:58Benchmark evaluation with VeriK
- 12:45Difficulty and challenges
- 13:07Conclusion and open questions
- 14:55Q&A: Implementation
- 15:59Q&A: Availability
- 17:06Q&A: Post-cutoff eval
related talks
26mDSPy: Compiling Declarative Language Model Calls into Self-Improving Pipelines
39mTraining AI To Code Using The Largest Code Dataset (Project CodeNet)- 39mTraining AI To Code Using The Largest Code Dataset (Project CodeNet)
24mThe Limits of Prompting: ArchitectingTrustworthy Coding Agents
22mTowards Automated Verification of LLM-Synthesized C Programs
39mMaking AI Reliable in the SDLC: The Role of Deterministic Context at Scale
36mCould a Machine ever write tests for our code
13mDeploying Enterprise-Grade Compliant Generative AI