Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast

📄 arXiv: 2411.02318v3 📥 PDF

作者: Wen Fan, Marilyn Rego, Xin Hu, Sanya Dod, Zhaorui Ni, Danning Xie, Jenna DiVincenzo, Lin Tan

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

发布日期: 2024-11-04 (更新: 2025-01-03)

💡 一句话要点

评估大型语言模型在VeriFast中生成可验证规范的能力

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

关键词: 大型语言模型 静态验证 VeriFast 分离逻辑 规范生成

📋 核心要点

  1. 静态验证依赖大量人力物力，尤其是在处理堆操作和所有权逻辑的程序时，存在效率瓶颈。
  2. 研究利用GPT-4o生成C程序的VeriFast规范，探索LLM在分离逻辑规范生成方面的能力。
  3. 实验结果表明，GPT-4o生成的规范能保持功能行为，但验证性较差，且存在冗余，未来有提升空间。

📝 摘要（中文）

静态验证是提高软件质量的有效方法，但需要大量的人工和资源。对于使用所有权逻辑推理堆操作程序的静态验证器来说尤其如此。大型语言模型（LLM）在代码生成、测试生成、定理证明器的证明生成以及静态验证器的规范生成等软件工程活动中展现出潜力。然而，以往的研究尚未探索LLM在基于所有权逻辑（如分离逻辑）的规范生成方面的表现。为了填补这一空白，本文探讨了OpenAI的GPT-4o模型在生成C程序规范方面的有效性，这些规范可以使用基于分离逻辑的静态验证器VeriFast进行验证。我们的实验采用了三种不同类型的用户输入以及基本提示和思维链（CoT）提示来评估GPT的能力。结果表明，GPT-4o生成的规范保留了功能行为，但难以验证。当规范可验证时，它们包含冗余。讨论了改进性能的未来方向。

🔬 方法详解

问题定义：论文旨在评估大型语言模型（LLM）在为C程序生成可验证的VeriFast规范方面的能力。现有的静态验证方法，特别是那些依赖于分离逻辑等所有权逻辑的验证器，需要大量的人工干预来编写规范，这既耗时又容易出错。因此，自动生成规范可以显著提高静态验证的效率和可扩展性。

核心思路：论文的核心思路是利用大型语言模型（特别是GPT-4o）的强大代码生成和理解能力，自动生成C程序的VeriFast规范。通过不同的提示策略（包括基本提示和思维链提示）以及不同类型的用户输入，来探索LLM生成可验证规范的能力。目标是减少人工编写规范的工作量，并提高静态验证的自动化程度。

技术框架：该研究的技术框架主要包括以下几个步骤：1) 准备C程序作为输入；2) 使用不同的提示策略（基本提示和思维链提示）和用户输入，提示GPT-4o模型生成VeriFast规范；3) 使用VeriFast验证器验证生成的规范；4) 分析验证结果，评估GPT-4o生成的规范的正确性和可验证性。整个流程旨在模拟一个自动化的静态验证流程，其中LLM负责规范生成，而VeriFast负责验证。

关键创新：该研究的关键创新在于探索了大型语言模型在分离逻辑规范生成方面的应用。以往的研究主要集中在LLM在代码生成、测试生成等方面的应用，而较少关注其在静态验证规范生成方面的潜力。该研究首次系统地评估了GPT-4o在生成VeriFast规范方面的能力，并分析了其优缺点。

关键设计：实验中使用了三种不同类型的用户输入，以评估GPT-4o在不同输入条件下的性能。同时，采用了基本提示和思维链（CoT）提示两种策略，以探索不同的提示方式对生成规范质量的影响。没有提及具体的参数设置、损失函数、网络结构等技术细节，可能因为GPT-4o是闭源模型，研究重点在于评估其能力而非修改其内部结构。

📊 实验亮点

实验结果表明，GPT-4o生成的规范能够保留C程序的功能行为，但在可验证性方面表现不佳。即使生成的规范是可验证的，也常常包含冗余信息。这表明LLM在理解分离逻辑和生成精确规范方面仍有提升空间。该研究为未来改进LLM在静态验证规范生成方面的性能提供了方向。

🎯 应用场景

该研究成果可应用于软件开发和静态验证领域，通过LLM自动生成规范，降低静态验证的成本和难度，提高软件质量和可靠性。未来可扩展到更复杂的程序和验证器，实现更智能的自动化验证流程，加速软件开发周期。

📄 摘要（原文）

Static verification is a powerful method for enhancing software quality, but it demands significant human labor and resources. This is particularly true of static verifiers that reason about heap manipulating programs using an ownership logic. LLMs have shown promise in a number of software engineering activities, including code generation, test generation, proof generation for theorem provers, and specification generation for static verifiers. However, prior work has not explored how well LLMs can perform specification generation for specifications based in an ownership logic, such as separation logic. To address this gap, this paper explores OpenAI's GPT-4o model's effectiveness in generating specifications on C programs that are verifiable with VeriFast, a separation logic based static verifier. Our experiment employs three different types of user inputs as well as basic and Chain-of-Thought (CoT) prompting to assess GPT's capabilities. Our results indicate that the specifications generated by GPT-4o preserve functional behavior, but struggle to be verifiable. When the specifications are verifiable they contain redundancies. Future directions are discussed to improve the performance.