Lemur: Integrating Large Language Models in Automated Program Verification
summary
A framework named Lemur integrates GPT-4 via OpenAI API with model-checkers UAutomizer and ESBMC, using LLM calls to propose, strengthen and repair loop invariants and a verifier to check implications. A formal calculus is sound and a heuristic algorithm guarantees termination of the strategy. On 50 short C benchmarks that neither solver could solve alone, Lemur proves properties for 25% solved by generating candidates (about 20 LLM calls per case) but struggles with arrays, nested loops, and locating invariants.
AI-written summary · about
chapters (9)
- 0:00Lemur project introduction
- 1:29LLMs in verification motivation
- 3:37LLMs verification challenges
- 5:49Lemur separation of responsibilities
- 7:18Algorithm workflow with LLM
- 10:28Experimental results setup
- 11:58Performance improvements
- 12:41Limitations and future work
- 13:25Q&A
related talks
19mAutomated Program Refinement: Guide and Verify Code Large Language Model with(…)
01h 02mHow can Machine Learning Help Formal Proving ?
53mSemantics-based program manipulation in the age of LLMs
26mLanguage Model Agents Enable Semi-Formal Programming
22mTowards Verified Code Reasoning by LLMs
15mLaurel: Unblocking Automated Verification with Large Language Models
18mLaurel: Unblocking Automated Verification with Large Language Models
15mInterleaving Large Language Models for Compiler Testing