用大模型+逻辑求解器自动找循环不变式，准确率100%。
Loop Invariant Generation: A Hybrid Framework of Reasoning optimised LLMs and SMT Solvers
- 大模型生成候选不变式，求解器用反例迭代优化。
- 在133个测试任务中全部成功，远超此前最高107个。
- 适合做程序验证或形式化方法研究的开发者。
循环不变式是证明带循环程序正确性的关键。完全自动合成不变式对任意程序无法保证。已有方法使用符号技术或神经网络，但仅能正确处理标准基准的部分问题。本文探究现代推理优化的大语言模型是否表现更优。我们构建了紧密耦合的生成-验证流水线，将OpenAI的O1、O1-mini和O3-mini与Z3 SMT求解器结合，利用求解器产生的反例迭代引导不变式精炼。实验基于Code2Inv基准，包含133个C语言程序及其前置与后置条件。本框架在所有133个任务上均成功，超越此前最佳的107/133，且每个实例仅需1-2次模型提议，耗时14-55秒。结果表明，大模型具备潜在的逻辑推理能力，可有效支持循环不变式自动化合成。尽管实验针对C语言程序，该方法应可推广至其他命令式语言。
原文摘要 · Abstract (English)
Loop invariants are essential for proving the correctness of programs with loops. Developing loop invariants is challenging, and fully automatic synthesis cannot be guaranteed for arbitrary programs. Some approaches have been proposed to synthesize loop invariants using symbolic techniques and more recently using neural approaches. These approaches are able to correctly synthesize loop invariants only for subsets of standard benchmarks. In this work, we investigate whether modern, reasoning-optimized large language models can do better. We integrate OpenAI's O1, O1-mini, and O3-mini into a tightly coupled generate-and-check pipeline with the Z3 SMT solver, using solver counterexamples to iteratively guide invariant refinement. We use Code2Inv benchmark, which provides C programs along with their formal preconditions and postconditions. On this benchmark of 133 tasks, our framework achieves 100% coverage (133 out of 133), outperforming the previous best of 107 out of 133, while requiring only 1-2 model proposals per instance and 14-55 seconds of wall-clock time. These results demonstrate that LLMs possess latent logical reasoning capabilities which can help automate loop invariant synthesis. While our experiments target C-specific programs, this approach should be generalizable to other imperative languages.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。