dafny-annotator: AI-Assisted Verification of Dafny Programs

• URL: http://arxiv.org/abs/2411.15143v1
• Date: Tue, 05 Nov 2024 19:27:56 GMT
• Title: dafny-annotator: AI-Assisted Verification of Dafny Programs
• Authors: Gabriel Poesia, Chloe Loughridge, Nada Amin,
• Abstract summary: We explore using a combination of Large Language Models and search to build dafny-annotator. On a test set from the DafnyBench collection of programs, greedy search guided by LLaMa 3.1 8B successfully annotates only 15.7% of the methods. Our results suggest a path towards capable AI assistants for languages that don't yet have large-scale human-generated examples.
• Score: 4.651620941143133
• License:
• Abstract: Formal verification has the potential to drastically reduce software bugs, but its high additional cost has hindered large-scale adoption. While Dafny presents a promise to significantly reduce the effort to write verified programs, users are often required to provide logical annotations to aid the verifier. Here, we explore using a combination of Large Language Models and search to build dafny-annotator: a tool that adds logical annotations to a Dafny method until the verifier can prove it correct. On a test set from the DafnyBench collection of programs, greedy search guided by LLaMa 3.1 8B successfully annotates only 15.7% of the methods. Since this data-driven approach is hindered by the lack of large-scale training data, we propose a method for open-ended synthesis of new Dafny programs in a flexible pipeline where LLMs formulate high-level ideas, implement them, and incrementally propose changes to existing programs, which Dafny validates. This gives us a synthetic dataset, DafnySynth, which we use to augment DafnyBench for training. Fine-tuning on both datasets boosts LLaMa 8B's success rate to 50.6% -- significantly better than the base model, or training on either dataset alone. Our results suggest a path towards capable AI assistants for languages that don't yet have large-scale human-generated examples. In turn, such assistants might reduce friction for users and ultimately drive adoption.

Related papers

• SIaM: Self-Improving Code-Assisted Mathematical Reasoning of Large Language Models [54.78329741186446]
  We propose a novel paradigm that uses a code-based critic model to guide steps including question-code data construction, quality control, and complementary evaluation. Experiments across both in-domain and out-of-domain benchmarks in English and Chinese demonstrate the effectiveness of the proposed paradigm.
  arXiv  Detail & Related papers  (2024-08-28T06:33:03Z)
• Laurel: Generating Dafny Assertions Using Large Language Models [2.6942525604796366]
  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.
  arXiv  Detail & Related papers  (2024-05-27T03:26:01Z)
• Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming [8.34623776815378]
  We curate a dataset of 600K lines of open-source F* programs and proofs. This dataset includes software used in production systems ranging from Windows and Linux to Python and Firefox. We investigate the use of AI to synthesize programs and their proofs in F*, with promising results.
  arXiv  Detail & Related papers  (2024-05-03T00:14:33Z)
• LESS: Selecting Influential Data for Targeted Instruction Tuning [64.78894228923619]
  We propose LESS, an efficient algorithm to estimate data influences and perform Low-rank gradiEnt Similarity Search for instruction data selection. We show that training on a LESS-selected 5% of the data can often outperform training on the full dataset across diverse downstream tasks. Our method goes beyond surface form cues to identify data that the necessary reasoning skills for the intended downstream application.
  arXiv  Detail & Related papers  (2024-02-06T19:18:04Z)
• 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)
• Uncertainty-aware Parameter-Efficient Self-training for Semi-supervised Language Understanding [38.11411155621616]
  We study self-training as one of the predominant semi-supervised learning approaches. We present UPET, a novel Uncertainty-aware self-Training framework. We show that UPET achieves a substantial improvement in terms of performance and efficiency.
  arXiv  Detail & Related papers  (2023-10-19T02:18:29Z)
• PaD: Program-aided Distillation Can Teach Small Models Reasoning Better than Chain-of-thought Fine-tuning [20.59775450213501]
  We propose Program-aided Distillation (PaD), which introduces reasoning programs to suppress the errors in distilled data. We evaluate PaD on arithmetic reasoning, symbolic reasoning, and general ability.
  arXiv  Detail & Related papers  (2023-05-23T10:11:56Z)
• Training Data is More Valuable than You Think: A Simple and Effective Method by Retrieving from Training Data [82.92758444543689]
  Retrieval-based methods have been shown to be effective in NLP tasks via introducing external knowledge. Surprisingly, we found that REtrieving from the traINing datA (REINA) only can lead to significant gains on multiple NLG and NLU tasks. Experimental results show that this simple method can achieve significantly better performance on a variety of NLU and NLG tasks.
  arXiv  Detail & Related papers  (2022-03-16T17:37:27Z)
• Efficient Nearest Neighbor Language Models [114.40866461741795]
  Non-parametric neural language models (NLMs) learn predictive distributions of text utilizing an external datastore. We show how to achieve up to a 6x speed-up in inference speed while retaining comparable performance.
  arXiv  Detail & Related papers  (2021-09-09T12:32:28Z)
• Learning to Count in the Crowd from Limited Labeled Data [109.2954525909007]
  We focus on reducing the annotation efforts by learning to count in the crowd from limited number of labeled samples. Specifically, we propose a Gaussian Process-based iterative learning mechanism that involves estimation of pseudo-ground truth for the unlabeled data.
  arXiv  Detail & Related papers  (2020-07-07T04:17:01Z)

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.