评估大型语言模型在VeriFast中生成可验证规约的能力
软件工程
2025-01-06 v3 人工智能
计算机科学中的逻辑
编程语言
摘要
静态验证是提升软件质量的强大方法，但需要大量人力和资源。这对于使用所有权逻辑推理堆操作程序的静态验证器而言尤其如此。LLMs已在多项软件工程活动中展现出潜力，包括代码生成、测试生成、定理证明器的证明生成以及静态验证器的规约生成。然而，此前研究尚未探索LLMs在基于所有权逻辑（如分离逻辑）的规约生成方面表现如何。为填补这一空白，本文探讨了OpenAI的GPT-4o模型在为VeriFast（一种基于分离逻辑的静态验证器）生成C程序规约方面的有效性。我们的实验采用三种不同类型的用户输入以及基础提示和思维链（Chain-of-Thought）提示来评估GPT的能力。我们的结果表明，GPT-4o生成的规约保留了功能行为，但难以通过验证。当规约可通过验证时，它们包含冗余内容。讨论了未来改进性能的方向。
引用
@article{arxiv.2411.02318,
title = {Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast},
author = {Wen Fan and Marilyn Rego and Xin Hu and Sanya Dod and Zhaorui Ni and Danning Xie and Jenna DiVincenzo and Lin Tan},
journal= {arXiv preprint arXiv:2411.02318},
year = {2025}
}