结合零样本学习与基于 MaxSAT 的错误定位的反例引导程序修复

针对入门编程作业的自动程序修复受到每年大量学生选修编程课程的驱动。由于对 IPA 提供反馈需要教师投入大量时间和精力，个性化反馈通常涉及向学生建议其程序的修复方案。基于形式化方法的语义修复方法通过测试套件或参考解来检查程序的执行，虽然有效但存在局限性。这些工具擅长识别错误部分，但只有在正确实现和错误实现共享相同控制流图时才能修复程序。相反，大型语言模型被用于 APR，但经常进行大范围而非最小化的重写。这导致修复更具侵入性，使学生更难从错误中学习。总而言之，LLM 擅长补全字符串，而基于 FM 的错误定位擅长识别程序的错误部分。在本文中，我们提出了一种新颖的方法，通过零样本学习结合基于 FM 的错误定位和 LLM 的优势，以增强针对 IPA 的 APR。我们的方法使用基于 MaxSAT 的错误定位来识别程序的错误部分，然后向 LLM 呈现一个去除了这些错误语句的程序草图。这种混合方法遵循 CEGIS 循环以迭代地改进程序。我们要求 LLM 合成缺失的部分，然后针对测试套件进行检查。如果建议的程序不正确，测试套件中的反例将被反馈给 LLM。我们的实验表明，我们使用基于 MaxSAT 的无错误程序草图的反例引导方法，显著提高了所有六个评估 LLM 的修复能力。该方法允许 LLM 用更小的修复修复更多程序，优于其他配置和最先进的符号程序修复工具。