An Empirical Study of LLM-Generated Specifications for VeriFast

📄 arXiv: 2606.26490v1 📥 PDF

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

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

发布日期: 2026-06-25

💡 一句话要点

评估LLM生成的规范以优化VeriFast的静态验证

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

关键词: 静态验证 大型语言模型 分离逻辑 软件工程 自动化验证 规范生成 功能行为 领域知识

📋 核心要点

  1. 现有的静态验证工具在编写规范时需要大量人力，尤其是分离逻辑验证器在处理堆结构时的复杂性。
  2. 本文通过评估LLMs在生成VeriFast验证规范时的表现，提出了多种提示方法和输入类型的组合。
  3. 实验结果表明，LLMs在功能行为保留上表现良好，但验证成功率较低，且大部分错误源于领域知识的不足。

📝 摘要（中文）

静态验证工具能够确保工业规模软件的可靠性，但编写规范需要大量人力，尤其是基于分离逻辑的验证器。本文评估了大型语言模型（LLMs）在生成用于验证303个C函数的规范时的表现，探索了八种提示方法、十种LLM和三种输入类型。结果显示，LLMs在源代码和规范中保留了91%以上的功能行为，但验证成功率仅为31.4%。使用Gemini 2.5 Pro和提供正式合约可提高成功率。大多数错误源于LLMs在领域特定知识上的不足，这为优化LLM生成的规范提供了指导。

🔬 方法详解

问题定义：本文旨在解决静态验证工具在编写规范时所需的人力成本，尤其是针对分离逻辑验证器的复杂性。现有方法在生成规范时缺乏有效的自动化支持，导致验证效率低下。

核心思路：论文提出利用大型语言模型（LLMs）生成验证规范，通过多种提示方法和输入类型的组合，评估其在静态验证中的有效性和准确性。

技术框架：研究分为两个阶段，首先探索不同的提示方法和输入类型，然后对生成的代码和规范进行定量和定性分析。主要模块包括LLM选择、提示设计和结果评估。

关键创新：最重要的创新在于将LLMs应用于分离逻辑验证器的规范生成，填补了以往研究中对SL验证器的关注不足。

关键设计：实验中使用了十种不同的LLM，采用了八种提示策略，并结合正式合约来提高生成规范的成功率。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果显示，LLMs在功能行为保留方面超过91%，但验证成功率仅为31.4%。使用Gemini 2.5 Pro和提供正式合约显著提高了成功率，表明领域特定知识的准确性对验证结果至关重要。

🎯 应用场景

该研究的潜在应用领域包括软件工程、自动化验证和人工智能辅助开发。通过优化LLM生成的规范，可以显著降低软件开发中的人力成本，提高静态验证工具的效率和准确性，推动软件质量的提升。

📄 摘要（原文）

Static verification tools can assure industrial scale software, but require significant human labor to write specifications. This is particularly true of static verifiers based on separation logic (SL verifiers), which excel at verifying heapmanipulating programs, but require many complex auxiliary specifications to reason about heap structure. Recent work applies large language models (LLMs) to generate code, tests, and proofs, including specifications for verifiers, but mostly targeting non-SL verifiers. To address this gap, this paper thoroughly evaluates how well LLMs perform when prompted to generate specifications for verifying 303 C functions with the SL verifier VeriFast. We explored eight prompting approaches, ten LLMs, and three input types in two stages. Quantitative and qualitative analyses are used to assess the LLM-generated code and specifications for functional behavior, verifiability and errors. The results show that LLMs preserve functional behavior in source code and specifications (both over 91%), but achieve modest verification success (31.4%). Using Gemini 2.5 Pro and providing formal contracts lead to higher success rates in our setting. Moreover, most errors (94%) come from LLMs' mistakes in the domainspecific knowledge of SL verifiers such as VeriFast. These findings provide guidance for optimizing LLM-generated specifications for SL verifiers.