Ranking LLM-Generated Loop Invariants for Program Verification

📄 arXiv: 2310.09342v3 📥 PDF

作者: Saikat Chakraborty, Shuvendu K. Lahiri, Sarah Fakhoury, Madanlal Musuvathi, Akash Lal, Aseem Rastogi, Aditya Senthilnathan, Rahul Sharma, Nikhil Swamy

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

发布日期: 2023-10-13 (更新: 2024-02-12)

备注: Findings of The 2023 Conference on Empirical Methods in Natural Language Processing (EMNLP-findings 2023)

🔗 代码/项目: GITHUB

💡 一句话要点

提出重排序方法以优化LLM生成的循环不变式

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

关键词: 循环不变式 程序验证 大型语言模型 重排序 自动化测试 对比学习

📋 核心要点

  1. 现有方法在生成循环不变式时需要多个样本，导致对程序验证器的频繁调用，效率低下。
  2. 本研究提出了一种重排序方法，通过优化排序器来区分正确与错误的循环不变式，减少验证调用。
  3. 实验结果显示，重排序机制显著提高了正确不变式的排名，减少了验证器调用次数，提升了效率。

📝 摘要（中文）

合成归纳循环不变式是自动化程序验证的基础。在本研究中，我们观察到大型语言模型（如gpt-3.5或gpt-4）能够在零样本设置下为某类程序合成循环不变式，但需要多个样本才能生成正确的不变式。这可能导致大量调用程序验证器以确立不变式。为了解决这个问题，我们提出了一种针对LLM生成结果的重排序方法。我们设计了一种能够根据问题定义区分正确归纳不变式和错误尝试的排序器。实验结果表明，这种重排序机制显著提高了生成候选中正确不变式的排名，从而显著减少了对验证器的调用次数。

🔬 方法详解

问题定义：本论文旨在解决大型语言模型在生成循环不变式时效率低下的问题。现有方法需要多个样本来生成正确的不变式，导致频繁调用程序验证器，增加了计算成本。

核心思路：论文提出了一种重排序方法，通过设计一个排序器来优化生成的不变式结果。该排序器能够有效区分正确的归纳不变式和错误的尝试，从而减少对验证器的调用次数。

技术框架：整体架构包括数据输入、LLM生成不变式、排序器优化和结果输出四个主要模块。首先，输入程序代码，然后通过LLM生成多个候选不变式，接着使用排序器对这些候选进行重排序，最后输出排名最高的正确不变式。

关键创新：最重要的技术创新在于设计了一个对比排序器，该排序器能够基于问题定义有效区分正确与错误的不变式。这一方法与现有的单纯依赖LLM生成的方式有本质区别。

关键设计：排序器的优化采用对比学习方法，损失函数设计为能够有效评估候选不变式的正确性。网络结构方面，排序器使用了深度学习模型，能够处理复杂的输入特征并进行有效的排序。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，重排序机制显著提高了正确不变式的排名，减少了对验证器的调用次数，提升幅度达到XX%（具体数据未知）。与基线方法相比，新的排序方法在生成候选不变式的准确性和效率上均有显著改善。

🎯 应用场景

该研究的潜在应用领域包括程序验证、自动化测试和软件开发等。通过提高循环不变式生成的效率，可以显著降低程序验证的时间成本，提升软件开发的整体效率。未来，该方法有望在更广泛的程序分析和验证任务中得到应用，推动自动化程序验证技术的发展。

📄 摘要（原文）

Synthesizing inductive loop invariants is fundamental to automating program verification. In this work, we observe that Large Language Models (such as gpt-3.5 or gpt-4) are capable of synthesizing loop invariants for a class of programs in a 0-shot setting, yet require several samples to generate the correct invariants. This can lead to a large number of calls to a program verifier to establish an invariant. To address this issue, we propose a {\it re-ranking} approach for the generated results of LLMs. We have designed a ranker that can distinguish between correct inductive invariants and incorrect attempts based on the problem definition. The ranker is optimized as a contrastive ranker. Experimental results demonstrate that this re-ranking mechanism significantly improves the ranking of correct invariants among the generated candidates, leading to a notable reduction in the number of calls to a verifier. The source code and the experimental data for this paper are available in \url{https://github.com/microsoft/NeuralInvariantRanker}.