REVIEW 9 cited by
Laurel: Unblocking Automated Verification with 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
Signed reviews
read the original abstract
Program verifiers such as Dafny automate proofs by outsourcing them to an SMT solver. This automation is not perfect, however, and the solver often requires hints in the form of assertions, creating a burden for the proof engineer. In this paper, we propose Laurel, a tool that alleviates this burden by automatically generating assertions using large language models (LLMs). To improve the success rate of LLMs in this task, we design two domain-specific prompting techniques. First, we help the LLM determine the location of the missing assertion by analyzing the verifier's error message and inserting an assertion placeholder at that location. Second, we provide the LLM with example assertions from the same codebase, which we select based on a new proof similarity metric. We evaluate our techniques on our new benchmark DafnyGym, a dataset of complex lemmas we extracted from three real-world Dafny codebases. Our evaluation shows that Laurel is able to generate over 56.6\% of the required assertions given only a few attempts, making LLMs an affordable tool for unblocking program verifiers without human intervention.
Forward citations
Cited by 9 Pith papers
-
From Scientific Texts to Verifiable Code: Automating the Process with Transformers
A prototype that uses an LLM iteratively with Dafny verification can turn natural-language graph proofs into verifiable code for three simple lemmas, suggesting a two-stage path toward automated verification.
-
Formal Mathematical Reasoning: A New Frontier in AI
Machine-checkable formal proof should become the backbone of AI mathematics, and a five-task, five-level capability roadmap can measure progress toward that goal.
-
Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects
LLM-based formalisation of software requirements is promising but faces five persistent challenges; the proposed VERIFAI framework plans to address them with human-in-the-loop and tool-neutral pipelines.
-
Seeking Specifications: The Case for Neuro-Symbolic Specification Synthesis
Deepseek-R1 can usually distinguish intended behavior from buggy implementations when writing ACSL specs, and augmenting prompts with Frama-C tool outputs measurably changes the type and focus of generated annotations.
-
Image Segmentation with Large Language Models: A Survey with Perspectives for Intelligent Transportation Systems
A survey that organizes vision-language segmentation methods for intelligent transportation, but its synthesis is undermined by fabricated references and unverifiable benchmarks.
-
Working Document -- Formalising Software Requirements with Large Language Models
The paper surveys 94 papers on LLM-assisted formalisation of software requirements, organised around formalisation, traceability, formal methods, and UTP/institutions.
-
A Short Survey on Formalising Software Requirements using Large Language Models
A survey summarizing 35 papers on using LLMs to formalize software requirements, but it contains no new experimental results and its classification tables have errors.
-
Formalising Software Requirements using Large Language Models
A short project-position paper describing VERIFAI, a planned system for automatic formalisation and traceability of natural language requirements, with no experimental results yet.
- Dafny as Verification-Aware Intermediate Language for Code Generation
Discussion (0). Continue with ORCID to comment.