Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs
summary
An automated repair pipeline for Dafny uses Hoare logic to localize arithmetic faults, prompts LLMs (GPT-4o mini, Llama 3, Mistral 7B, Llemma 7B) to synthesize single-line patches, and re-verifies with the Dafny verifier; implemented in C and able to call local models or APIs. Evaluation on DafnyBench shows 89.7% fault localization and GPT-4o mini achieves 74.18% repair success (over 80% reproduce original fixes); it assumes correct specifications and currently targets only arithmetic bugs.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 2:13Formal specs strengthen repair
- 4:04Repair pipeline overview
- 5:29Fault localization with Hoare logic
- 7:58LLM patch generation
- 8:42Patch validation
- 9:46Dafny benchmarks evaluation
- 12:13Limitations and challenges
- 13:15Future work
- 14:43Key takeaways
related talks
23mdafny-annotator: AI-Assisted Verification of Dafny Programs
18mDafnyBench: A Benchmark for Formal Software Verification
15mLaurel: Unblocking Automated Verification with Large Language Models
15mDafny as Verification-Aware Intermediate Language for Code Generation
18mLaurel: Unblocking Automated Verification with Large Language Models
53mSemantics-based program manipulation in the age of LLMs
22mTowards Verified Code Reasoning by LLMs
37mGPT-3-Powered Type Error Debugging: Investigating the Use of Large Language Models...