解决多循环程序的不变式自动生成难题，提升代码验证准确性。
InvWeaver: Deductive Feedback for Invariant Synthesis in Interacting-Loop Programs
- 通过抽象与证明义务传播，揭示多循环间的依赖关系。
- 在82个测试用例中解决72个复杂多循环问题，表现远超现有方法。
- 适合关注程序验证、自动推理的开发者和研究人员。
循环不变式推断是程序验证中的核心挑战。尽管基于大模型的猜-验方法在单循环程序上表现良好，但在存在多个交互循环的程序中常失效。本文提出InvWeaver，一种神经符号框架，用于合成此类程序的不变式。核心思想是暴露循环间依赖，并结合循环层抽象、义务引导推理与最弱前置条件驱动的精化，实现证明义务的传递。我们在一个全面的基准测试集上评估了InvWeaver，包括从经典算法中整理的新数据集。实验结果表明，InvWeaver显著优于现有不变式推断方法，在82个多循环基准问题中成功解决72个，同时在单循环任务上也保持优异性能。
原文摘要 · Abstract (English)
Loop invariant inference is a fundamental yet challenging problem in program verification. Recent LLM-aided guess-and-check techniques have shown strong performance on single-loop programs, but they often struggle with programs containing multiple interacting loops. This paper presents InvWeaver, a neuro-symbolic framework for synthesizing invariants for such programs. The key idea is to expose inter-loop dependencies and propagate proof obligations through a combination of loop-level abstraction, obligation-guided inference, and weakest-precondition-based refinement. We evaluate InvWeaver on a comprehensive benchmark suite, including a newly curated dataset derived from classic algorithms. Experimental results show that InvWeaver substantially outperforms existing invariant inference methods, solving 72 out of 82 multi-loop benchmark problems and maintaining strong performance on single-loop tasks.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。