InvWeaver: 交互循环程序中不变式合成的演绎反馈

arXiv cs.LG 论文
loop-invariant program-verification neuro-symbolic llm-aided invariant-synthesis

摘要

InvWeaver 是一个神经符号框架，利用大语言模型和演绎反馈来合成具有多个交互循环程序的循环不变式，在基准测试中优于现有方法。

arXiv:2607.05478v1 公告类型：新提交 摘要：循环不变式推断是程序验证中一个基本但具有挑战性的问题。近期借助大语言模型的猜测与检查技术在单循环程序上表现出色，但往往难以处理包含多个交互循环的程序。本文提出 InvWeaver，一个用于合成此类程序不变式的神经符号框架。其核心思想是通过结合循环级抽象、义务引导推理和基于最弱前置条件的细化，来暴露循环间依赖关系并传播证明义务。我们在一个全面的基准测试套件上评估了 InvWeaver，其中包括一个新近整理的源自经典算法的数据集。实验结果表明，InvWeaver 显著优于现有的不变式推断方法，在 82 个多循环基准问题中解决了 72 个，并在单循环任务上保持了强劲性能。
查看原文
查看缓存全文

缓存时间: 2026/07/08 04:43 

# InvWeaver: 交互循环程序中不变式合成的演绎反馈
来源: https://arxiv.org/abs/2607.05478
查看PDF (https://arxiv.org/pdf/2607.05478)

> 摘要: 循环不变式推断是程序验证中一个基础而具有挑战性的问题。近年来，基于LLM的猜测与检查技术在单循环程序上表现出色，但在处理包含多个交互循环的程序时往往遇到困难。本文提出了InvWeaver，一个用于合成此类程序不变式的神经符号框架。其核心思想是通过循环级抽象、义务引导推断和基于最弱前置条件的改进相结合，暴露循环间依赖关系并传播证明义务。我们在一套全面的基准测试套件上评估了InvWeaver，其中包括一个新近从经典算法中精选的数据集。实验结果表明，InvWeaver显著优于现有的不变式推断方法，解决了82个多循环基准问题中的72个，同时在单循环任务上保持了强劲性能。

## 提交历史

来自: Guangyuan Wu \[查看电子邮件 (https://arxiv.org/show-email/51479f36/2607.05478)\] **\[v1\]** Mon, 6 Jul 2026 14:36:36 UTC (174 KB)

相似文章