Source-linked AI summary
Finding Inductive Loop Invariants using Large Language Models
Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K. Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, Rahul Sharma
TL;DR
Finding inductive loop invariants is an undecidable problem central to formal verification, and the paper asks whether LLMs can help. It builds a benchmark dataset and combines LLM-generated candidates with symbolic pruning; this combination outperforms state-of-the-art symbolic verifiers on multiple benchmarks.
Problem
Finding inductive loop invariants is undecidable in general, yet they are needed to establish formal properties of programs with loops.
Source: §1 · p. 1Method
The paper evaluates LLM-generated loop invariants on a curated dataset and combines LLMs with Houdini formal pruning.
Source: §1 · p. 2, §2 · p. 3, §3.2 · p. 4Results
The LLM and formal-pruning combination outperforms state-of-the-art symbolic verifiers on multiple benchmarks.
Source: §6 · p. 13Takeaways & Limitations
The results support further research into combining formal verification and LLMs.
Source: §6 · p. 13Houdini may miss a valid candidate subset when the oracle does not identify candidates that fail entry or preservation checks.
Source: §3.2 · p. 5
Abstract
from arXiv · showhide
Loop invariants are fundamental to reasoning about programs with loops. They establish properties about a given loop's behavior. When they additionally are inductive, they become useful for the task of formal verification that seeks to establish strong mathematical guarantees about program's runtime behavior. The inductiveness ensures that the invariants can be checked locally without consulting the entire program, thus are indispensable artifacts in a formal proof of correctness. Finding inductive loop invariants is an undecidable problem, and despite a long history of research towards practical solutions, it remains far from a solved problem. This paper investigates the capabilities of the Large Language Models (LLMs) in offering a new solution towards this old, yet important problem. To that end, we first curate a dataset of verification problems on programs with loops. Next, we design a prompt for exploiting LLMs, obtaining inductive loop invariants, that are checked for correctness using sound symbolic tools. Finally, we explore the effectiveness of using an efficient combination of a symbolic tool and an LLM on our dataset and compare it against a purely symbolic baseline. Our results demonstrate that LLMs can help improve the state-of-the-art in automated program verification.
1 INTRODUCTION
The paper studies whether LLMs can help with the long-standing, undecidable problem of finding inductive loop invariants. It contributes a C-program benchmark dataset and evaluation toolchain, and investigates combining LLM-generated candidates with symbolic verification.
1 INTRODUCTION
- The paper evaluates whether LLMs can generate loop invariants using a curated C-program dataset and a toolchain that measures success.LLM candidates can be checked by symbolic verifiers, which reject incorrect candidates and validate a passing Hoare triple.Source: §1 · pp. 1–2
- Inductive loop invariants support formal verification by establishing loop properties that are preserved across iterations and sufficient to prove a postcondition.They must follow from the precondition, be preserved by the loop body, and imply the postcondition on exit.Source: §1 · pp. 1–2
- Finding loop invariants is undecidable in general, despite decades of symbolic and machine-learning-based approaches.Prior techniques include abstraction refinement, interpolation, abstract interpretation, synthesis, and learned models.Source: §1 · p. 2
- The contributions include evaluating GPT-4, GPT-3.5, and Code Llama against a symbolic baseline, plus combining LLMs with symbolic techniques to tolerate output inaccuracies.The combination asks the model for invariant ingredients rather than a complete invariant and uses a linear number of solver calls in the number of LLM generations.Source: §1 · p. 2
2 DATASET
The dataset combines C verification benchmarks from prior invariant-inference work and SV-COMP, then filters and selects a one-loop, one-method subset for evaluation.
2 DATASET
- The combined dataset contains 1,166 C benchmarks, with verification properties encoded as program assertions.Sources include LoopInvGen, Code2Inv, Accelerating Invariant Generation, LinearArbitrary-SeaHorn, and SV-COMP.Source: §2 · p. 3
- Filtering out arrays, pointers, ambiguous semantics, and programs longer than 500 lines leaves 1,005 benchmarks.The restrictions focus the dataset on integer programs and account for current LLM prompt-size limitations.Source: §2 · p. 3
- The evaluation focuses on 555 benchmarks with exactly one loop and one method: 469 positive instances and 86 negative instances.Ground truth was established using original sources, Ultimate Automizer, and manual inspection; dataset modifications preserve program semantics for the verified property.Source: §2 · p. 3
3 TECHNICAL DETAILS
Loopy combines LLM-generated invariant candidates with an oracle that checks inductiveness and verification sufficiency. It first tests sampled candidates, then applies Houdini and, if needed, an LLM-guided repair procedure.
3 TECHNICAL DETAILS
- The toolchain prompts an LLM with a shared template and target program to produce candidate invariants, then passes annotated programs to an oracle for checking.The oracle reports success, syntax errors, and candidates it identifies as unsupported.Source: §3 · pp. 3–4
3.1 Loopy
- Loopy samples up to a user-provided bound, checks each completion, unions candidates from unsuccessful completions, and applies Houdini before attempting repair.Houdini can search for a sufficient inductive subset with a linear number of oracle calls in the candidate-set size.Source: §3.1 · p. 4, §3.2 · p. 5
3.2 Houdini
- Houdini repeatedly checks candidates and prunes syntax-invalid or oracle-blamed expressions, returning a sufficient set or failure.Its optimality requires the oracle to identify candidates that fail entry or preservation checks; without that information, it can miss a valid subset.Source: §3.2 · pp. 4–5
3.3 Repair
- Repair uses oracle error information to prompt the LLM for a revised invariant set, then checks it and applies Houdini to find an inductive subset.It repeats this process up to the repair bound and returns failure if no suitable set is found.Source: §3.3 · pp. 5–6
4 EVALUATION
The evaluation tests Loopy with Frama-C across six research questions, including comparisons among prompts and models, repair, failure patterns, and Ultimate. Loopy verifies fewer benchmarks overall than Ultimate, but also solves some that Ultimate misses.
4 EVALUATION
- The experiments use Frama-C’s WP plugin with GPT-4, GPT-3.5-Turbo, and CodeLlama-34b-Instruct; Ultimate Automizer provides the symbolic baseline.The evaluation frames six questions about generation, invariant ingredients, models, repair, failure features, and symbolic comparison.Source: §4 · p. 6
4.1 [RQ1] Using LLMs to generate loop invariants
- With M2, Loopy verifies 293 benchmarks versus M1’s 237, a 23% increase; multiple completions help, with diminishing returns after about eight.Figure 1 plots success rate against completion count; dashed lines omit Houdini and Repair.Source: §4.1 · pp. 7–8, Figure 1 · p. 8
4.2 [RQ2] LLMs generating ingredients of invariant
- With 15 completions and M2, Houdini raises solved benchmarks by 30.7%, from 293 to 383; LLMs find invariant ingredients more readily than complete sets.Figure 1’s solid lines show Loopy with Houdini and without Repair.Source: §4.2 · pp. 8–9, Figure 1 · p. 8
4.3 [RQ3] Comparing different LLMs
- GPT-4 performs best among the tested models, while GPT-3.5-Turbo is a close second with 370 solved benchmarks using Houdini; their solved sets include unique cases.Figure 2 compares models with 15 completions and M2; Figure 3 shows their benchmark intersection.Source: Figure 2 · p. 8, §4.3 · p. 9, Figure 3 · p. 9
4.4 [RQ4] Using LLMs to fix incorrect invariants
- With generation and repair budgets totaling 15, Loopy uses eight completions and seven repair iterations; repair verifies 15 additional benchmarks, for 398 total.The generation budget is set near the point where performance without repair begins to plateau.Source: §4.4 · p. 9
4.5 [RQ5] Qualitative analysis of the failure cases
- The failure analysis identifies disjunctions, clauses with at least three variables, insufficiently precise constraints, and floating-point reasoning as challenging features.The authors describe these categories as somewhat predictive, not as features LLMs cannot solve; the classification uses manually selected simple ground-truth invariants.Source: §4.5 · p. 10
- Some failures arise when Frama-C rejects correct invariants, likely because of imprecise solver reasoning; the authors consider these cases within modern SMT solvers’ reach.Integer-modulo reasoning is one example cited.Source: §4.5 · p. 10
4.6 [RQ6] Symbolic baseline
- Ultimate verifies 430 of 469 benchmarks versus Loopy’s 398, while Loopy solves 31 benchmarks that Ultimate misses.Figure 4 compares the benchmarks verified by the two tools.Source: §4.6 · p. 11, Figure 4 · p. 12
5 RELATED WORK
Earlier work explored fine-tuned LLMs for invariant generation and custom models for ranking LLM-generated candidates. This paper evaluates foundational models directly and describes invariant ranking as complementary.
5 RELATED WORK
- Pei et al. fine-tune a pre-trained LLM on programs paired with invariants, whereas this work evaluates foundational models without pre-training and focuses on inductive invariants.The related work says Pei et al. do not focus on generating inductive invariants needed for formal proof of correctness.Source: §5 · p. 12
- iRank uses a custom model to rank LLM-generated invariant candidates and could reduce oracle calls by checking highly ranked candidates first.The paper describes iRank as orthogonal and complementary to its approach.Source: §5 · p. 12
- Unlike iRank’s lower-level SMT encodings, this work queries LLMs with C programs and does not use iRank’s candidate-generation approach with Houdini or invariant repair.The authors argue that LLMs should understand C syntax better.Source: §5 · p. 12
6 CONCLUSION
The paper evaluates pre-trained LLMs for generating inductive loop invariants and contributes a dataset and evaluation toolchain. It reports that combining LLMs with Houdini outperforms state-of-the-art symbolic verifiers on multiple benchmarks.
6 CONCLUSION
- The paper evaluates pre-trained LLMs on generating inductive invariants for program loops.The evaluation is presented as a way to investigate LLMs’ potential for formal verification.Source: §6 · pp. 12–13
- A simple, efficient combination of LLMs and Houdini outperforms state-of-the-art symbolic verifiers on multiple benchmarks.The authors say these results should inspire further research combining formal verification and LLMs.Source: §6 · p. 13
- The paper presents a dataset and a toolchain for evaluating LLMs on loop-invariant generation.Source: §6 · p. 13
A.1 Prompts and parameters
The appendix specifies prompts for generating and repairing loop invariants, along with shared generation settings. The prompts request verifier-usable invariants and provide rules for handling failed verification and program assumptions.
A.1 Prompts and parameters
- All LLM queries use a sampling temperature of 0.7 and a maximum of 2,000 tokens per generation.Source: §A.1 · p. 14
- The generation prompt asks for invariants sufficient to prove the postcondition, with instructions to split conjunctions and return the invariants in one code block.The prompt also advises using implications for conditional code and adding variable bounds or relations when they exist.Source: §A.1 · pp. 15–16
- The repair prompt asks the model to fix syntax errors and non-inductive invariants using Frama-C feedback, including whether invariants are established or preserved.It also directs the model to replace or strengthen invariants when needed and output corrected invariants in one code block.Source: §A.1 · p. 16
- The prompts caution against undeclared or uninitialized variables, unsupported ACSL keywords, assumptions about undefined functions, and non-deterministic calls.The repair prompt specifies using \at(x, LoopEntry) rather than \at(x, Pre); the generation prompt prohibits \at(x, Pre).Source: §A.1 · pp. 15, 17
- For repair, the model receives a C program and Frama-C’s message, then returns corrected ACSL loop invariants in a single code block.The prompt explains verifier feedback such as an unbound logic variable and distinguishes established, preserved, and partially inductive invariants.Source: §A.1 · pp. 16–18
A.2 Modifications
The dataset preparation standardizes benchmark comments, nondeterministic functions, and assertions for the Frama-C verification workflow. It also adjusts error markers, main functions, and preprocessor lines for compatibility.
A.2 Modifications
- Comments describing loops or required invariants were removed to make benchmarks uniform.Source: §A.2 · p. 18
- Different benchmark conventions for nondeterministic functions and assumptions were standardized using common functions and an assume macro.Source: §A.2 · p. 18
- Assertions and unreachable-error markers were converted to ACSL annotations, including replacing error labels or reach_error calls with assertions of false.Source: §A.2 · p. 18
- A default return statement was added when needed to match the main function’s return type, and preprocessor-generated lines were discarded.The paper states that the return adjustment does not affect the verification task.Source: §A.2 · p. 18