The demonstrated code-understanding capability of LLMs raises the question of whether they can be used for automated program verification, a task that 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.

翻译：大语言模型在代码理解方面的能力引发了这样的问题：它们能否被用于自动化程序验证？这项任务需要对程序属性进行高级抽象推理，这对验证工具而言极具挑战性。我们提出了一种通用方法论，将大语言模型与自动化推理器的能力相结合，用于自动化程序验证。我们从形式上将该方法论描述为一组推导规则，并证明了其可靠性。我们将该演算实例化为一套可靠的自动化验证流程，这在一组合成基准和竞赛基准上带来了实际的性能提升。