💻 computer science

Neuro-Symbolic Software Verification: Hyper-charging Local Language Models with Symbolic Reasoning at Scale

本文介绍了 VerIbmc，这是一个神经符号流水线，它利用本地开源权重语言模型，结合符号不变性合成与迭代验证器反馈，实现了用于软件验证的最先进循环不变式生成，为专有的云端工具提供了一种保护隐私且具有成本效益的替代方案。

原作者： Muhammad A. A. Pirzada, Julian Parsert, Weiqi Wang, Konstantin Korovin, Lucas C. Cordeiro

发布于 2026-06-16

📖 1 分钟阅读☕ 轻松阅读

原作者： Muhammad A. A. Pirzada, Julian Parsert, Weiqi Wang, Konstantin Korovin, Lucas C. Cordeiro

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正试图证明一台复杂的机器（一个计算机程序）永远不会损坏，无论它运行多少次。证明中最困难的部分是理解这台机器的“循环”——即那些重复执行任务的部分。为了证明机器是安全的，你需要找到一个循环不变式（Loop Invariant）。

把循环不变式想象成一条“安全规则”，它在循环的每一次新周期开始时都必须成立。例如，如果一个循环从 10 倒数到 0，那么安全规则可能是：“数字始终在 0 到 10 之间。”如果你能证明这条规则在开始时成立、在每一步之后依然成立，并最终导向一个安全的终点，那么整台机器就被证明是安全的。

问题在于，自动寻找这些规则极其困难。这就像是在没有任何线索的情况下，试图猜出保险箱的密码。

旧方法 vs. 新方法

旧方法（符号推理）：
传统上，计算机尝试使用严格的数学和逻辑来寻找这些规则。这就像一位极其精准的会计在检查每一个数字。它非常可靠，但速度很慢，并且经常在复杂、混乱的问题面前卡壳。这就像是通过逐一检查每一面墙来试图走出迷宫。

“云端”方式（大型 AI 模型）：
最近，人们开始使用大规模的人工智能（AI）模型来猜测这些规则。这些 AI 就像是博学多才的学生，阅读过数百万个代码示例。它们可以非常快速地猜出正确的规则。然而，要使用它们，你通常必须将你的代码发送到巨大的、昂贵的云端服务器（这就像把你的秘密蓝图交给一个陌生人）。对于需要保护代码隐私的公司来说，这既不利于隐私，也耗费大量资金。

解决方案：VerIbmc（本地“超级助手”）

该论文的作者构建了一个名为 VerIbmc 的新系统。你可以把它想象成一个本地工作坊，在这里你可以使用智能 AI 助手，而无需离开你的建筑。

以下是 VerIbmc 的工作原理，我们使用一个简单的类比：

想象你正在尝试解决一个困难的谜题（循环不变式）。

确定性侦探（阶段 0 & 1）： 在请求 AI 帮忙之前，VerIbmc 会先派出一名严谨的逻辑侦探（一个名为 ESBMC 的工具）来观察谜题。侦探会先检查简单的事实。如果谜题很简单，侦探会立即解决它。如果侦探发现了一些坚实的线索（例如“数字始终为正数”），他们会将这些线索写在白板上。
本地 AI 助手（阶段 2）： 如果侦探卡住了，他们就会请出本地 AI 助手。但诀窍在于：AI 并不是从零开始。侦探会将写有已发现线索的白板交给 AI。
反馈循环： AI 猜出一个完整的解法。侦探对其进行检查。
- 如果错了，侦探不会只说“不对”。他们会说：“这一部分是错的，但另一部分实际上是正确的。”他们会提取正确的部分，将其写在白板上，然后要求 AI 再次尝试，并利用新的线索。
- 这个过程会不断重复，直到谜题被解决或时间耗尽。

两种思考方式（CoT vs. ToT）

论文还测试了 AI 在解决谜题时应该如何“思考”：

思维链（Chain-of-Thought, CoT）： AI 以直线方式思考，循序渐进，就像在写一个单一的故事。
思维树（Tree-of-Thoughts, ToT）： AI 像树一样向外分支。它同时尝试几条不同的路径，观察哪些看起来更有希望，然后将精力集中在最好的路径上。论文发现，对于最强的 AI 模型，这种分支方法效果很好；但对于较小、较弱的模型，这种方法有时会浪费时间。

