Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs

TL;DR

This paper introduces a formal specification-guided automated repair tool for Dafny programs that leverages LLMs to fix arithmetic errors, achieving high fault localization and repair success rates.

Contribution

It presents a novel approach combining formal specifications and LLMs for fault localization and repair in Dafny programs, focusing on arithmetic bugs.

Findings

89.6% fault localization coverage

74.18% repair success rate with GPT-4o mini

Effective combination of formal reasoning and LLMs

Abstract

Debugging and repairing faults when programs fail to formally verify can be complex and time-consuming. Automated Program Repair (APR) can ease this burden by automatically identifying and fixing faults. However, traditional APR techniques often rely on test suites for validation, but these may not capture all possible scenarios. In contrast, formal specifications provide strong correctness criteria, enabling more effective automated repair. In this paper, we present an APR tool for Dafny, a verification-aware programming language that uses formal specifications - including pre-conditions, post-conditions, and invariants - as oracles for fault localization and repair. Assuming the correctness of the specifications and focusing on arithmetic bugs, we localize faults through a series of steps, which include using Hoare logic to determine the state of each statement within the program, and applying Large Language Models (LLMs) to synthesize candidate fixes. The models considered are GPT-4o mini, Llama 3, Mistral 7B, and Llemma 7B. We evaluate our approach using DafnyBench, a benchmark of real-world Dafny programs. Our tool achieves 89.6% fault localization coverage and GPT-4o mini yields the highest repair success rate of 74.18%. These results highlight the potential of combining formal reasoning with LLM-based program synthesis for automated program repair.