评测大模型生成与修复循环不变式的能力，发现加辅助信息后效果显著提升。
LLM For Loop Invariant Generation and Fixing: How Far Are We?
- 用大模型自动推导循环不变式，结合示例和领域知识提升效果
- 生成正确不变式成功率最高达78%，修复错误不变式仅16%
- 适合研究程序验证或大模型在形式化方法中应用的开发者
循环不变式是循环执行前后始终保持为真的性质，对自动化程序安全评估至关重要。近年来，大语言模型（LLM）在软件工程与形式化验证任务中展现出潜力。本文首次系统评估了不同规模的开源与闭源大模型在生成和修复归纳性循环不变式方面的能力。结果表明，尽管大模型具备一定生成与修复能力，但性能显著依赖于辅助信息，如领域知识和示例。在生成任务中，最大成功率达78%；而在修复错误不变式时，成功率仅为16%。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。