结果：为什么这很重要

研究人员使用五种不同的“开源权重”AI 模型（任何人都可以下载并在自己电脑上运行的模型），在数百个不同的编程谜题上测试了这个系统。

隐私至上： 因为一切都在本地机器上运行，代码永远不会离开组织。这就像是在自己的房间里做数学作业，而不是把作业交给一个陌生人。
成本效益： 你不需要向大型云端公司支付昂贵的费用。
性能表现： 最好的配置（使用名为 GPT-OSS-120B 的大型本地模型）解决了 86.4% 的问题。这优于许多传统的工具，并且足以与昂贵的基于云端的 AI 工具相媲美。
“免费”的提升： 系统发现，“侦探”阶段（符号部分）在完全不需要 AI 介入的情况下就独立解决了 75 个问题。对于较弱的 AI 模型，侦探提供的线索帮助它们比单独使用 AI 时多解决了 35 个问题。

核心结论

VerIbmc 证明了你不需要昂贵且侵犯隐私的云端超级计算机来进行软件安全验证。通过将严谨的逻辑侦探与能够从错误中学习的智能本地 AI 助手相结合，你可以在自己的电脑上获得顶级的性能。这是一种让软件验证变得私密、经济且强大的方式。

技术摘要：基于 VerIbmc 的神经符号软件验证

问题陈述

循环不变式合成仍然是形式化软件验证中的核心瓶颈。虽然存在符号技术（如抽象解释、约束求解）和数据驱动的“猜想与检查”方法，但它们往往在可扩展性、表达能力或处理现实世界代码的多样性方面面临挑战。近期，大语言模型（LLMs）通过利用从代码语料库中学习到的模式，在生成候选不变式方面展现出了潜力。然而，现有的神经符号方法通常依赖于通过外部云端 API 访问的专有闭源模型。这种依赖为工业化部署引入了显著障碍：

隐私与合规性： 源代码必须传输到第三方服务，这引发了机密性担忧。
可复现性： 对外部供应商的依赖使得集成到受控的验证流水线中变得复杂。
成本与可持续性： 大型模型计算成本高昂且能耗巨大，限制了其在持续验证工作流中的实用性。

作者认为，这些挑战迫使研究转向可在组织内部基础设施中完全运行、无需暴露专有代码的、可本地部署的开源权重语言模型。

方法论：VerIbmc 流水线

本文提出了 VerIbmc，这是一个神经符号流水线，旨在通过将符号推理与本地托管的开源权重 LLM 相结合，为 C 程序合成循环不变式。该系统使用 ESBMC（基于 SMT 的高效上下文边界模型检测器）作为验证预言机（Oracle）。该流水线基于“仅在必要时升级”的原则设计，优先进行廉价、确定性的符号推理，然后再调用 LLM。

核心架构

该流水线分为三个阶段运行：

阶段 0（基准验证）： ESBMC 验证未标注的程序。如果程序是平凡安全的或可证明是不安全的，流程立即终止，从而避免不必要的合成工作。
阶段 1（符号候选生成）： 如果阶段 0 返回“未知（Unknown）”，系统通过对循环入口变量和常数进行两两比较，符号化地枚举原子候选不变式。这些原子通过 ESBMC 进行归纳性验证。系统维护三个存储库：可证（ $P$ ）、可证伪（ $D$ ）和未知（ $U$ ）。如果所有可证原子的合取足以证明后置条件，则流水线成功终止，无需调用 LLM。
阶段 2（LLM 精炼循环）： 如果符号阶段不足以完成任务，流水线进入迭代循环，由 LLM 被提示生成新的不变式。
- 反馈机制： LLM 接收当前程序、 $P$ 、 $D$ 和 $U$ 存储库的内容作为结构化反馈，以及少样本（few-shot）示例。
- 分解与重组： 当 LLM 生成的候选式验证失败时，系统将其分解为子公式（原子）。原子被单独验证并添加到相应的存储库中。所有当前可证原子的合取随后被重新验证。这使得系统能够回收失败的 LLM 提议中有用的组成部分。
- 终止： 循环持续进行，直到找到有效的不变式、迭代预算耗尽或发生超时。

推理策略

作者根据两个设计维度评估了四种推理策略：

