홈 › Papers

DafnyBench: A Benchmark for Formal Software Verification

2024-06-12 · Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin, Max Tegmark

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 hints 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 hints. We hope that DafnyBench will enable rapid improvements from this baseline as LLMs and verification techniques grow in quality.

📄 PDF Abstract BibTeX arXiv:2406.08467

Code (1)

sun-wendy/dafnybench 공식 구현

Methods 이 논문이 사용한 방법론

Attention 설명 없음

Residual Connection 설명 없음

Softmax The Softmax output function transforms a previous layer's output into a vector of probabilities. It is commonly used for multiclass classification. Given an input vector $x$…

Layer Normalization Unlike batch normalization, Layer Normalization directly estimates the normalization statistics from the summed inputs…

BPE Byte Pair Encoding, or BPE, is a subword segmentation algorithm that encodes rare and unknown words as sequences of subword units. The intuition is that various word…

Label Smoothing Label Smoothing is a regularization technique that introduces noise for the labels. This accounts for the fact that datasets may have mistakes in them, so maximizing the…

Adam 설명 없음

Linear Layer A Linear Layer is a projection $\mathbf{XW + b}$.

dafny-annotator: AI-Assisted Verification of Dafny Programs

2024-11-05 · Gabriel Poesia, Chloe Loughridge, Nada Amin

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 verifi…

Friction

AxDafny: Agentic Verified Code Generation in Dafny

2026-06-30 · Benjamin Breen, Austin Letson, Borja Requena Pozo, Leopoldo Sarra arxiv

We study agentic code generation in Dafny, where a model must generate both executable code and the proof artifacts for verification. We present AxDafny, a verifier-guided repair framework that iteratively generates impl…

Code Generation

Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK

2025-02-11 · Marcos Cramer, Lucian McIntyre

Large language models (LLMs) have demonstrated remarkable code generation capabilities, but the correctness of the generated code cannot be inherently trusted. This paper explores the feasibility of using formal software…

Code Generation

Inferring multiple helper Dafny assertions with LLMs

2025-10-31 · Álvaro Silva, Alexandra Mendes, Ruben Martins arxiv

The Dafny verifier provides strong correctness guarantees but often requires numerous manual helper assertions, creating a significant barrier to adoption. We investigate the use of Large Language Models (LLMs) to automa…

Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview

2025-03-13 · Norbert Tihanyi, Tamas Bisztray, Mohamed Amine Ferrag, Bilel Cherif 외

Software testing and verification are critical for ensuring the reliability and security of modern software systems. Traditionally, formal verification techniques, such as model checking and theorem proving, have provide…

Automated Theorem Proving software testing Vulnerability Detection