[2606.26490] 面向VeriFast的LLM生成规约的实证研究
[2606.26490] 面向VeriFast的LLM生成规约的实证研究
作者： 樊文、Minh Tran、Sanya Dod、胡鑫、Marilyn Rego、谢丹宁、Jenna DiVincenzo、林谭
摘要： 静态验证工具能够保障工业级软件的可靠性，但需要大量人力编写规约。基于分离逻辑的静态验证器（SL验证器）尤其如此，它们在验证堆操作程序方面表现出色，但需要大量复杂的辅助规约来推理堆结构。近期研究尝试将大语言模型（LLM）应用于生成代码、测试和证明（包括验证器规约），但多数针对非SL验证器。为填补这一空白，本文全面评估了LLM在提示生成SL验证器VeriFast所需的规约以验证303个C函数时的表现。我们分两个阶段探索了八种提示方法、十个LLM以及三种输入类型。通过定量和定性分析，评估了LLM生成的代码与规约在功能性行为、可验证性和错误方面的表现。结果表明：LLM在源代码和规约中均保持了较高的功能性行为（均超过91%），但验证成功率中等（31.4%）。在我们设定的场景中，使用Gemini 2.5 Pro并提供形式化契约可带来更高的成功率。此外，绝大多数错误（94%）源于LLM在VeriFast等SL验证器领域知识上的失误。这些发现为优化SL验证器的LLM生成规约提供了指导。
学科分类： 软件工程（cs.SE）；人工智能（cs.AI）；计算机科学逻辑（cs.LO）；编程语言（cs.PL）
引用方式： arXiv:2606.26490 [cs.SE]