REVIEW 7 cited by
Finding Inductive Loop Invariants using Large Language Models
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
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.
Forward citations
Cited by 7 Pith papers
-
InvWeaver: Deductive Feedback for Invariant Synthesis in Interacting-Loop Programs
InvWeaver synthesizes multi-loop invariants by exposing inter-loop dependencies on a loop-level call graph and refining candidates with weakest-precondition-guided LLM feedback, solving 72/82 multi-loop benchmarks.
-
VeriSkill: A Self-Evolution Framework for Program Verification Skills
VeriSkill turns failed program-verification attempts into validated, reusable skill updates, reporting PASS-rate gains of 17.6 to 51.3 percentage points over no-skill agents across Dafny, Frama-C, and VeriFast.
-
LimICE: Integrating LLM into ICE Framework for Efficient Loop Invariant Inference
LimICE combines LLM-generated facts, incremental lemma synthesis, and a decision-tree fallback to solve 349/367 linear and 47/50 nonlinear loop-invariant benchmarks, beating state-of-the-art tools.
-
Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability
Diverse recursive and imperative array/list implementations of the same task, paired with frozen representation-specific contracts and bounded Why3 repair, raise task-level verification to 67.1% versus lower rates for...
-
Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?
LLMs, verified by a symbolic model checker, produced correct inductive strengthenings for 82 of 94 curated RTL safety properties.
-
Autoformalization in the Era of Large Language Models: A Survey
A literature review of LLM-based autoformalization, covering datasets, workflows, benchmarks, and its potential role in verifying AI outputs.
-
The 4/$\delta$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee
The 4/δ bound is the mean of four geometric distributions, not a new theorem, and the simulation validation is circular.
Discussion (0). Continue with ORCID to comment.