DafnyBench: A Benchmark for Formal Software Verification

Authors: chloe  loughridge
qinyi  sun
seth  ahrenbach
federico  cassano
chuyue  sun
ying  sheng
anish  mudide
md  rakib
hossain  misu
nada  amin
max  tegmark
Venue: NeurIPS_cc_2024_Workshop_MATH-AI
Published: 2024-08-29 00:46:08

Abstract: We introduce DafnyBench, the largest benchmark of its kind for training and evaluating machine learning systems for formal software verification. We test the ability of LLMs such as GPT-4 and Claude 3 to auto-generate enough annotations for the Dafny formal verification engine to successfully verify over 750 programs with about 53,000 lines of code. The best model and prompting scheme achieved 68% success rate, and we quantify how this rate improves when retrying with error message feedback and how it deteriorates with the amount of required code and annotations. We hope that DafnyBench will enable rapid improvements from this baseline as LLMs and verification techniques grow in quality.

Main paper: 
 introduction: 
 Rapidly improving Large Language Models (LLMs) [1] [2] [3] are helping accelerate software development through program synthesis tools. But how can we ensure that LLM-generated code meets our specifications and reliably does precisely what it is supposed to do? Indeed, this remains a persistent problem even with human-written code: major code-testing efforts failed to prevent e.g. bugs causing an Ariane-V rocket explosion [4] and security vulnerabilities in ssh [5] and the Bash shell [6] .Although formal verification can guarantee reliability, providing rigorous mathematical proof that software meets specification, it has yet to gain widespread adoption. Formally verifying code is often a significant burden on the developer [7, 8] . Also, existing formal verification tools involve a major learning curve above and beyond just coding, greatly reducing the pool of people able to do this work.Machine learning methods have the potential to minimize a common pain point of formal methods, i.e., writing formal specifications. To support automation of formal verification, this paper's goal is to build a benchmark by assembling a suite of formally verified programs written in Dafny, a formal verification language developed for easy adoption by programmers due to its similarity with popular imperative programming languages such as Python [9] . For formal verification to succeed, most of these programs require supplementary "annotations" to guide the automated theorem prover. 
related work: 
 As summarized in Table 1 below, there is a striking lack of training data for formal verification: while there are hundreds of thousands of training examples for proving mathematical theorems and over ten thousand training examples for synthesizing programs, there are only 66 + 153 = 219 for proving program correctness. This motivates our work in the current paper to expand the largest existing formal verification benchmarks from Clover [10] and dafny-synthesis [11] .Table 1 : Summary of popular machine learning benchmark datasets for proving mathematical theorems, synthesizing programs, and formally verifying programs. Size is measured by the number of samples in each dataset. In the formal reasoning datasets, each sample is usually a math problem or a theorem. In the program synthesis and verified software programming benchmarks, each sample is a program.Dataset SizeCoqGym [12] 71,000 proofs LeanDojo [13] 98,734 proofs PISA [14] 138,000 proofs Natural Proofs [15] 15,000 proofs Archive of Formal Proofs [16] 1 million lines of codeAPPS [17] 10,000 programs HumanEvalX [18, 19] 165 programs MBPP [20] 974 programs SWEBench [21] 2,294 programs LiveCodeBench [22] grows weeklyFormal software verification Clover [10] 66 programs Dafny-synthesis [11] 153 programs3 DafnyBench Construction 
sourcing ground truth programs: 
 In total, our DafnyBench benchmark contains 782 ground_truth stand-alone Dafny programs that compile and verify. These programs come from the following sources:• GitHub Scrape: We scraped all publicly available Dafny files on GitHub published on and before the end of 2023. We adapted a deduplication script from [23] to retain a unique set of the scraped Dafny files. The deduplication process reduced the number of .dfy files from ∼15,000 to ∼5,000. We removed any files that did not verify, which left 1,112 files. We found 374 of these files lacked ensures statements (postconditions) and 459 of them lacked assert and invariant clauses (annotations), and removed the union of these sets, which left 556 ground_truth files. Out of these files, 113 verify without any annotations.• Clover: We added 62 ground truth textbook Dafny programs provided by the Clover benchmark [10] . Out of these files, 23 verify without any annotations.• Dafny-synthesis: Finally, we included 164 Dafny programs provided by the dafny-synthesis benchmark. These problems have been translated from the MBPP benchmark [11] . Out of these files, 72 verify without any annotations.The ground_truth programs in our dataset have on average 2.12 methods, 1.03 functions, and 1.40 lemmas. This places the mean complexity of our examples at a level higher than Clover [10] alone, which has only one stand-alone method per example. For more detailed summary statistics of DafnyBench dataset, see Appendix A.We implemented the fill_annotations task. For this task, we took a ground_truth program, removed all of its annotations (all of the assert and invariant statements in the body of the code), and asked LLM to fill annotations back in so that the resulting program could be verified with Dafny.  
