Towards Automated Verification of LLM-Synthesized C Programs
summary
SYNVER is a pipeline that uses GPT-4 to synthesize C programs and a Verified Software Toolchain backend with an Ltac layer called SEauto to discharge proofs. On a 50-program benchmark GPT-4 produces correct code for all but one case; automation verifies most proofs but generates side conditions requiring human steps. Biases (no loops, prefer recursion) matter: without them 24 of 26 recursive tasks become loops; separation-logic success rises from 12 to 20 when prompts include precise English specs.
AI-written summary · about
chapters (12)
- 0:00SynVer introduction
- 1:05Motivation for LLM guarantees
- 3:10Demo of SynVer verification
- 5:15SynVer workflow and architecture
- 7:42SE auto verification proofs
- 10:29Experimental results
- 12:38Biases in generated programs
- 13:19SE auto user assistance
- 14:23Comparison with PharmaC, Very Fast, RefineC
- 15:48Prompt component sensitivity
- 17:35Conclusion and future directions
- 18:58Q&A
related talks
38mAutomatically Synthesising Programs that We Can Trust
15mA benchmark for vericoding: formally verified program synthesis
41m"Do What I Mean": The History of AI and Program Synthesis
33mCorrectness Too Cheap To Meter: Formal Verification and LLMs
22mA Certifying Proof Assistant for Synthetic Mathematics in Lean
17mNeuro-Symbolic Proof Generation for Scaling Systems Software Verification
01h 08mLean: Machine-Checked Mathematics and Verified Programming, Past and Future
25mVerifying LLM powered Code Transformations with Equivalence Checking