LLM 用于循环不变量生成与修复：我们离目标还有多远？
LLM For Loop Invariant Generation and Fixing: How Far Are We?
AI总结：
本文实证评估了不同规模开源与闭源大语言模型在循环不变量生成与修复任务中的表现，发现其生成成功率达78%、修复仅16%，并证明补充领域知识和示例可显著提升性能。
摘要：
循环不变量是循环的一种性质，在循环每次执行之前和之后都保持为真。识别循环不变量是支持自动化程序安全评估的关键步骤。大语言模型（LLMs）的最新进展已在多种软件工程（SE）和形式化验证任务中展现出潜力。然而，我们尚不清楚 LLM 推断循环不变量的表现。我们报告了一项针对不同规模的开源和闭源 LLM 的实证研究，以评估它们在为程序推断归纳循环不变量以及修复错误不变量方面的能力。我们的发现表明，尽管 LLM 在推断和修复循环不变量方面表现出一定的实用性，但当补充辅助信息（如领域知识和示例说明）时，其性能会显著提升。LLM 在生成不变量方面的最高成功率为 78%，但在修复不变量方面仅为 16%。
英文摘要：
A loop invariant is a property of a loop that remains true before and after each execution of the loop. The identification of loop invariants is a critical step to support automated program safety assessment. Recent advancements in Large Language Models (LLMs) have demonstrated potential in diverse software engineering (SE) and formal verification tasks. However, we are not aware of the performance of LLMs to infer loop invariants. We report an empirical study of both open-source and closed-source LLMs of varying sizes to assess their proficiency in inferring inductive loop invariants for programs and in fixing incorrect invariants. Our findings reveal that while LLMs exhibit some utility in inferring and repairing loop invariants, their performance is substantially enhanced when supplemented with auxiliary information such as domain knowledge and illustrative examples. LLMs achieve a maximum success rate of 78\% in generating, but are limited to 16\% in repairing the invariant.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