hyperparameters & prompts: 
 We set max_tokens = 4096, which corresponds to the lowest max output token limit among all the evaluated models, and we set temperature = 0.3. We gave each model up to n = 10 attempts at a given file. If the model failed on any of the intermediate attempts, it received the Dafny error message and was asked to fill in annotations again with the error message taken into consideration. If it failed on all n attempts, it was considered to fail on that specific test program. See Appendix C for prompts.We tested GPT-4o, GPT-4 Turbo [24] , GPT-3.5 Turbo [25] , Claude 3 Opus [2] , and CodeLlama-7b-Instruct-hf [26] on the 782 programs. Table 2 shows that Claude 3 Opus achieved the highest success rate ∼ 68%.Figure 2 shows how the cumulative success rate improved with more attempts n. We see that the best models succeeded on the first try about 54%, with rapidly diminishing returns after that, approaching a plateau at about 65% for n ∼ 5. This suggests that the LLMs are not great at taking Dafny error messages into consideration, or struggle to cope with the underlying task. Figure 3a shows that the success rate drops with program length. An obvious explanation could be that there is more to verify. Also, as a program gets longer, there may be more dependencies among variables, functions, methods, and classes, increasing the overall verification difficulty level.Figure 3b shows that the success rate drops with annotation quantity, defined as the number of characters in the lines of annotations. In other words, the success rate drops with the amount of work that LLM needs to do (the amount of text that it needs to insert in the right places). For visual clarity, the scales are adjusted for both plots and their x-axes do not start at 0 character.To analyze where LLMs failed on the benchmark, we categorized failures into nine types, including verification logic error, code logic error, type error, resolution error, syntax issue, altered specification, timeout, trivial verification, and others. For a test program that a model failed at, we: 1) checked for timeout, cheating by altering specification, and cheating by trivial verification; and 2) passed Dafny error message from the failed program to Claude and asked it to classify the failure type. Table 3 explains each failure type, and Figure 4 gives by-model statistics of failure types.  
