LimICE：将 LLM 集成到 ICE 框架中以实现高效的循环不变推理

循环不变综合是程序验证中的一个基本问题，但其固有的不可判定性使其极具挑战性。最近的研究越来越多地采用各种机器学习技术来生成循环不变量。然而，这些方法大多数采用整体方法。由于无法严格约束学习过程，基于学习的方法在解决复杂问题时很难同时考虑所有必要条件并产生完整的不变量。事实上，循环不变量通常是引理的有序序列，而不是单个不变量公式。这促使我们提出增量 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 个附加实例。