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 transition rules and prove its soundness. We instantiate the calculus as a sound automated verification procedure and demonstrate practical improvements on a set of synthetic and competition benchmarks.

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