VerIbmc：结合本地LLM与符号推理的软件验证

循环不变量合成仍然是形式软件验证的中心和关键瓶颈。最近基于 LLM 的神经符号工具已经取得了令人印象深刻的解决率。然而，这些工具依赖于专有且通常昂贵的云 API，这对隐私敏感的工业部署构成了障碍，因为源代码无法离开组织或成本是一个因素。我们提出了 VerIbmc，一种神经符号管道，它将符号不变量生成与本地可部署的开放权重语言模型与 ESBMC 验证工具配对。我们的管道将确定性符号不变量合成阶段与由结构化验证器反馈驱动的迭代 LLM 细化循环相结合。此外，我们提供了两种提示策略不同的管道：思想链与思想树。我们对五个开放权重模型（参数范围从 7B 到 120B 不等）进行了广泛的实验评估，涉及五个基准系列，包含 520 个问题（排除 21 个不可避免的溢出问题后为 499 个）。总体而言，最佳单一配置 (GPT-OSS-120B) 解决了 499 个问题中的 431 个问题 (86.4%)。此外，在与最强大的云 API 工具共享的四个基准测试套件中，VerIbmc 仅在单个本地计算机上运行具有竞争力。评估显示，符号不变量合成无需任何 LLM 调用即可解决 75 个问题，并为最弱的模型产生多达 35 个额外问题。重要的是，所有推理完全在使用开放权重模型的单个本地计算机上运行——不需要云 API 或专有模型。总的来说，我们证明了基于 LLM 的神经符号方法可以以保护隐私和节能的方式有效地用于不变量合成，而不必求助于锁定在 API 后面的昂贵的专有前沿模型。