discussion & conclusions: 
 We have assembled the largest machine learning benchmark to date for formal software verification and made it publicly available on GitHub at https://github.com/sun-wendy/DafnyBench.Data contamination emerges as a potentially significant limitation for evaluating LLMs on Dafny-Bench. Scraping data from platforms such as GitHub introduces risks of leveraging previous models' training data into the benchmark evaluation, potentially inflating the abilities of certain models.Another limitation emerges in that DafnyBench does not assess a model's competence in translating natural language into concise formal specifications. Arguably, this conversion is a demanding and crucial skill we seek from language models: the capacity to validate, beyond merely verifying code. The pivotal question is whether a model can assist in identifying the essential properties an algorithm must fulfill. This provides an exciting frontier for future work, which we begin to brainstorm in Appendix D.For further discussion on LLM's potential for auto-verifying program synthesis and synthesizing specifications from natural language, see Appendix E.  
 
 Appendix: We based our prompts on the prompts used in the Clover benchmark [10] , one of the previously largest such benchmarks, since they provide a fairly rigorous precedent. We tried to keep prompts mostly the same across models in order to reduce the difference between model performances that is caused by prompts. However, the prompts are not fully identical. For example, when we ask LLM to simply return the annotations-filled program without any explanation, Claude 3 tends to add explanations that interfere with Dafny compilation. Thus, we had to adjust some prompts slightly to fit each model's peculiarities. The prompts for CodeLlama-7b-Instruct-hf are the same as those in C.2.The evaluation of models' capability to generate formal specifications might be enhanced by integrating the process with the creation of positive and negative test cases for each Dafny implementation. This approach proposes a reward system where models are evaluated based on the number of positive test cases their formal specifications support and the number of negative test cases they successfully reject. However, this method introduces a new challenge: ensuring the test cases accurately reflect the comprehensive meaning intended in the natural language descriptions. The consistency and validity of these test cases become critical, raising questions about the methods used to generate and verify them.It will be valuable to further expand formal verification benchmarks, which still remain more than two orders of magnitude smaller than corresponding benchmarks for mathematical theorem proving. One convenient way to expand the number of available problems may involve incorporating Dafny programs from GitHub that have dependencies spread across multiple files (while DafnyBench encompasses increasingly complex multi-step programs, its programs each fit in a single file, avoiding the intricacies associated with distributed files or the integration of external libraries).Perhaps models that perform especially well on this initial benchmark can later be used to expand it by translating existing Python benchmark problems into Dafny, Rust [27] or other popular formal verification languages.A subset of the programs we scraped from GitHub do not have appropriate docstrings. By building a benchmark with better code documentation, models may be able to leverage helpful contextual information to better constructing verification annotations.We evaluated the models with a fixed temperature setting and a max output token limit of 4096, and we used prompts that were manually but not very systematically tuned for effectiveness (see Appendix C) -all of these choices probably leave room for improvement.We do not yet provide an official training dataset or models custom-trained to do well on the DafnyBench evaluation set. However, we do provide the full json file produced by the GitHub scrape, and we separately provide the names of the files we use for the evaluation benchmark. Hence, it is possible for researchers to use files from the Github scrape that are not used in the benchmark as training data, though we cannot at this time provide strong guarantees on similarity between such training problems and the benchmark problems.We also see opportunities for LLM-related innovation on the algorithmic side: out-of-the-box LLMs provide a floor but not a ceiling for possible performance on this benchmark. For example, fine-tuning or search-based inference-time algorithms might boost models' performances on this benchmark [28] .LLMs also have potential to improve formal verification in more profound ways than mentioned above, when used in combination with other AI tools. For example, they can help automate the identification of sub-goals and annotations, reducing the search space for automated theorem provers and SAT solvers. A software developer is likely able to specify the high level assurance properties of a piece of code, but may lack familiarity with the complexities of proof sub-goals and annotations. LLMs offer a way to bridge this gap between software developers and formal verification.Bigger, more general benchmarks can be used to train LLMs to specify sub-goals and annotations in formats most useful to the presently available provers and solvers. Benchmarks covering broad ground, from cryptography, lambda calculus, embedded systems, and avionics, in a variety of widely used programming languages suitable for verification, will help create LLMs that can take real-world software, automatically process and serve it to verification tools, and inform the developer in near real time about the correctness of the code. The problem is analogous to that solved by existing automated theorem provers and model checkers in the domain of mathematics. For a survey on the application of deep learning to automated theorem proving, see [29] .Above we discussed the challenge of verifying existing pre-programs. Anther potential of LLMs is use program-synthesis techniques that produce both programs and proofs of their correctness, all at the same time. This makes intuitive sense, since when a human programmer writes code, they typically have an informal proof in their head for why this code is correct. In other words, in addition to bridging the gap from low level implementation to high level specification in the upward direction, LLMs can offer assistance in generating provably correct low level code from high level specifications via program synthesis.Current approaches to program synthesis enable engineers to encode a desired specification in a high level language, and then through a (hopefully) verified correct compiler generate correct low level code in a language like VHDL [30] or Verilog [31] for hardware synthesis. Program synthesis is limited by the need for a special purpose language or compiler to be constructed and verified correct in its own right. For example, ReWire, a domain specific language defined as a subset of Haskell [32] , was manually verified correct using the Coq Interactive Theorem Prover. In order to add a new high-to-low path, a new language or compiler will need to be defined and verified. If an engineer needs to synthesize correct Verilog rather than VHDL, they would likely need to first learn Caisson [33] .LLMs offer a way to generalize this approach. Starting with a high level language, an engineer might be able to specify a system and then leverage a LLM to generate low level code with the corresponding loop invariants, weakest pre-conditions, strongest post-conditions, etc, included. Early results indicate that an LLM that is able to converse with a human when producing a program can reduce the error rate against a simple programming benchmark by half [20] . If instead of receiving feedback from a human, the LLM were to interact with a suite of formal verification tools, we expect further improvements. The LLM should be capable of generating code that is appropriately annotated for theorem proving, which is exactly the skill assessed by test benches like that described here.We can think about deduplicating a set of files by finding groups of "similar"files and then choosing only one file representative from each group to form our final deduplicated set of files. To do this, we can use the Jaccard similarity metric to decide whether one document is a duplicate of another.The Jaccard similarity metric provides a way to quantify the similarity of two sets. It is defined as [34] :J(A, B) = |A ∩ B| |A ∪ B| .In the application to code files, we could consider each file to be a set of n-grams, where an n-gram is defined as a sequence of n adjacent symbols in a particular order [35] , and then apply the Jaccard score as a similarity metric for our files. To directly calculate this Jaccard score, we would need to run string comparison on every n-gram, which would have time complexity O nm 2 if we have n n-grams each with max length m characters. This turns out to be an inefficient method for representing each code file as a set. Instead, the minhash deduplication algorithm approximates the Jaccard similarity between two documents by shingling the documents and comparing the minhash representation of each set of shingles (i.e. we compare fingerprints of documents instead of full documents). The minhash representation of a document is a way to represent a text document as a set of numbers that is faithful to the structure of its content but with a fixed set size that is smaller than the total number of n-grams in the document (i.e. the minhash representation of the document is a form of numerical fingerprint of the document). In Figure 6 below, we provide the pseudocode for the minhash algorithm used, based entirely on the script in [23] :Note that the probability two files have the same min hash value under the same hash function is equivalent to their Jaccard similarity. Concretely, for file A and file B:Pr [ min h i (A) = min h i (B) ] = J(A, B)where min h i () denotes taking the minimum hash value under hash function h i . This makes sense because, assuming negligible hash collision, Pr [min h i (A) = min h i (B)] is equivalent to the probability that the first n-gram hash of A under h i is equal to the first n-gram hash of B under h i . If h i is a good hash function, then it uniformly distributes the hash values of the original n-gram hashes over the range of h i . Let c denote the number of n-grams with equivalent hashes; let a denote the number of n-grams from A with smaller hash values than the hash value of corresponding n-gram from B; let b denote the reverse of the previous category. Then, Pr [min hi (A) = min h i (B)] = c a+b+c , given the uniformity of h 1 . Note that c a+b+c = |A∩B| |A∪B| = J(A, B).We provide a full list of all repositories whose data we used in the scraped portion of DafnyBench in Tables 5, 6, 7. When reporting the license information, "Renamed so N/A" implies that the original repository we scraped in December 2023 no longer exists under that name. Otherwise, the repositories have either Microsoft open-source licenses, MIT licenses, GNU General Public License v3.0 licenses, Creative Commons Zero v1.0 Universal, Apache 2.0 licenses, or "Other" (which is secretly an MIT License in a strange format, which has been checked manually). In light of this, we release our derivative DafnyBench repository under an Apache 2.0 license and a GNU General Public License v3.0. We note explicitly here that all files from repositories with the Apache 2.0 license have been modified from their original form. * Equal contribution. Order determined alphabetically. † Corresponding author. 



