CLOVER: Closed-Loop Verifiable Code Generation
summary
Generates code, docstrings, and formal annotations with GPT‑4 then applies six directed consistency checks (using reconstruction testing and the Dafny verifier) to accept only fully consistent triples; dataset is CloverBench (60 Dafny programs) with three incorrect variants per problem to test rejection. With up to K=10 independent generation attempts the pipeline reports 87% acceptance, 0% false positives on correct vs mutated examples and uses unit tests plus deductive verification to decide equivalence.
AI-written summary · about
chapters (11)
- 0:00CLOVER project intro
- 1:04Motivation for verifiable code gen
- 2:31Reducing verification complexity
- 4:43Two phases of CLOVER
- 6:12CLOVER Bench dataset
- 7:16Verifying code consistency
- 10:09GBD4 generates DEFY code
- 12:16Evaluating consistency checks
- 14:03CLOVER limitations
- 15:05Conclusion and future work
- 16:12Q&A
related talks
18mDafnyBench: A Benchmark for Formal Software Verification
15mDafny as Verification-Aware Intermediate Language for Code Generation
30mExploring the Verifiability of Code Generated by GitHub Copilot
16mDafnyPro: LLM-Assisted Automated Verification for Dafny Programs
23mdafny-annotator: AI-Assisted Verification of Dafny Programs
15mKeynote: Pre-training and Fine-tuning of Code Generation Models
36mCode Mending in the AI age
23mBeyond Tests What to Verify in AI Generated Code