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

• URL: http://arxiv.org/abs/2507.03659v1
• Date: Fri, 04 Jul 2025 15:36:12 GMT
• Title: Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs
• Authors: Valentina Wu, Alexandra Mendes, Alexandre Abreu,
• Abstract summary: We present an innovative APR tool for Dafny, a verification-aware programming language.<n>We localize faults through a series of steps, which include using Hoare Logic to determine the state of each statement within the program.<n>We evaluate our approach using DafnyBench, a benchmark of real-world Dafny programs.
• Score: 84.30534714651093
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal verification offers strong assurances of software correctness. However, debugging and repairing the underlying faults can be complex and time-consuming when verification fails. Automated Program Repair (APR) aims to ease this by automatically identifying and fixing faults. Traditional APR techniques often depend on test suites for validation, but these may fail to capture all scenarios. In contrast, formal specifications provide stronger correctness criteria for effective repairs. We present an innovative 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 state-of-the-art Large Language Models (LLMs) to synthesize candidate fixes. The chosen models were 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% accuracy in fault localization, with GPT-4o mini yielding the highest repair success rate (74.18%). These results highlight the potential of combining formal reasoning with LLM-driven program synthesis for automated program repair.

Related papers

• Do AI models help produce verified bug fixes? [62.985237003585674]
  Large Language Models are used to produce corrections to software bugs.<n>This paper investigates how programmers use Large Language Models to complement their own skills.<n>The results are a first step towards a proper role for AI and LLMs in providing guaranteed-correct fixes to program bugs.
  arXiv  Detail & Related papers  (2025-07-21T17:30:16Z)
• Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization [0.0]
  Automated Program Repair (APR) for introductory programming assignments (IPAs) is motivated by the large number of student enrollments.<n>We propose a novel approach that combines the strengths of both FM-based fault localization and Large Language Models (LLMs)<n>Our method uses MaxSAT-based fault localization to identify buggy parts of a program, then presents the LLM with a program sketch devoid of these buggy statements.
  arXiv  Detail & Related papers  (2024-12-19T12:08:44Z)
• Subtle Errors in Reasoning: Preference Learning via Error-injected Self-editing [59.405145971637204]
  We propose a novel preference learning framework called eRror-Injected Self-Editing (RISE)<n>RISE injects predefined subtle errors into pivotal tokens in reasoning or steps to construct hard pairs for error mitigation.<n>Experiments validate the effectiveness of RISE, with preference learning on Qwen2-7B-Instruct yielding notable improvements of 3.0% on GSM8K and 7.9% on MATH with only 4.5K training samples.
  arXiv  Detail & Related papers  (2024-10-09T07:43:38Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  Large language models (LLMs) struggle with consistent and accurate reasoning. LLMs are trained primarily on correct solutions, reducing their ability to detect and learn from errors. We propose a novel collaborative method integrating Chain-of-Thought (CoT) and Program-of-Thought (PoT) solutions for verification.
  arXiv  Detail & Related papers  (2024-10-05T05:21:48Z)
• A Deep Dive into Large Language Models for Automated Bug Localization and Repair [12.756202755547024]
  Large language models (LLMs) have shown impressive effectiveness in various software engineering tasks, including automated program repair (APR) In this study, we take a deep dive into automated bug fixing utilizing LLMs. This methodological separation of bug localization and fixing using different LLMs enables effective integration of diverse contextual information. Toggle achieves the new state-of-the-art (SOTA) performance on the CodeXGLUE code refinement benchmark.
  arXiv  Detail & Related papers  (2024-04-17T17:48:18Z)
• An Empirical Evaluation of Pre-trained Large Language Models for Repairing Declarative Formal Specifications [7.286515881369693]
  This paper systematically investigates the capacity of Large Language Models (LLMs) to repair declarative specifications in Alloy.<n>We designed 12 different repair settings, encompassing single-agent and dual-agent paradigms, utilizing various LLMs.<n>Our study reveals that dual-agent with auto-prompting setup outperforms the other settings, albeit with a marginal increase in the number of iterations and token usage.
  arXiv  Detail & Related papers  (2024-04-17T03:46:38Z)
• Aligning the Objective of LLM-based Program Repair [14.935596175148586]
  This paper investigates a new approach to adapt large language models (LLMs) to program repair.<n>Our core insight is that LLM's APR capability can be greatly improved by simply aligning the output to their training objective.<n>Based on this insight, we designed D4C, a straightforward prompting framework for APR.
  arXiv  Detail & Related papers  (2024-04-13T02:36:40Z)
• A Novel Approach for Automatic Program Repair using Round-Trip Translation with Large Language Models [50.86686630756207]
  Research shows that grammatical mistakes in a sentence can be corrected by translating it to another language and back. Current generative models for Automatic Program Repair (APR) are pre-trained on source code and fine-tuned for repair. This paper proposes bypassing the fine-tuning step and using Round-Trip Translation (RTT): translation of code from one programming language to another programming or natural language, and back.
  arXiv  Detail & Related papers  (2024-01-15T22:36:31Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  We present a holistic end-to-end solution for annotating the factuality of large language models (LLMs)-generated responses. We construct an open-domain document-level factuality benchmark in three-level granularity: claim, sentence and document. Preliminary experiments show that FacTool, FactScore and Perplexity are struggling to identify false claims.
  arXiv  Detail & Related papers  (2023-11-15T14:41:57Z)
• Is Self-Repair a Silver Bullet for Code Generation? [68.02601393906083]
  Large language models have shown remarkable aptitude in code generation, but still struggle to perform complex tasks. Self-repair -- in which the model debugs and repairs its own code -- has recently become a popular way to boost performance. We analyze Code Llama, GPT-3.5 and GPT-4's ability to perform self-repair on problems taken from HumanEval and APPS.
  arXiv  Detail & Related papers  (2023-06-16T15:13:17Z)
• Fully Autonomous Programming with Large Language Models [0.9558392439655015]
  Current approaches to program synthesis with Large Language Models (LLMs) exhibit a "near miss syndrome" We use OpenAI Codex as the LLM and Program Synthesis Benchmark 2 as a database of problem descriptions and tests for evaluation. The resulting framework outperforms both conventional usage of Codex without the repair phase and traditional genetic programming approaches.
  arXiv  Detail & Related papers  (2023-04-20T16:12:05Z)

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.