A benchmark for vericoding: formally verified program synthesis
summary
A public benchmark assembles roughly 10,000 tasks across Lean, Rust/Verus and Dafny (Lean ~4,000, Dafny ~800 after splitting/cleaning) and runs LLM prompting that returns code plus machine-checkable proofs with a validate/verify loop. Experiments show best results with Dafny, weaker performance on Verus and surprisingly poor results on Lean; ensembling multiple models improves coverage. Practical problems include duplicated trivial specs, cross-language translation glitches, cheating solutions that map to mathematical integers, and an estimated cost of about $20,000.
AI-written summary · about
chapters (9)
- 0:00Vericoding and formal verification
- 1:47Vericoding framework
- 3:36Benchmark for vericoding
- 5:23Benchmark tasks sources
- 6:50Lean and Rust results
- 9:18Specification difficulty case study
- 12:28Benchmark results analysis
- 13:51Future work and conclusion
- 14:12Q&A: Cost and accessibility
related talks
22mTowards Automated Verification of LLM-Synthesized C Programs
01h 08mLean: Machine-Checked Mathematics and Verified Programming, Past and Future
38mAutomatically Synthesising Programs that We Can Trust
33mCorrectness Too Cheap To Meter: Formal Verification and LLMs
33mPractical Evaluation of LLMs for Code
01h 16mCoding Agents: New opportunities for formal methods?
31mMaking the most of test-time compute in LLMs
41m"Do What I Mean": The History of AI and Program Synthesis