Loop invariants are fundamental to reasoning about programs with loops. They establish properties about a given loop's behavior. When they additionally are inductive, they become useful for the task of formal verification that seeks to establish strong mathematical guarantees about program's runtime behavior. The inductiveness ensures that the invariants can be checked locally without consulting the entire program, thus are indispensable artifacts in a formal proof of correctness. Finding inductive loop invariants is an undecidable problem, and despite a long history of research towards practical solutions, it remains far from a solved problem. This paper investigates the capabilities of the Large Language Models (LLMs) in offering a new solution towards this old, yet important problem. To that end, we first curate a dataset of verification problems on programs with loops. Next, we design a prompt for exploiting LLMs, obtaining inductive loop invariants, that are checked for correctness using sound symbolic tools. Finally, we explore the effectiveness of using an efficient combination of a symbolic tool and an LLM on our dataset and compare it against a purely symbolic baseline. Our results demonstrate that LLMs can help improve the state-of-the-art in automated program verification.

翻译：循环不变量是推理带循环程序的基础，它们建立了关于给定循环行为的关键性质。当这些不变量同时具有归纳性时，它们在形式验证中变得尤为有用——形式验证旨在为程序的运行时行为建立强大的数学保证。归纳性确保不变量可以局部验证，而无需检查整个程序，因此是形式正确性证明中不可或缺的要素。寻找归纳循环不变量是一个不可判定问题，尽管针对实用解决方案已有长期研究历史，但至今仍未得到完全解决。本文探讨了大型语言模型（LLMs）为这一古老且重要问题提供新解决方案的能力。为此，我们首先整理了一个关于带循环程序的验证问题数据集。接着，我们设计了一种利用LLMs的提示方法，以获得经符号工具验证正确的归纳循环不变量。最后，我们探索了在数据集上高效结合符号工具与LLM的有效性，并与纯符号基准方法进行对比。研究结果表明，LLMs有助于提升自动程序验证的技术水平。