Reviews: review: title: title: Review for DafnyBench
main_review: main_review: DafnyBench is a large benchmark designed to evaluate machine learning models' ability to auto-generate annotations for formal software verification. It includes over 750 Dafny programs and tests models GPT-4 and Claude 3, with the latter achieving a 68% success rate. The benchmark measures how well models generate annotations necessary for the Dafny verification engine to confirm program correctness. Success rates decrease with program length and annotation complexity but improve with error feedback. DafnyBench aims to advance formal verification techniques by integrating machine learning.

DafnyBench offers a valuable dataset, providing a valuable resource for testing machine learning models in formal software verification. Its large size and diverse range of programs enable extensive evaluation of annotation generation capabilities. It also encourages the development of improved LLM-based verification techniques through structured benchmarking.

On the downside, the success rates of state-of-the-art models are already high. The benchmark’s reliance on existing data sources introduces potential contamination from models trained on similar datasets. Moreover, it does not assess a model's ability to translate natural language into formal specifications, a key skill in formal verification.
title: title: Review
main_review: main_review: This paper introduces DafnyBench, a large benchmark for training and evaluating LLMs for Dafny formal verification.
They provide analyses on how the difficulty of a problem changes and how well LLMs are at solving these problems and taking error feedback from Dafny.
DafnyBench will be helpful for future research on LLM for formal verification.

