Research map / Large language models / Agents, code and math
Lemur: Integrating Large Language Models in Automated Program Verification
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes Lemur, a sound proof calculus that lets LLMs (GPT models) propose and repair program invariant sub-goals which automated verifiers (ESBMC, UAutomizer) check, and evaluates it on Code2Inv and hard SV-COMP benchmarks.
Problem
Automated program verification requires high-level abstract reasoning, such as decomposing a verification task into sub-goals/invariants, which conventional verifiers struggle to automate; prior LLM approaches lack formal soundness guarantees or require manual effort.
Approach
Formalize an interaction between LLM oracles (proposing and repairing sub-goal properties) and automated verifiers as a proof calculus with transition rules; LLM outputs are treated only as assumptions until verifiers prove implications, giving soundness, and an instantiated algorithm terminates.
Key results
- On the 133 Code2Inv benchmarks, the GPT-4 configuration solves 107 vs 92 for Code2Inv and 68 for ESBMC alone (10-minute timeout for ESBMC comparison).
- On 47 SV-COMP benchmarks that ESBMC and UAutomizer could not solve in 10 minutes, the GPT-4 configuration solves 25, versus 1 each for UAutomizer and ESBMC.
- The GPT-3.5 turbo configuration solves 103 Code2Inv and 14 SV-COMP benchmarks, showing oracle choice matters.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Add LLM-proposed proof goals and verifier-guided decomposition | ESBMC on the Code2Inv benchmarks · Code2Inv benchmarks | solved instances: 68 -> 107 | Helped |
| Add LLM-proposed proof goals and verifier-guided decomposition | Code2Inv · Code2Inv benchmarks | solved instances: 92 -> 107 | Helped |
| Add LLM-proposed proof goals and verifier-guided decomposition | ESBMC on the 47 SV-COMP benchmarks · 47 SV-COMP benchmarks | solved instances: 1 -> 25 | Helped |
| Add LLM-proposed proof goals and verifier-guided decomposition | Ultimate Automizer on the 47 SV-COMP benchmarks · 47 SV-COMP benchmarks | solved instances: 1 -> 25 | Helped |
| Use GPT-4 instead of GPT-3.5 turbo as the LLM oracle | Lemur · Code2Inv benchmarks | solved instances: 103 -> 107 | Helped |
| Use GPT-4 instead of GPT-3.5 turbo as the LLM oracle | Lemur · 47 SV-COMP benchmarks | solved instances: 14 -> 25 | Helped |
| Use GPT-4 instead of GPT-3.5 turbo as the LLM oracle | Lemur · 47 SV-COMP benchmarks | average time (s): 162.2 -> 234.5 | Hurt |
Surprising findings
- A GPT-4-driven configuration outperforms Code2Inv, which was specifically trained for invariant synthesis, on the Code2Inv benchmark set.
- GPT-4 consistently proposes invariants such as x%4==0 even when the modulo operator is absent from the program.
Limitations
- Performance depends on the verifier's capacity; modern verifiers handle only small programs.
- LLMs have token limits and struggle with complex nested logical formulas and programs with multiple loops.
- Does not yet offer a significant boost for complex properties of real-world C libraries; focuses on imperative languages.
Experimental setup
Datasets: Code2Inv benchmarks (133) SV-COMP 2023 reachability benchmarks (47 selected)
Benchmarks: Code2Inv SV-COMP hard reachability benchmarks
Metrics: number of solved instances average time average number of proposals
Baselines: Code2Inv ESBMC UAutomizer GPT-3.5 turbo variant of Lemur
Builds on: Code2Inv k-induction predicate abstraction chain-of-thought
Closest papers by meaning
- Evaluating Program Semantics Reasoning with Type Inference in System $F$ (NeurIPS 2025 · similarity 0.89)
- Verified Code Transpilation with LLMs (NeurIPS 2024 · similarity 0.88)
- FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving (NeurIPS 2024 · similarity 0.87)
- CoRe: Benchmarking LLMs’ Code Reasoning Capabilities through Static Analysis Tasks (NeurIPS 2025 · similarity 0.87)
- AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement (ICML 2025 · similarity 0.87)
- Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation (NeurIPS 2024 · similarity 0.86)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.