REVIEW 8 cited by
Lemur: Integrating Large Language Models in Automated Program Verification
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
The demonstrated code-understanding capability of LLMs raises the question of whether they can be used for automated program verification, a task that demands high-level abstract reasoning about program properties that is challenging for verification tools. We propose a general methodology to combine the power of LLMs and automated reasoners for automated program verification. We formally describe this methodology as a set of transition rules and prove its soundness. We instantiate the calculus as a sound automated verification procedure and demonstrate practical improvements on a set of synthetic and competition benchmarks.
Forward citations
Cited by 8 Pith papers
-
Satisfiability Solving with LLMs: A Matched-Pair Evaluation of Reasoning Capability
A matched-pair protocol and Accurate Differentiation Rate metric reveal that conventional LLM accuracy on SAT problems is often inflated by over-predicting satisfiability, while cross-representation agreement exceeds ...
-
Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair
Event-B Agent is an LLM agent that synthesizes, refines, and repairs Event-B formal models from natural language requirements via iterative verification feedback loops.
-
An AI Approach to Verified Production Cryptographic Libraries
An AI agent, guarded by mechanical integrity gates, synthesized Verus-verified internal specifications and proofs for curve25519-dalek and chacha20 without changing executable code.
-
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.
-
Guiding Human Validation of LLM-Generated Code via Verifiable Literate Programming
VLP adds an NL documentation layer with trace-linked mismatch detection and derived formal checks to make human validation of LLM code feasible, lifting pass@1 from 28.7-73.2% to 65.4-93.5%.
-
Using LLMs to Adjudicate Static-Analysis Alerts with Error Reduction Techniques
Mid-tier reasoning LLMs with consistency checks and LLM reasoning evaluation adjudicate static-analysis alerts at ≥98% recall and ≥94.8% specificity across Juliet, FormAI, and SV-COMP.
-
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.