Laurel: Generating Dafny Assertions Using Large Language Models

• URL: http://arxiv.org/abs/2405.16792v1
• Date: Mon, 27 May 2024 03:26:01 GMT
• Title: Laurel: Generating Dafny Assertions Using Large Language Models
• Authors: Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, Yuanyuan Zhou,
• Abstract summary: We propose Laurel, a tool that uses large language models (LLMs) to automatically generate helper assertions for Dafny programs. Laurel is able to generate over 50% of the required helper assertions given only a few attempts.
• Score: 2.6942525604796366
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Dafny is a popular verification language, which automates proofs by outsourcing them to an SMT solver. This automation is not perfect, however, and the solver often requires guidance in the form of helper assertions creating a burden for the proof engineer. In this paper, we propose Laurel, a tool that uses large language models (LLMs) to automatically generate helper assertions for Dafny programs. 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 lemma similarity metric. We evaluate our techniques on a dataset of helper assertions we extracted from three real-world Dafny codebases. Our evaluation shows that Laurel is able to generate over 50% of the required helper assertions given only a few attempts, making LLMs a usable and affordable tool to further automate practical program verification.

Related papers

• Self-play with Execution Feedback: Improving Instruction-following Capabilities of Large Language Models [54.14602121129874]
  We introduce AutoIF, the first scalable and reliable method for automatically generating instruction-following training data. AutoIF transforms the validation of instruction-following data quality into code verification.
  arXiv  Detail & Related papers  (2024-06-19T13:29:53Z)
• Are you still on track!? Catching LLM Task Drift with Activations [55.75645403965326]
  Task drift allows attackers to exfiltrate data or influence the LLM's output for other users. We show that a simple linear classifier can detect drift with near-perfect ROC AUC on an out-of-distribution test set. We observe that this approach generalizes surprisingly well to unseen task domains, such as prompt injections, jailbreaks, and malicious instructions.
  arXiv  Detail & Related papers  (2024-06-02T16:53:21Z)
• LLMAuditor: A Framework for Auditing Large Language Models Using Human-in-the-Loop [7.77005079649294]
  An effective method is to probe the Large Language Models using different versions of the same question. To operationalize this auditing method at scale, we need an approach to create those probes reliably and automatically. We propose the LLMAuditor framework, where one uses a different LLM along with human-in-the-loop (HIL) This approach offers verifiability and transparency, while avoiding circular reliance on the same LLM.
  arXiv  Detail & Related papers  (2024-02-14T17:49:31Z)
• Why and When LLM-Based Assistants Can Go Wrong: Investigating the Effectiveness of Prompt-Based Interactions for Software Help-Seeking [5.755004576310333]
  Large Language Model (LLM) assistants have emerged as potential alternatives to search methods for helping users navigate software. LLM assistants use vast training data from domain-specific texts, software manuals, and code repositories to mimic human-like interactions.
  arXiv  Detail & Related papers  (2024-02-12T19:49:58Z)
• Efficient Tool Use with Chain-of-Abstraction Reasoning [65.18096363216574]
  Large language models (LLMs) need to ground their reasoning to real-world knowledge. There remains challenges for fine-tuning LLM agents to invoke tools in multi-step reasoning problems. We propose a new method for LLMs to better leverage tools in multi-step reasoning.
  arXiv  Detail & Related papers  (2024-01-30T21:53:30Z)
• Leveraging Large Language Models to Boost Dafny's Developers Productivity [49.64902130083662]
  This paper proposes leveraging Large Language Models (LLMs) to enhance the productivity of Dafny developers. A new Dafny plugin generates suggestions for relevant lemmas that Dafny is unable to discover and use. For the lemmas that cannot be proved automatically, the plugin also attempts to provide accompanying calculational proofs.
  arXiv  Detail & Related papers  (2024-01-01T21:58:13Z)
• CLOMO: Counterfactual Logical Modification with Large Language Models [109.60793869938534]
  We introduce a novel task, Counterfactual Logical Modification (CLOMO), and a high-quality human-annotated benchmark. In this task, LLMs must adeptly alter a given argumentative text to uphold a predetermined logical relationship. We propose an innovative evaluation metric, the Self-Evaluation Score (SES), to directly evaluate the natural language output of LLMs.
  arXiv  Detail & Related papers  (2023-11-29T08:29:54Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  We propose a new satisfiability-aided language modeling (SatLM) approach for improving the reasoning capabilities of large language models (LLMs) We use an LLM to generate a declarative task specification rather than an imperative program and leverage an off-the-shelf automated theorem prover to derive the final answer. We evaluate SATLM on 8 different datasets and show that it consistently outperforms program-aided LMs in the imperative paradigm.
  arXiv  Detail & Related papers  (2023-05-16T17:55:51Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.