The demonstrated code-understanding capability of LLMs raises the question of whether they can be used for automated program verification, a task that typically demands high-level abstract reasoning about program properties that is challenging for verification tools. We propose a general methodology to combine the power of LLMs and automated reasoners for automated program verification. We formally describe this methodology as a set of derivation rules and prove its soundness. We instantiate the calculus as a sound automated verification procedure, which led to practical improvements on a set of synthetic and competition benchmarks.

翻译：语言模型（LLMs）已展现出理解代码的能力，这引发了一个问题：它们是否可用于自动化程序验证？该任务通常需要对程序属性进行高层次抽象推理，而验证工具难以胜任。我们提出了一种通用方法论，将LLMs与自动化推理器的能力相结合，用于自动化程序验证。我们以一组推导规则的形式对方法论进行形式化描述，并证明其可靠性。我们将该演算实例化为一种可靠的自动化验证过程，并在合成基准和竞赛基准上实现了实际性能提升。