验证器反馈（符号先验）：
- 基础型（Basic）： 运行完整的三个阶段流水线，利用来自阶段 1 的符号先验和原子级过滤。
- 仅限 LLM（LLM-Only）： 跳过阶段 1 和原子级分解，仅依靠 LLM 作为一个整体生成归纳不变式。这作为消融基准。
推理结构：
- 思维链（CoT）： 使用标准的提示词，配合逐步推理示例（归纳、霍尔逻辑、霍恩子句或直接推导）。
- 思维树（ToT）： 在“侦察”阶段并行探索多种推导风格，根据其生成的可靠原子数量进行评分，并将剩余的迭代预算集中在表现最好的两种风格上。

核心贡献

神经符号流水线： 一个完整的系统，将本地服务的开源权重 LLM 与 ESBMC 集成，用于自动化循环不变式合成，并完全在内部基础设施上运行。
系统的策略评估： 对纯 LLM、符号引导型和思维树（ToT）变体进行了全面比较，展示了符号反馈和推理结构的影响。
符号反馈增益： 证明了将可证不变式原子作为上下文提供给 LLM 可以带来一致的收益，特别是对于较弱的模型（例如，Llama-3.1-8B 在纯 LLM 基准之上增加了 35 个解决的基准测试）。
提示工程分析： 评估了不同的提示风格（CoT vs. ToT）和推理模板（归纳、霍尔逻辑、霍恩子句）在不变式合成中的表现。
大规模基准测试： 在五种开源权重模型（7B 到 120B 参数）和四种推理策略下进行了广泛评估，涵盖五个基准家族（520 个问题，其中 499 个有效），总计 10,400 个单问题结果。

实验结果

评估是在一台配备四块 NVIDIA RTX A6000 GPU 的服务器上进行的，使用了五种开源权重模型：GPT-OSS-120B、GPT-OSS-20B、Qwen2.5-32B、Qwen2.5-7B 和 Llama-3.1-8B。

整体性能： 最佳单配置（GPT-OSS-120B 配合 Basic 策略）解决了 431/499 个问题（86.4%）。
与现有技术（SOTA）的比较：
- 在相同的本地硬件上运行时，VerIbmc 显著优于传统的符号工具（CPA-Checker, 2ls, ESBMC-Kind）和纯神经工具（Code2Inv）。
- 在共享的基准测试集上，VerIbmc 与那些依赖昂贵外部 API（如 GPT-4）的强力 LLM 增强工具（Clause2Inv, LaM4Inv, LORIS）相当或略低。值得注意的是，VerIbmc 在无需向云端传输代码的情况下实现了这些结果。
- VerIbmc 能够独特地扩展到完整的 SV-COMP 基准集（154 个问题），包括包含数组、嵌套循环和指针的程序，而许多竞争工具由于前端限制无法处理这些程序。
符号阶段的影响： 符号阶段 1 在没有 LLM 调用的情况下解决了 75 个 问题。对于较弱的模型，符号增强提供了显著提升（例如，Llama-3.1-8B 增加了高达 35 个解决的问题）。
ToT vs. CoT： ToT 提示表现出一种多样性与准确性的权衡。虽然它触及了 CoT 无法达到的独特“问题-模型”组合，但通常会产生墙钟时间（wall-clock time）开销，并且对于较弱的模型，由于迭代预算耗尽，会导致解决问题数量的净减少。对于最强的模型（GPT-OSS-120B），CoT 与 ToT 之间的性能差异可以忽略不计。
模型能力： 结果表明，模型能力是准确性的主要驱动力。最强模型与最弱模型之间的差距，明显大于在同一模型内改变策略所带来的性能差异。

意义与主张

本文声称，VerIbmc 证明了基于 LLM 的神经符号方法可以有效地应用于不变式合成，并实现隐私保护和能源高效。通过在本地基础设施上使用开源权重模型，该方法消除了对昂贵的、被锁定在 API 背后的专有前沿模型的依赖。

作者强调，其方法是**构造性健全（sound by construction）**的：每个候选不变式在被接受之前都必须经过形式化验证器（ESBMC）的验证。虽然由于问题的不可判定性，该系统是不完备的，但它为 AI 辅助的形式化验证生产软件提供了一条实用、可扩展且可复现的路径。这项工作向着工业级验证流水线迈进了一步，在这些场景中，数据隐私和资源效率是至关重要的要求。