Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization
作者: Pedro Orvalho, Mikoláš Janota, Vasco Manquinho
分类: cs.SE, cs.AI
发布日期: 2024-12-19
备注: Accepted at AAAI 2025. 11 pages, 4 listings, 2 figures and 5 tables
💡 一句话要点
结合零样本学习与MaxSAT故障定位，提升LLM在程序自动修复中的性能
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 程序自动修复 大型语言模型 零样本学习 MaxSAT 故障定位 CEGIS 编程教育
📋 核心要点
- 现有基于形式化方法的程序修复工具依赖于控制流图相似性，而大型语言模型的修复则过于激进，不利于学生学习。
- 本文提出一种混合方法，利用MaxSAT故障定位识别错误代码，并引导LLM在无错程序草图上进行零样本学习修复。
- 实验结果表明，该方法显著提升了LLM的程序修复能力，修复更多程序的同时，修复范围更小，效果优于现有方法。
📝 摘要（中文）
针对编程入门作业（IPAs）的自动程序修复（APR）旨在解决编程课程中学生数量庞大导致的教师负担问题。基于形式化方法（FM）的语义修复方法通过检查程序执行与测试套件或参考解决方案的一致性来工作，但其修复能力受限于程序控制流图的相似性。另一方面，大型语言模型（LLMs）虽然能用于APR，但常进行大范围重写，不利于学生学习。本文提出一种新方法，结合FM故障定位和LLMs的优势，通过零样本学习增强IPAs的APR。该方法使用基于MaxSAT的故障定位识别程序中的错误部分，然后向LLM提供一个不包含这些错误语句的程序草图。这种混合方法遵循CEGIS循环迭代改进程序。LLM负责合成缺失部分，并通过测试套件进行验证。如果程序不正确，则将测试套件中的反例反馈给LLM。实验表明，使用基于MaxSAT的无错程序草图的反例引导方法显著提高了六个评估LLM的修复能力。该方法使LLM能够修复更多程序，且修复更小，优于其他配置和最先进的符号程序修复工具。
🔬 方法详解
问题定义：论文旨在解决程序自动修复（APR）领域中，现有方法在修复编程入门作业（IPAs）时存在的不足。具体来说，基于形式化方法的APR工具依赖于程序控制流图的相似性，限制了其修复能力；而直接使用大型语言模型（LLMs）进行APR往往会产生过于激进的修改，不利于学生理解和学习。因此，需要一种既能精确定位错误，又能生成合理修复的APR方法。
核心思路：论文的核心思路是结合形式化方法和LLMs的优势。首先，使用基于MaxSAT的故障定位技术精确定位程序中的错误部分。然后，将程序中错误部分移除，形成一个“程序草图”，并将其输入到LLM中，让LLM基于零样本学习补全缺失的代码。通过这种方式，可以利用形式化方法的精确性来指导LLM的修复过程，避免LLM产生过于激进的修改。
技术框架：整体框架采用CEGIS（Counterexample-Guided Inductive Synthesis）循环。主要包含以下几个阶段：1) 故障定位：使用基于MaxSAT的故障定位技术识别程序中的错误部分。2) 程序草图生成：从原始程序中移除错误部分，生成程序草图。3) LLM代码合成：将程序草图输入到LLM中，LLM生成缺失的代码片段。4) 测试与验证：使用测试套件验证合成后的程序。如果程序通过所有测试，则修复成功；否则，将测试失败的反例反馈给LLM，重复代码合成和测试过程。
关键创新：最重要的技术创新点在于将基于MaxSAT的故障定位与LLM的零样本学习相结合。这种混合方法能够充分利用形式化方法的精确性和LLM的生成能力，从而实现更有效、更合理的程序修复。与现有方法相比，该方法能够更精确地定位错误，并生成更小的修复，从而更有利于学生学习。
关键设计：论文的关键设计包括：1) 使用MaxSAT进行故障定位的具体方法（未知，论文中未详细描述）。2) 如何将程序草图有效地输入到LLM中，以便LLM能够理解程序上下文并生成正确的代码（未知，论文中未详细描述）。3) 如何选择合适的LLM，并针对APR任务进行优化（未知，论文中未详细描述）。4) CEGIS循环中，反例的选择策略（未知，论文中未详细描述）。
🖼️ 关键图片
📊 实验亮点
实验结果表明，该方法显著提高了六个评估LLM的程序修复能力。与现有方法相比，该方法能够修复更多程序，并且修复的范围更小。具体性能数据和对比基线在摘要中有所提及，但未提供详细的数值结果。该方法优于其他配置和最先进的符号程序修复工具。
🎯 应用场景
该研究成果可应用于在线编程教育平台、自动评测系统等场景，帮助教师减轻批改作业的负担，并为学生提供个性化的修复建议。通过更精确、更易于理解的修复方案，促进学生对编程错误的理解和学习，提高编程能力。未来，该方法有望扩展到更复杂的程序修复任务中。
📄 摘要（原文）
Automated Program Repair (APR) for introductory programming assignments (IPAs) is motivated by the large number of student enrollments in programming courses each year. Since providing feedback on IPAs requires substantial time and effort from faculty, personalized feedback often involves suggesting fixes to students' programs. Formal Methods (FM)-based semantic repair approaches, check a program's execution against a test suite or reference solution, are effective but limited. These tools excel at identifying buggy parts but can only fix programs if the correct implementation and the faulty one share the same control flow graph. Conversely, Large Language Models (LLMs) are used for APR but often make extensive instead of minimal rewrites. This leads to more invasive fixes, making it harder for students to learn from their mistakes. In summary, LLMs excel at completing strings, while FM-based fault localization excel at identifying buggy parts of a program. In this paper, we propose a novel approach that combines the strengths of both FM-based fault localization and LLMs, via zero-shot learning, to enhance APR for IPAs. 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. This hybrid approach follows a CEGIS loop to iteratively refine the program. We ask the LLM to synthesize the missing parts, which are then checked against a test suite. If the suggested program is incorrect, a counterexample from the test suite is fed back to the LLM. Our experiments show that our counterexample guided approach, using MaxSAT-based bug-free program sketches, significantly improves the repair capabilities of all six evaluated LLMs. This method allows LLMs to repair more programs with smaller fixes, outperforming other configurations and state-of-the-art symbolic program repair tools.