Do AI models help produce verified bug fixes?
作者: Li Huang, Ilgiz Mustafin, Marco Piccioni, Alessandro Schena, Reto Weber, Bertrand Meyer
分类: cs.SE, cs.AI
发布日期: 2025-07-21 (更新: 2025-08-04)
💡 一句话要点
研究AI模型辅助程序修复的有效性，揭示LLM在调试中的实际作用与程序员行为模式。
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 自动程序修复 大型语言模型 程序调试 形式化验证 程序员行为分析
📋 核心要点
- 自动程序修复（APR）面临挑战，现有方法难以保证修复的正确性，且缺乏对程序员与AI协同工作的深入理解。
- 本研究通过可验证的程序修复环境，对比分析了有无LLM辅助下程序员的调试行为，旨在揭示LLM在程序修复中的实际作用。
- 初步实验结果表明，LLM在调试中的表现与预期存在差异，研究还提出了调试实验方法，分析了程序员行为模式。
📝 摘要（中文）
大型语言模型（LLM）在自动程序修复（APR）领域展现出巨大潜力。为了验证这一潜力，并探究程序员如何利用LLM提升调试效率，本研究设计了一项实验，将程序员随机分为两组，一组可以使用LLM，另一组不能，两组都使用程序验证工具来验证修复方案的正确性。研究采用Goal-Query-Metric方法，从通用研究问题、具体问题和可衡量指标三个层面进行分析。初步结果揭示了AI在调试和APR中的实际作用与预期存在差异。此外，本研究还提出了调试实验的详细方法，分析了程序员行为，定义了LLM的使用模式，并为利用LLM进行调试和APR提供了建议。
🔬 方法详解
问题定义：论文旨在研究大型语言模型（LLM）在自动程序修复（APR）中的实际效用。现有方法主要痛点在于，缺乏对LLM辅助下程序员调试行为的细致分析，以及对修复方案正确性的严格验证。简单地使用LLM可能无法达到预期的修复效果，甚至可能引入新的错误。
核心思路：论文的核心思路是通过受控实验，对比有无LLM辅助的两组程序员在调试过程中的表现，并利用程序验证工具对提出的修复方案进行形式化验证。通过这种方式，可以更客观地评估LLM的实际贡献，并深入了解程序员与LLM的交互模式。
技术框架：研究采用Goal-Query-Metric（GQM）方法，将研究目标分解为具体问题（Queries）和可衡量指标（Metrics）。实验中，程序员被随机分配到两个组：实验组（可以使用LLM）和对照组（不能使用LLM）。两组程序员都需要使用程序验证工具来验证其修复方案的正确性。研究记录了程序员的完整会话过程，以便进行细粒度的行为分析。
关键创新：本研究的关键创新在于：1) 使用形式化验证工具来保证修复方案的正确性，避免了传统APR方法中常见的过度拟合问题；2) 通过对比实验，深入分析了LLM对程序员调试行为的影响，揭示了LLM的实际作用与预期之间的差异；3) 提出了LLM在调试中的使用模式分类，为后续研究提供了参考。
关键设计：实验中，关键设计包括：1) 随机分组，确保两组程序员的初始能力相当；2) 使用相同的程序验证工具，保证验证过程的公平性；3) 记录完整的会话过程，以便进行细粒度的行为分析；4) 定义清晰的GQM，确保研究目标明确，结果可衡量。
🖼️ 关键图片
📊 实验亮点
研究结果表明，LLM在调试中的表现与预期存在差异，提示开发者需要谨慎使用AI工具。研究还总结了7种不同的LLM使用模式，为开发者提供了利用LLM进行调试的实用建议。通过对程序员行为的细粒度分析，揭示了LLM对调试过程的潜在影响。
🎯 应用场景
该研究成果可应用于软件开发和维护领域，帮助开发者更有效地利用AI工具进行程序调试和修复。通过理解LLM在调试中的实际作用和程序员的行为模式，可以开发出更智能、更可靠的AI辅助调试工具，提高软件质量和开发效率。此外，该研究提出的实验方法和分析框架也可为其他AI辅助软件工程领域的研究提供借鉴。
📄 摘要（原文）
Among areas of software engineering where AI techniques -- particularly, Large Language Models -- seem poised to yield dramatic improvements, an attractive candidate is Automatic Program Repair (APR), the production of satisfactory corrections to software bugs. Does this expectation materialize in practice? How do we find out, making sure that proposed corrections actually work? If programmers have access to LLMs, how do they actually use them to complement their own skills? To answer these questions, we took advantage of the availability of a program-proving environment, which formally determines the correctness of proposed fixes, to conduct a study of program debugging with two randomly assigned groups of programmers, one with access to LLMs and the other without, both validating their answers through the proof tools. The methodology relied on a division into general research questions (Goals in the Goal-Query-Metric approach), specific elements admitting specific answers (Queries), and measurements supporting these answers (Metrics). While applied so far to a limited sample size, the results are a first step towards delineating a proper role for AI and LLMs in providing guaranteed-correct fixes to program bugs. These results caused surprise as compared to what one might expect from the use of AI for debugging and APR. The contributions also include: a detailed methodology for experiments in the use of LLMs for debugging, which other projects can reuse; a fine-grain analysis of programmer behavior, made possible by the use of full-session recording; a definition of patterns of use of LLMs, with 7 distinct categories; and validated advice for getting the best of LLMs for debugging and Automatic Program Repair.