用形式化规范提升LLM生成修复测试质量，但真实场景仍难落地
From Benchmark Data To Applicable Program Repair: An Experience Report
- 用形式化规范增强代码，让LLM生成更高质量的单元测试
- 对复杂生产代码覆盖率与异常处理有明显提升，但基准表现不等于实际有效
- 适合关注工业级修复实用性的研究者，尤其关注人机协作与可测性
本文提出一种自动化程序修复方法，融合文献中的多种技术。实验表明该方法在标准基准上优于其他技术，但深入分析发现其无法解决工业界常见的真实缺陷。我们发现，为代码添加形式化规范可显著提升LLM生成单元测试的质量，尤其在复杂生产代码中增强了边缘情况和异常处理的覆盖。然而，对于已知错误（如空指针、下标越界）规范作用有限，主要利好逻辑与字符串操作类错误。尽管基准结果令人鼓舞，但真实应用受限——通过测试不等于修复正确。当前挑战包括JML语言表达力不足，需更强大的验证工具与丰富谓词支持。后续工作聚焦合同自动机、示例编程与测试用例修复，强调人机反馈整合与生产力评估，凸显学术基准与工业需求间的鸿沟。
原文摘要 · Abstract (English)
This paper describes our approach to automated program repair. We combine various techniques from the literature to achieve this. Our experiments show that our approach performs better than other techniques on standard benchmarks. However, on closer inspection, none of these techniques work on realistic defects that we see in industry. We find that augmenting code with formal specifications enables LLMs to generate higher-quality unit tests, especially for complex production code with improved coverage of edge cases and exception handling. However, specifications add little value for well-understood errors (e.g., null pointer, index out of bounds), but are beneficial for logic and string manipulation errors. Despite encouraging benchmark results, real-world adoption is limited since passing tests do not guarantee correct patches. Current challenges include insufficient expressiveness of the JML specification language, necessitating advanced verification tools and richer predicates. Our ongoing work is exploring contract automata, programming by example, and testcase repair, with a focus on integrating human feedback and measuring productivity gains - highlighting the gap between academic benchmarks and practical industry needs
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。