Stepwise: Neuro-Symbolic Proof Search for Automated Systems Verification

📄 arXiv: 2603.19715v1 📥 PDF

作者: Baoding He, Zenan Li, Wei Sun, Yuan Yao, Taolue Chen, Xiaoxing Ma, Zhendong Su

分类: cs.AI

发布日期: 2026-03-20

💡 一句话要点

提出Stepwise神经符号框架，用于自动化系统验证中的定理证明搜索。

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 神经符号计算 自动化定理证明 形式验证 大型语言模型 系统验证

📋 核心要点

  1. 交互式定理证明在形式验证中应用广泛，但手动构建证明脚本限制了其可扩展性。
  2. Stepwise框架结合神经和符号方法，利用LLM生成候选证明步骤，并使用ITP工具进行验证和优化。
  3. 在seL4基准测试中，Stepwise证明了高达77.6%的定理，显著优于现有LLM方法和Sledgehammer。

📝 摘要（中文）

本文提出了一种神经符号证明生成框架，旨在自动化系统级验证项目的证明搜索。该框架在证明状态上执行最佳优先树搜索，并重复查询大型语言模型（LLM）以获得下一个候选证明步骤。在神经方面，我们使用证明状态-步骤对的数据集对LLM进行微调；在符号方面，我们结合了一系列ITP工具来修复被拒绝的步骤，过滤和排序证明状态，并在搜索停滞时自动完成子目标。这种协同作用实现了数据高效的LLM适应和语义感知的搜索空间修剪。我们在一个新的Isabelle REPL上实现了该框架，该REPL公开了细粒度的证明状态和自动化工具，并在FVEL seL4基准和其他Isabelle开发项目上对其进行了评估。在seL4上，该系统证明了高达77.6％的定理，大大超过了以前基于LLM的方法和独立的Sledgehammer，同时解决了更多的多步证明。进一步基准测试的结果表明了强大的泛化能力，表明了可扩展的自动化软件验证的可行途径。

🔬 方法详解

问题定义：当前，使用交互式定理证明进行形式验证需要大量的手动工作来构建证明脚本，这限制了其在复杂系统中的应用。现有的基于LLM的方法虽然有所进展，但在处理复杂的多步证明时仍然存在困难，并且缺乏对证明语义的深入理解，导致效率低下。

核心思路：Stepwise框架的核心思路是将LLM的强大推理能力与传统ITP工具的精确性和可靠性相结合，形成一个神经符号协同系统。LLM负责生成候选的证明步骤，而ITP工具负责验证这些步骤的正确性，并提供反馈以指导LLM的搜索方向。通过这种方式，可以充分利用LLM的泛化能力和ITP工具的精确性，从而提高自动化证明的效率和成功率。

技术框架：Stepwise框架采用最佳优先树搜索算法，在证明状态空间中进行搜索。其主要模块包括：1) LLM：用于生成候选证明步骤；2) ITP工具：用于验证候选步骤的正确性，并提供反馈；3) 状态评估器：用于评估当前证明状态的质量，并指导搜索方向；4) 搜索控制器：用于控制整个搜索过程，包括选择下一个要探索的证明状态，以及何时停止搜索。

关键创新：Stepwise框架的关键创新在于其神经符号协同机制。它不是简单地将LLM作为黑盒使用，而是将其与ITP工具紧密集成，形成一个闭环反馈系统。这种集成使得LLM能够更好地理解证明语义，并生成更有效的证明步骤。此外，该框架还采用了数据高效的LLM微调方法，以及语义感知的搜索空间修剪技术，进一步提高了搜索效率。

关键设计：Stepwise框架使用证明状态-步骤对的数据集对LLM进行微调。具体而言，它使用交叉熵损失函数来训练LLM，使其能够预测给定证明状态下的下一个最佳证明步骤。此外，该框架还使用了一种基于规则的启发式方法来评估证明状态的质量。该启发式方法考虑了多个因素，包括当前证明状态的复杂性，以及距离目标状态的距离。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

Stepwise在FVEL seL4基准测试中证明了高达77.6%的定理，显著优于之前的LLM方法和独立的Sledgehammer。与Sledgehammer相比，Stepwise在seL4基准上提升了约10%的定理证明成功率。此外，Stepwise在解决多步证明方面表现出色，表明其具有更强的推理能力和泛化能力。

🎯 应用场景

该研究成果可应用于各种需要高可靠性保证的系统验证领域，如操作系统内核、安全协议、智能合约等。通过自动化定理证明，可以显著降低验证成本，提高系统安全性，并加速软件开发流程。未来，该技术有望推广到更广泛的软件验证场景，例如代码静态分析和动态测试。

📄 摘要（原文）

Formal verification via interactive theorem proving is increasingly used to ensure the correctness of critical systems, yet constructing large proof scripts remains highly manual and limits scalability. Advances in large language models (LLMs), especially in mathematical reasoning, make their integration into software verification increasingly promising. This paper introduces a neuro-symbolic proof generation framework designed to automate proof search for systems-level verification projects. The framework performs a best-first tree search over proof states, repeatedly querying an LLM for the next candidate proof step. On the neural side, we fine-tune LLMs using datasets of proof state-step pairs; on the symbolic side, we incorporate a range of ITP tools to repair rejected steps, filter and rank proof states, and automatically discharge subgoals when search progress stalls. This synergy enables data-efficient LLM adaptation and semantics-informed pruning of the search space. We implement the framework on a new Isabelle REPL that exposes fine-grained proof states and automation tools, and evaluate it on the FVEL seL4 benchmark and additional Isabelle developments. On seL4, the system proves up to 77.6\% of the theorems, substantially surpassing previous LLM-based approaches and standalone Sledgehammer, while solving significantly more multi-step proofs. Results across further benchmarks demonstrate strong generalization, indicating a viable path toward scalable automated software verification.