一句话：提出“查询-过滤-重组”策略，用 LLM 生成候选循环不变式、以有界模型检测筛选谓词并组装，再由 SMT 求解器校验。
循环不变式推断是程序验证中的关键环节，但由于不可判定性和复杂循环行为，实践中仍很困难。现有机器学习方法虽能自动生成不变式，却依赖标注训练数据，且具有随机性和不确定性，导致性能不稳定。本文探索大语言模型（LLM）与有界模型检测（BMC）的协同，核心观察是 LLM 单次响应可能给不出完整正确的不变式，但多次响应往往能提供正确不变式所需的各个谓词。为此，作者提出“查询-过滤-重组”策略：先用 LLM 生成一组候选不变式，无需训练数据；再用 BMC 从中识别有效谓词，组装成新的候选不变式并用现成 SMT 求解器检查；检查反馈会加入下一轮提示中。作者将原有 133 个程序的基准扩展到 316 个程序进行更全面测试。实验表明该方法显著优于现有最优技术，在 316 个用例中成功生成 309 个循环不变式，而基线方法最多只能处理 219 个程序。
Loop invariant inference, a key component in program verification, is a challenging task due to the inherent undecidability and complex loop behaviors in practice. Recently, machine learning based techniques have demonstrated impressive performance in generating loop invariants automatically. However, these methods highly rely on the labeled training data, and are intrinsically random and uncertain, leading to unstable performance. In this paper, we investigate a synergy of large language models (LLMs) and bounded model checking (BMC) to address these issues. The key observation is that, although LLMs may not be able to return the correct loop invariant in one response, they usually can provide all individual predicates of the correct loop invariant in multiple responses. To this end, we propose a "query-filter-reassemble" strategy, namely, we first leverage the language generation power of LLMs to produce a set of candidate invariants, where training data is not needed. Then, we employ BMC to identify valid predicates from these candidate invariants, which are assembled to produce new candidate invariants and checked by off-the-shelf SMT solvers. The feedback is incorporated into the prompt for the next round of LLM querying. We expand the existing benchmark of 133 programs to 316 programs, providing a more comprehensive testing ground. Experimental results demonstrate that our approach significantly outperforms the state-of-the-art techniques, successfully generating 309 loop invariants out of 316 cases, whereas the existing baseline methods are only able to tackle 219 programs at best. The code is publicly available at https://github.com/SoftWiser-group/LaM4Inv.git.CCS CONCEPTS•Software and its engineering → Formal software verification.
@inproceedings{WuC0W0M24,
title = {LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant Inference},
author = {Guangyuan Wu and Weining Cao and Yuan Yao and Hengfeng Wei and Taolue Chen and Xiaoxing Ma},
booktitle = {ASE},
year = {2024},
doi = {10.1145/3691620.3695014}
}