ChatGPT能否支持软件验证？

大型语言模型在代码生成、调试与修复等软件工程任务中已变得日益有效。诸如ChatGPT之类的语言模型不仅能生成代码，还能解释其内部运行机制，尤其是其正确性。这引发了一个问题：我们能否利用ChatGPT来支持形式化软件验证？本文在回答该问题上迈出了一些初步步伐。更具体地，我们探究ChatGPT能否生成循环不变式。循环不变式生成是软件验证中的核心任务，而生成有效且有用的不变式很可能有助于形式化验证器。为对该假设提供一些初步证据，我们让ChatGPT为106个C程序标注循环不变式。我们通过将这些生成的不变式传递给两个验证器Frama-C和CPAchecker，来检验其有效性与有用性。我们的评估表明，ChatGPT能够生成有效且有用的不变式，使Frama-C得以验证其此前无法解决的任务。基于我们的初步见解，我们提出了将ChatGPT（或广义上的大型语言模型）与软件验证器相结合的方法，并讨论了当前的局限性与开放问题。