P.S. There is a non-anonymous acknowledgment section. Not sure if it's problematic @AC.
title: title: review
main_review: main_review: **Note to PCs:** The paper is not anonymised. There is a link to a GitHub repo containing the new benchmark, which reveals the authors' names, and the pdf contains list of names in the acknowledgments.

The paper presents a new benchmark for program verification in the Dafny language. The construction follows a standard pipeline: scraping GitHub and appropriately filtering. Different pretrained/fixed LLMs are evaluated on the task of filling in the verification annotations in programs where those annotations have been deleted. The analysis measures the dependence on the error rate on the size of the program and annotations and the distribution of types of errors made by different models.

There is little technical novelty here, but I find it to be a solid benchmark paper and later work can build on it in more extended form. Plenty of directions remain to be explored (fine-tuning, sensitivity to the prompt, syntax-constrained decoding, and so on).

Minor:
- The second sentence of the abstract doesn't make sense to me ('we test the ability to generate enough annotations to successfully verify 750 programs").
- There are some broken `\ref`s.
title: title: Review
main_review: main_review: # Summary

The paper introduces DafnyBench, a code generation benchmark consisting of 556 Dafny files from open-source GitHub repositories, and problems from 2 previous Dafny programming benchmarks (62 from CloverBench and 164 from MBPP-DFY). The paper proposes a new task **fill_annotations** that tests models to generate annotations (assert and invariant statements) for Dafny programs so that they can be verified.


# Strengths

## Originality

This is the first benchmark dataset for Dafny code generation derived from real-world code repositories, making it a valuable resource for the community.



## Quality

1. The paper clearly describes the data curation and evaluation processes, including an in-depth analysis of model performance based on program length, annotation quantity, and error distribution.

2. Appendix F provides insightful discussions on potential future work and opportunities, highlighting the paper’s forward-thinking approach.


## Significance

Automated annotation generation is a practically impactful task that can meaningfully aid Dafny programmers. 



# Weaknesses


## Significance

As mentioned in Section 5.1 Limitations, while automated annotation generation is already beneficial, generating complete Dafny programs with pre-conditions, post-conditions, and annotations could more comprehensively evaluate the models' capability of Dafny programming.

A potential extension of DafnyBench is to synthesize natural language specifications of the corresponding programs using LLMs. Promising natural language specifications can be filtered using Self-Consistency [1] i.e. give the generated natural language specification to the LLM and check if it generates the correct code.

[[1] Beyond Accuracy: Evaluating Self-Consistency of Code Large Language Models with IdentityChain](https://arxiv.org/abs/2310.14053)


# Questions
 
1. Could you clarify the rationale behind retaining the 26.9% of programs that Dafny can verify without any annotations?

2. Based on the error distribution analysis in Appendix D, syntax error is the top 3 error source for all models. It's somewhat expected since Dafny is a low-resource language. Could we curate a list of syntax warnings based on those common syntax errors and append it to the prompt so that the model can be evaluated solely on its logical errors? Alternatively, we can provide feedback when we detect syntax errors (or altered specs), inform the model of the specific error, and prompt it to regenerate.

3. Based on the error distribution analysis in Appendix D, altered specs is surprisingly a prominent issue for `gpt-4o` and `claude-3-opus`, but not for `gpt-4-turbo` or `gpt-3.5-turbo`. Typically, the former models are better at instruction following than the latter ones. Do you have any insights as to why this might be the case?