Can ChatGPT support software verification?

📄 arXiv: 2311.02433v2 📥 PDF

作者: Christian Janßen, Cedric Richter, Heike Wehrheim

分类: cs.SE, cs.AI, cs.FL, cs.LG, cs.LO

发布日期: 2023-11-04 (更新: 2025-10-14)

备注: accepted at Fundamental Approaches to Software Engineering 2024

💡 一句话要点

利用ChatGPT生成循环不变式以支持软件验证

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

关键词: 软件验证 循环不变式 大型语言模型 ChatGPT 形式验证 代码分析 自动化验证

📋 核心要点

  1. 现有的软件验证方法在生成循环不变式方面存在挑战，导致验证效率低下。
  2. 本文提出利用ChatGPT生成循环不变式，旨在提高软件验证的有效性和效率。
  3. 实验结果表明，ChatGPT生成的不变式有效且有用，显著提升了Frama-C的验证能力。

📝 摘要（中文）

大型语言模型在软件工程任务中变得越来越有效，例如代码生成、调试和修复。像ChatGPT这样的语言模型不仅能够生成代码，还能解释其内部工作原理，尤其是其正确性。这引发了一个问题：我们能否利用ChatGPT来支持形式软件验证。本文首次探讨了这一问题，具体研究了ChatGPT是否能够生成循环不变式。循环不变式生成是软件验证中的核心任务，生成有效且有用的不变式可能会帮助形式验证器。我们要求ChatGPT为106个C程序注释循环不变式，并通过Frama-C和CPAchecker两个验证器检查生成的不变式的有效性和有用性。我们的评估显示，ChatGPT能够生成有效且有用的不变式，使Frama-C能够验证之前无法解决的任务。基于我们的初步见解，我们提出了将ChatGPT（或大型语言模型）与软件验证器结合的方法，并讨论了当前的局限性和未解问题。

🔬 方法详解

问题定义：本文旨在解决如何有效生成循环不变式的问题。现有方法在这一领域的表现不尽如人意，导致软件验证的效率和准确性受到影响。

核心思路：论文的核心思路是利用ChatGPT的语言生成能力来生成循环不变式，认为这种方法能够提高生成的不变式的有效性和实用性。

技术框架：研究流程包括：首先选择106个C程序，然后使用ChatGPT为这些程序生成循环不变式，最后通过Frama-C和CPAchecker验证生成的不变式的有效性和实用性。

关键创新：最重要的技术创新在于将大型语言模型应用于软件验证领域，尤其是循环不变式的生成，这与传统的手动生成方法形成鲜明对比。

关键设计：在实验中，ChatGPT的生成结果被系统地评估，验证器的选择（Frama-C和CPAchecker）也经过精心设计，以确保结果的可靠性和有效性。实验中对生成的不变式进行了有效性和实用性的双重检验。

🖼️ 关键图片

img_0

📊 实验亮点

实验结果显示，ChatGPT能够生成有效且有用的循环不变式，使得Frama-C能够成功验证之前无法解决的任务，验证成功率显著提升，展示了大型语言模型在软件验证中的应用潜力。

🎯 应用场景

该研究的潜在应用领域包括软件验证工具的开发和改进，尤其是在自动化验证和代码分析方面。通过结合大型语言模型与传统验证方法，可以显著提高软件的可靠性和安全性，推动软件工程领域的进步。

📄 摘要（原文）

Large language models have become increasingly effective in software engineering tasks such as code generation, debugging and repair. Language models like ChatGPT can not only generate code, but also explain its inner workings and in particular its correctness. This raises the question whether we can utilize ChatGPT to support formal software verification. In this paper, we take some first steps towards answering this question. More specifically, we investigate whether ChatGPT can generate loop invariants. Loop invariant generation is a core task in software verification, and the generation of valid and useful invariants would likely help formal verifiers. To provide some first evidence on this hypothesis, we ask ChatGPT to annotate 106 C programs with loop invariants. We check validity and usefulness of the generated invariants by passing them to two verifiers, Frama-C and CPAchecker. Our evaluation shows that ChatGPT is able to produce valid and useful invariants allowing Frama-C to verify tasks that it could not solve before. Based on our initial insights, we propose ways of combining ChatGPT (or large language models in general) and software verifiers, and discuss current limitations and open issues.