测试大模型生成可验证的程序规格能力，发现能保功能但难通过验证。
Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast
- 用GPT-4o生成基于分离逻辑的C程序规格
- 生成规格多数保功能但无法通过VeriFast验证
- 适合研究大模型在形式化验证中的应用
静态验证能有效提升软件质量，但需大量人力与资源，尤其针对使用所有权逻辑分析堆内存操作程序的验证器。大语言模型在代码生成、测试生成、定理证明和规格生成等软件工程任务中已显潜力。然而，此前研究未探讨大模型在基于所有权逻辑（如分离逻辑）的规格生成上的表现。本文评估OpenAI GPT-4o在生成可被VeriFast验证的C程序规格方面的有效性。实验采用三种用户输入类型及基础提示与思维链（CoT）提示策略。结果表明，GPT-4o生成的规格能保持程序功能，但难以通过验证；当能通过验证时，规格常含冗余内容。未来方向包括改进模型生成质量。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。