LLM 为 VeriFast 生成规格说明的实证研究
软件工程
2026-06-25 v1 人工智能
计算机科学中的逻辑
编程语言
摘要
静态验证工具可保障工业级软件，但编写规格说明需要大量人力。基于分离逻辑的静态验证器（SL 验证器）尤为如此，它们擅长验证操纵堆的程序，却需要许多复杂的辅助规格说明来推理堆结构。近期工作应用大语言模型（LLMs）生成代码、测试和证明，包括为验证器生成规格说明，但大多面向非 SL 验证器。为弥补这一空白，本文全面评估了当被提示为使用 SL 验证器 VeriFast 验证 303 个 C 函数而生成规格说明时，LLM 的表现如何。我们探索了八个提示方法、十个 LLM 和三类输入，分两个阶段进行。采用定量与定性分析评估 LLM 生成的代码和规格说明在功能行为、可验证性和错误方面的情况。结果显示，LLM 在源代码和规格说明中保留了功能行为（均超 91%），但仅取得 modest 的验证成功率（31.4%）。在我们的设定中，使用 Gemini 2.5 Pro 并提供形式化契约带来了更高的成功率。此外，大多数错误（94%）源于 LLM 在 VeriFast 等 SL 验证器领域特定知识上的失误。这些发现为优化 SL 验证器的 LLM 生成规格说明提供了指导。
引用
@article{arxiv.2606.26490,
title = {An Empirical Study of LLM-Generated Specifications for VeriFast},
author = {Wen Fan and Minh Tran and Sanya Dod and Xin Hu and Marilyn Rego and Danning Xie and Jenna DiVincenzo and Lin Tan},
journal= {arXiv preprint arXiv:2606.26490},
year = {2026}
}