Research map / Large language models / Agents, code and math
Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation
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.
Introduces LIG-MM, a 312-program benchmark of loop invariant generation for memory-manipulating programs, and LLM-SE, which fine-tunes CodeGen-350M with self-supervised predicate recovery and couples it with symbolic execution and an entailment solver.
Problem
Loop invariant generation has been limited to numerical programs; programs with linked data structures and memory manipulation (shape and memory safety verification) lack benchmarks and effective automated methods.
Approach
Self-supervised fine-tuning of an LLM on synthetic predicate-recovery tasks built by splitting inductive separation-logic predicate definitions (with augmentation and mix-up), then an interactive loop where the LLM proposes separating conjuncts that are checked by symbolic execution and an entailment solver.
Key results
- LLM-SE reaches 38.78% Pass Rate @ 1 on LIG-MM versus 12.82% for SLING, 12.50% for GPT-4, and 0.00% for AutoSpec.
- At Pass Rate @ 8, LLM-SE reaches 42.95% versus 21.79% for SLING and 17.68% for GPT-4.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use LLM-SE instead of SLING | Loop invariant generation on LIG-MM · LIG-MM (312 programs), Pass Rate @ 1 | pass rate: 12.82% -> 38.78% | Helped |
| Use LLM-SE instead of SLING | Loop invariant generation on LIG-MM · LIG-MM (312 programs), Pass Rate @ 8 | pass rate: 21.79% -> 42.95% | Helped |
Surprising findings
- AutoSpec, a state-of-the-art numerical loop invariant generator, achieves 0% pass rate on memory-manipulating programs.
- SLING performs poorly partly because many of its benchmark programs use function calls rather than loops.
Limitations
- Pass rate of about 39% still insufficient for real-world use, as the authors acknowledge.
- Baseline GPT-4 outputs sometimes in invalid format, requiring manual correction that may inflate baseline pass rates.
Experimental setup
Datasets: LIG-MM SV-COMP 2022 programs SLING benchmarks Linux Kernel programs GlibC programs LiteOS programs Zephyr programs course homework programs
Benchmarks: LIG-MM
Metrics: Pass Rate @ 1 Pass Rate @ 8
Baselines: SLING AutoSpec GPT-4
Builds on: CodeGen SLING LoopInvGen AutoSpec
Closest papers by meaning
- Lemur: Integrating Large Language Models in Automated Program Verification (ICLR 2024 · similarity 0.86)
- CLEVER: A Curated Benchmark for Formally Verified Code Generation (NeurIPS 2025 · similarity 0.86)
- AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement (ICML 2025 · similarity 0.85)
- T1: Tool-integrated Verification for Test-time Compute Scaling in Small Language Models (ICLR 2026 · similarity 0.85)
- Verified Code Transpilation with LLMs (NeurIPS 2024 · similarity 0.85)
- How efficient is LLM-generated code? A rigorous & high-standard benchmark (ICLR 2025 · similarity 0.84)
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.