循环不变式生成:面向推理优化大语言模型与 SMT 求解器的混合框架
计算机科学中的逻辑
2025-08-04 v1 机器学习
编程语言
摘要
循环不变式对于证明含循环程序的正确性至关重要。循环不变式的开发具有挑战性,且对任意程序都无法保证完全自动化的合成。已有研究提出使用符号技术以及近期兴起的神经方法来合成循环不变式,但这些方法仅能在标准基准的子集上正确合成循环不变式。在本工作中,我们探究现代的、面向推理优化的大语言模型能否取得更好的效果。我们将 OpenAI 的 O1、O1-mini 和 O3-mini 与 Z3 SMT 求解器集成到一个紧耦合的生成-检查流水线中,利用求解器返回的反例迭代地指导不变式精化。我们使用 Code2Inv 基准,该基准提供 C 程序及其形式化的前置条件和后置条件。在该基准的 133 个任务上,我们的框架达到了 100% 的覆盖率(133/133),优于此前最佳的 107/133,且每个实例仅需 1-2 次模型提议,墙钟时间为 14-55 秒。这些结果表明,大语言模型具备潜在的逻辑推理能力,可用于自动化循环不变式合成。尽管我们的实验针对 C 语言程序,但该方法应可推广到其他命令式语言。
引用
@article{arxiv.2508.00419,
title = {Loop Invariant Generation: A Hybrid Framework of Reasoning optimised LLMs and SMT Solvers},
author = {Varun Bharti and Shashwat Jha and Dhruv Kumar and Pankaj Jalote},
journal= {arXiv preprint arXiv:2508.00419},
year = {2025}
}
备注
Under Review