REVIEW 15 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 15 Pith papers
-
Verification Modulo Tested Library Contracts
A new framework synthesizes library method contracts that are adequate for client verification and pass testing scrutiny, using CHC solvers and ICE learning.
-
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...
-
Guiding LLM-based Loop Invariant Synthesis via Feedback on Local Reasoning Errors
LORIS detects local reasoning errors in LLM-generated proofs for loop invariants by translating natural-language steps to first-order logic implications and using invalid implications to refine the invariants, achievi...
-
Combining Mechanical and Agentic Specification Inference for Move
Early prototype merges weakest-precondition analysis with an AI agent to infer Move specifications, using the prover as oracle to validate and refine them for code with loops, references, and higher-order functions.
-
Verification Modulo Tested Library Contracts
Synthesizes adequate modular and contextual contracts for library methods via counterexample-guided learning with CHC solvers and testing to verify clients without full library verification.
-
Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?
A neurosymbolic method using two LLM prompting frameworks generates provably correct inductive arguments for 84% of a set of mid-size open-source RTL hardware designs.
-
ClassInvGen: Class Invariant Synthesis using Large Language Models
ClassInvGen co-generates class invariants and tests with LLMs to outperform pure LLM generation and Daikon on C++ data structures.
-
Automating Formal Verification with Reinforcement Learning and Recursive Inference
RLVR training raises verified Dafny pass rates from 9.7% to 31.1% on a filtered benchmark while a Lean proof scaffold lifts success from 46.2% to 69.2% on a pilot set and solves 7 of 42 prior unsolved tasks.
-
Combining Mechanical and Agentic Specification Inference for Move
A hybrid tool pairs mechanical weakest-precondition analysis with an AI agent to infer verifiable specifications for Move programs, using the prover as an oracle to refine results until they pass.
-
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.
-
Evaluating LLM-Generated ACSL Annotations for Formal Verification
Rule-based annotation generation for ACSL outperforms LLM-based methods in achieving successful formal verification of C programs.
-
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). Sign in to comment.