arXivDaily arXiv每日学术速递 周一至周五更新
北美退伍军人节（Veterans Day），12 日无更新
arXiv 2311.02433cs.SEcs.AIcs.FLcs.LGcs.LO
收藏

ChatGPT能否支持软件验证？

Can ChatGPT support software verification?

Carl-von-Ossietzky Universität Oldenburg（奥尔登堡卡尔·冯·奥西特齐大学）

Christian Janßen, Cedric Richter, Heike Wehrheim

备注：
accepted at Fundamental Approaches to Software Engineering 2024
阅读 PDF
arXiv 页面 ↗HTML 原文 ↗

AI总结：

本研究探索ChatGPT能否生成循环不变量以支持软件验证，实验表明其生成的不变量有效且有用，能增强Frama-C的验证能力，并提出结合大语言模型与验证器的方向。

摘要：

大型语言模型在软件工程任务中变得越来越有效，例如代码生成、调试和修复。像ChatGPT这样的语言模型不仅能生成代码，还能解释其内部工作原理，特别是其正确性。这引发了一个问题：我们能否利用ChatGPT来支持正式的软件验证？在本文中，我们朝回答这个问题迈出了初步步伐。更具体地说，我们调查ChatGPT能否生成循环不变量。循环不变量生成是软件验证中的核心任务，生成有效且有用的不变量很可能有助于形式验证器。为了对这一假设提供初步证据，我们要求ChatGPT为106个C程序标注循环不变量。我们通过将生成的不变量传递给两个验证器Frama-C和CPAchecker来检查其有效性和有用性。我们的评估表明，ChatGPT能够生成有效且有用的不变量，使Frama-C能够验证之前无法解决的任务。基于我们的初步见解，我们提出了将ChatGPT（或一般的大型语言模型）与软件验证器相结合的方法，并讨论了当前的局限性和未解决的问题。

英文摘要：

Large language models have become increasingly effective in software engineering tasks such as code generation, debugging and repair. Language models like ChatGPT can not only generate code, but also explain its inner workings and in particular its correctness. This raises the question whether we can utilize ChatGPT to support formal software verification. In this paper, we take some first steps towards answering this question. More specifically, we investigate whether ChatGPT can generate loop invariants. Loop invariant generation is a core task in software verification, and the generation of valid and useful invariants would likely help formal verifiers. To provide some first evidence on this hypothesis, we ask ChatGPT to annotate 106 C programs with loop invariants. We check validity and usefulness of the generated invariants by passing them to two verifiers, Frama-C and CPAchecker. Our evaluation shows that ChatGPT is able to produce valid and useful invariants allowing Frama-C to verify tasks that it could not solve before. Based on our initial insights, we propose ways of combining ChatGPT (or large language models in general) and software verifiers, and discuss current limitations and open issues.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

↑