用大模型提升复杂程序循环不变量生成能力，效果优于现有工具。
Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models
- 结合静态分析与大模型生成循环不变量，自动提取关键信息注入提示词。
- 在含数据结构的测试集上解决率比AutoSpec高21%，整体表现更优。
- 适合需要自动化验证复杂代码的开发者和形式化验证研究者。
自动化程序验证是构建可信软件的重要环节。尽管真实程序的分析仍是理论难题，循环不变量的自动化生成已有效解决该问题。然而，现实程序常混合复杂数据结构与控制流，对传统不变量生成工具构成挑战。为此，我们提出ACInv——一种融合静态分析与大语言模型（LLM）的复杂程序循环不变量生成工具。通过静态分析提取每个循环的关键信息，并嵌入提示词中，由LLM生成初始不变量；再利用基于LLM的评估器判断其正确性，通过强化、弱化或拒绝进行迭代优化，最终获得增强后的不变量。实验表明，ACInv在包含数据结构的数据集上优于此前工具，在无数据结构的数值程序上性能与当前最优工具AutoSpec相当。在总数据集上，ACInv可多解决21%的实例，并能生成参考数据结构模板。
原文摘要 · Abstract (English)
Automated program verification has always been an important component of building trustworthy software. While the analysis of real-world programs remains a theoretical challenge, the automation of loop invariant analysis has effectively resolved the problem. However, real-world programs that often mix complex data structures and control flows pose challenges to traditional loop invariant generation tools. To enhance the applicability of invariant generation techniques, we proposed ACInv, an Automated Complex program loop Invariant generation tool, which combines static analysis with Large Language Models (LLMs) to generate the proper loop invariants. We utilize static analysis to extract the necessary information for each loop and embed it into prompts for the LLM to generate invariants for each loop. Subsequently, we employ an LLM-based evaluator to assess the generated invariants, refining them by either strengthening, weakening, or rejecting them based on their correctness, ultimately obtaining enhanced invariants. We conducted experiments on ACInv, which showed that ACInv outperformed previous tools on data sets with data structures, and maintained similar performance to the state-of-the-art tool AutoSpec on numerical programs without data structures. For the total data set, ACInv can solve 21% more examples than AutoSpec and can generate reference data structure templates.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。