AI 中文总结
该研究提出集成LLM与ICE框架的增量式学习框架LimICE，用于循环不变式综合，在367个线性、50个非线性基准上的实验显示其解决实例更多、运行速度更快，性能优于相关基线。
AI 中文摘要
循环不变式综合是程序验证中的基础问题，但其固有的不可判定性使其极具挑战性。近期研究越来越多地采用各类机器学习技术生成循环不变式，但多数此类方法采用整体式方法，由于无法严格约束学习过程，基于学习的方法在处理复杂问题时难以同时考虑所有必要条件并生成完整不变式。实际上，循环不变式通常是引理的有序序列，而非单个不变式公式，这促使我们提出增量式ICE（Incremental ICE）——一种用于增量式综合的新型学习框架。该框架将IC3的增量理念融入通用不变式学习框架ICE，通过定义引理特定的学习目标并引入反例过滤机制，实现可靠的增量式学习。在该框架下，我们实例化了循环不变式综合工具LimICE，其利用LLM生成引理的有序序列，并采用ICE-DT作为回退机制补充引理序列。在367个线性基准和50个非线性基准上的实验验证了所提方法的有效性：LimICE在平均15.2秒内解决了367个线性问题中的349个，在平均8.8秒内解决了50个非线性问题中的47个；与最先进的基于LLM的基线相比，该方法在线性和非线性基准上多解决12-24%的实例，同时运行速度快36-63%；LimICE还持续优于强大的非LLM基线，在线性和非线性基准上分别至少多解决86和27个实例。
英文摘要
Loop invariant synthesis is a fundamental problem in program verification, yet the inherent undecidability makes it highly challenging. Recent studies have increasingly employed various machine learning techniques to generate loop invariants. However, most of these methods adopt a monolithic approach. Due to the inability to strictly constrain the learning process, learning-based methods struggle to simultaneously consider all necessary conditions and generate complete invariants when tackling complex problems. In fact, a loop invariant is often an ordered sequence of lemmas, rather than a single invariant formula. This motivates us to propose Incremental ICE, a novel learning framework for incremental synthesis. Our framework integrates the incremental philosophy of IC3 into the general invariant learning framework ICE. By defining a lemma-specific learning objective and introducing a counterexample filtering mechanism, we can achieve sound incremental learning. Under this framework, we instantiate a loop invariant synthesis tool, LimICE, which leverages LLMs to generate the ordered sequence of lemmas and incorporates ICE-DT as a fallback mechanism to complement the lemma sequence. Experiments on 367 linear benchmarks and 50 nonlinear benchmarks demonstrate the effectiveness of the proposed approach. LimICE solves 349 (out of 367) linear problems on an average of 15.2 seconds and 47 (out of 50) nonlinear problems on an average of 8.8 seconds. Compared to the state-of-the-art LLM-based baseline, our approach solves 12-24% more instances while running 36-63% faster across linear and nonlinear benchmarks. LimICE also consistently outperforms strong non-LLM baselines and solves at least 86 and 27 additional instances on the linear and nonlinear benchmarks, respectively.
Comments21 pages, 2 figures
