导读
在形式化验证领域，确保关键系统（如操作系统内核、加密协议）的正确性至关重要，但传统交互式定理证明（ITP）高度依赖专家手动编写证明，成为规模化应用的瓶颈。本文提出的 Stepwise 框架，通过神经符号（Neuro-Symbolic）方法，将大语言模型（LLM）的推理潜力与符号证明工具的逻辑严谨性深度融合，实现了对复杂系统验证任务的自动化证明搜索。其核心在于构建一个最佳优先树搜索（Best-First Tree Search）引擎，让LLM在符号工具的引导与修正下，逐步探索证明路径，最终在seL4微内核验证等基准测试中取得了突破性成果。
核心突破
Stepwise 并非简单地将LLM作为代码补全工具，而是构建了一个协同演进的证明搜索生态系统。其革命性体现在：
- 双向赋能循环：LLM提供创造性的证明步骤候选，符号工具（如定理证明器）进行语义验证、错误修复和状态修剪，形成“生成-验证-修正”的闭环。
- 数据高效适应：通过微调LLM于特定领域的证明状态-步骤对数据集，显著提升了模型在目标验证环境下的指令遵循与逻辑一致性能力。
- 搜索空间智能管控：结合启发式评分与符号推理，动态评估证明状态的可行性，有效剪枝无效分支，将LLM的探索聚焦于高成功率路径。
深度解析
1. 框架架构：神经与符号的精密耦合
Stepwise 的核心是一个证明状态树搜索管理器。它将当前的证明目标（Proof Goal）及上下文作为状态节点，循环执行以下步骤：
- 神经提议：将当前证明状态输入给微调后的LLM，模型生成多个候选的下一步证明命令（如
apply auto,unfold definition）。 - 符号执行与过滤：在Isabelle REPL环境中尝试执行每个候选命令。利用ITP工具（如
Sledgehammer）快速验证步骤的有效性，并过滤掉导致错误或无效状态的提议。 - 状态扩展与评分：将成功的证明步骤应用于当前状态，生成新的子状态（子目标）。系统为每个新状态计算一个启发式分数，该分数综合了子目标的复杂度、与最终目标的语义距离等。
- 最佳优先探索：从所有未探索的状态中，选择分数最高的节点进行下一轮扩展，实现导向性的深度搜索。
- 停滞恢复机制：当搜索陷入局部僵局时，自动调用强大的自动化工具（如
auto,simp）尝试批量消解当前子目标，推动证明继续前进。
点击展开原理：Isabelle REPL 与状态管理
Stepwise 实现的关键是构建了一个与 Isabelle 定理证明器深度交互的 **REPL（Read-Eval-Print Loop）接口**。与传统脚本模式不同，该接口能： - **捕获细粒度证明状态**：在证明的任意中间点，获取所有未决子目标（subgoals）、当前可用的假设（assumptions）和已定义的规则。 - **执行原子证明命令**：允许框架以编程方式发送单个证明命令，并立即获取执行后的新状态或错误信息。 - **集成自动化工具**：直接调用 Isabelle 内置的 `Sledgehammer`（尝试调用外部求解器寻找证明）、`auto`、`arith` 等策略，并将它们的结果整合到搜索过程中。 此设计使 Stepwise 能像人类专家一样进行“试探性”推理，并在每一步获得即时、精确的反馈。2. 性能表现：基准测试中的压倒性优势
论文在著名的 FVEL seL4 验证基准 和额外的 Isabelle 开发项目上进行了全面评估。结果清晰地展示了 Stepwise 的卓越性能。
| 评估指标 / 对比系统 | Stepwise (Ours) | Previous LLM-based | Sledgehammer Alone | 说明 |
|---|---|---|---|---|
| seL4 定理证明率 | 77.6% | ~40-50% | ~65% | 在最具挑战性的系统验证基准上取得最高成功率 |
| 多步证明解决能力 | 显著更强 | 有限 | 非常有限 | 能解决需要多步策略组合的复杂证明 |
| 泛化能力 | 强 | 中等 | 依赖配置 | 在其他 Isabelle 项目上保持高性能，表明方法具有普适性 |
| 搜索效率 | 高 | 低 | 高但能力有限 | 通过神经引导的启发式搜索，减少盲目尝试 |
关键发现
表格数据表明，Stepwise 不仅超越了所有先前基于LLM的方法，甚至击败了Isabelle中强大的自动化工具Sledgehammer。这证明了神经引导与符号验证协同的价值：LLM弥补了纯符号搜索在策略创新性和长程推理上的不足，而符号工具确保了LLM输出的正确性并约束了搜索空间。
3. 技术精髓：微调与搜索策略
- LLM微调：使用从Isabelle证明脚本中提取的**（证明状态，下一步命令）** 配对数据对基础LLM进行监督微调。这教会了模型理解特定证明上下文中“接下来合理的步骤是什么”，极大提升了提议的相关性。
- 混合评分函数：状态评分函数
Score(state) = α * Heuristic(state) + β * Neural_Confidence(state)，其中启发式部分评估子目标复杂度，神经置信度部分来自LLM对生成该状态步骤的置信度。两者结合平衡了逻辑进展与模型直觉。
点击展开原理：错误修复与状态修剪
当LLM提议的步骤被证明器拒绝时，Stepwise不会简单地丢弃该分支。其符号组件会尝试进行**轻量级修复**： 1. **参数修正**：检查是否是命令的参数（如引理名称）有误，尝试使用符号索引查找相似的正确引理进行替换。 2. **策略降级**：如果 `apply (rule ...)` 失败，可能尝试更温和的 `apply (erule ...)` 或 `apply (drule ...)`。 3. **前提补全**：如果步骤因缺少前提而失败，系统会自动尝试从已知定理库或当前假设中寻找并添加所需前提。 同时，**状态修剪**策略会识别并丢弃以下状态： - **语义等价状态**：避免对同一子目标的不同表示进行重复探索。 - **明显不可达状态**：例如，子目标中出现了与公理矛盾的假设。 - **深度过大或评分过低的状态**：防止搜索资源浪费在希望渺茫的分支上。未来展望
演进方向
Stepwise 为自动化形式验证开辟了一条清晰的道路，其未来的发展可能聚焦于：
- 跨证明器泛化：将框架适配到 Coq、Lean、HOL4 等其他主流交互式定理证明器，构建通用的神经符号验证平台。
- 自我迭代与学习：引入强化学习机制，让系统能从搜索成功与失败中自主优化其评分函数和LLM的生成策略，实现持续进化。
- 端到端验证合成：不仅自动化证明，还能在LLM的辅助下，参与规约撰写和性质形式化，覆盖从需求到验证的完整链条。
- 硬件与超大规模系统验证：应用于芯片设计、分布式协议等更复杂、对正确性要求极致的场景，挑战验证的极限规模。
挑战与思考
尽管前景光明，Stepwise 及其代表的方向仍面临挑战：
- 可解释性：神经模型的决策过程仍是黑盒，如何让验证工程师信任并理解其生成的证明步骤？
- 计算成本：结合大模型推理与符号计算，对算力要求较高，如何优化以实现实用级的效率？
- 知识边界：LLM在训练数据之外的数学或逻辑概念上可能表现不佳，如何保证其在全新验证项目中的零样本或少样本能力？ 这些挑战正是下一代研究需要攻克的关键。
结语：Stepwise 标志着自动化形式验证从“工具辅助”迈向“智能主导”的关键转折。它证明，通过精心设计的神经符号架构，人工智能不仅能辅助人类专家，更能独立驾驭系统验证中深邃而复杂的逻辑迷宫。这不仅是技术的胜利，更是迈向构建高可信赖智能系统基石的重要一步。