Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models

📄 arXiv: 2412.10483v3 📥 PDF

作者: Ruibang Liu, Minyu Chen, Ling-I Wu, Jingyu Ke, Guoqiang Li

分类: cs.SE, cs.AI, cs.PL

发布日期: 2024-12-13 (更新: 2025-09-16)

备注: 26 pages, 11 figures

💡 一句话要点

ACInv：结合静态分析与大语言模型，提升复杂程序循环不变式自动生成

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 循环不变式生成 程序自动验证 大语言模型 静态分析 复杂程序 数据结构 LLM评估

📋 核心要点

  1. 现有循环不变式生成工具难以处理包含复杂数据结构和控制流的现实程序。
  2. ACInv结合静态分析提取循环信息，利用大语言模型生成和评估循环不变式。
  3. 实验表明，ACInv在包含数据结构的数据集上优于现有工具，整体问题解决率提升21%。

📝 摘要（中文）

程序自动验证是构建可信软件的重要组成部分。现实程序分析面临理论挑战，而循环不变式分析的自动化有效缓解了该问题。然而，现实程序常混合复杂数据结构和控制流，对传统循环不变式生成工具构成挑战。为提高不变式生成技术的适用性，我们提出了ACInv，一种自动复杂程序循环不变式生成工具，它结合静态分析与大语言模型（LLM）来生成合适的循环不变式。我们利用静态分析提取每个循环的必要信息，并将其嵌入到LLM的提示中，以生成每个循环的不变式。随后，我们采用基于LLM的评估器来评估生成的不变式，通过加强、减弱或拒绝它们来改进不变式，最终获得增强的不变式。ACInv的实验表明，在包含数据结构的数据集上，ACInv优于之前的工具，并且在没有数据结构的数值程序上，保持了与最先进工具AutoSpec相似的性能。对于整个数据集，ACInv比AutoSpec多解决了21%的例子，并且可以生成参考数据结构模板。

🔬 方法详解

问题定义：论文旨在解决复杂程序中循环不变式自动生成的问题。现有方法在处理包含复杂数据结构和控制流的程序时表现不佳，生成的循环不变式不够准确或无法生成，导致程序验证失败。

核心思路：论文的核心思路是结合静态分析和大语言模型（LLM）的优势。静态分析用于提取循环的关键信息，LLM则用于生成和评估循环不变式。通过这种结合，可以更好地处理复杂程序中的数据结构和控制流。

技术框架：ACInv的整体框架包含以下几个主要阶段：1. 静态分析：提取循环的控制流信息、变量信息等。2. LLM提示生成：将提取的信息嵌入到LLM的提示中。3. LLM不变式生成：利用LLM生成循环不变式。4. LLM不变式评估：使用LLM评估生成的不变式的正确性。5. 不变式改进：根据评估结果，加强、减弱或拒绝生成的不变式。

关键创新：关键创新在于将静态分析与LLM相结合，利用LLM的强大生成能力和评估能力来提升循环不变式生成的准确性和效率。与传统方法相比，ACInv能够更好地处理复杂数据结构和控制流，从而提高程序验证的成功率。

关键设计：LLM提示的设计至关重要，需要包含循环的控制流信息、变量信息以及目标循环不变式的类型等。LLM评估器的设计也需要仔细考虑，需要能够准确评估生成的不变式的正确性，并给出改进建议。具体LLM的选择和微调策略未知。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

ACInv在包含数据结构的数据集上优于之前的工具，并在没有数据结构的数值程序上保持了与AutoSpec相似的性能。在整个数据集上，ACInv比AutoSpec多解决了21%的例子，展示了其在处理复杂程序循环不变式生成方面的优势。此外，ACInv还可以生成参考数据结构模板，为程序理解和验证提供更多信息。

🎯 应用场景

该研究成果可应用于软件自动验证、程序调试和代码质量评估等领域。通过自动生成准确的循环不变式，可以提高程序验证的效率和可靠性，减少人工干预，从而降低软件开发和维护成本。未来，该技术有望应用于更广泛的软件工程领域，例如安全漏洞检测和代码自动修复。

📄 摘要（原文）

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.