Loop invariants, essential for program verification, are challenging to auto-generate especially for programs incorporating complex memory manipulations. Existing approaches for generating loop invariants rely on fixed sets or templates, hampering adaptability to real-world programs. Recent efforts have explored machine learning for loop invariant generation, but the lack of labeled data and the need for efficient generation are still troublesome. We consider the advent of the large language model (LLM) presents a promising solution, which can analyze the separation logic assertions after symbolic execution to infer loop invariants. To overcome the data scarcity issue, we propose a self-supervised learning paradigm to fine-tune LLM, using the split-and-reassembly of predicates to create an auxiliary task and generate rich synthetic data for offline training. Meanwhile, the proposed interactive system between LLM and traditional verification tools provides an efficient online querying process for unseen programs. Our framework can readily extend to new data structures or multi-loop programs since our framework only needs the definitions of different separation logic predicates, aiming to bridge the gap between existing capabilities and requirements of loop invariant generation in practical scenarios. Experiments across diverse memory-manipulated programs have demonstrated the performance of our proposed method compared to the baselines with respect to efficiency and effectiveness.

翻译：循环不变量是程序验证的关键要素，但在处理包含复杂内存操作的程序时，其自动生成仍面临挑战。现有循环不变量生成方法依赖固定集合或模板，难以适应真实世界程序。近年来虽有研究尝试利用机器学习生成循环不变量，但标注数据匮乏及生成效率问题仍未解决。大语言模型（LLM）的出现提供了一种可行方案——通过分析符号执行后的分离逻辑断言来推断循环不变量。为克服数据稀缺问题，我们提出基于自监督学习的LLM微调范式：通过谓词的分割重组构建辅助任务，离线生成海量合成训练数据。同时，我们设计的LLM与传统验证工具交互系统，能对未见程序实现高效在线查询。由于本框架仅需定义不同分离逻辑谓词，可便捷扩展至新型数据结构或多循环程序，旨在弥合实际场景中循环不变量生成现有能力与需求之间的鸿沟。在多样化的内存操作程序上的实验结果表明，相较基线方法，本方法在效率与有效性方面均具优势。