💻 computer science

PROMISE: Proof Automation as Structural Imitation of Human Reasoning

本文提出了 PROMISE 框架，通过将证明生成重构为基于证明状态转换的结构化搜索，利用结构感知挖掘技术从证明状态和策略转换中提取模式，从而在 seL4 基准测试中显著超越了现有方法，实现了高达 186% 的相对性能提升。

原作者： Youngjoo Ahn, Sangyeop Yeo, Gijung Lim, Jongmin Lee, Jinyoung Yeo, Jieung Kim

发布于 2026-04-08

📖 1 分钟阅读☕ 轻松阅读

原作者： Youngjoo Ahn, Sangyeop Yeo, Gijung Lim, Jongmin Lee, Jinyoung Yeo, Jieung Kim

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

这篇论文介绍了一个名为 PROMISE 的新系统，它的目标是帮助计算机自动完成一项极其困难的任务：形式化验证（Formal Verification）。

为了让你轻松理解，我们可以把这项任务想象成**“建造一座完全不会倒塌的摩天大楼”**。

1. 背景：为什么这很难？（建造摩天大楼的噩梦）

想象一下，你要建造一座摩天大楼（比如一个操作系统，像 seL4 微内核）。

传统方法（测试）： 就像你盖好楼后，派人去敲敲墙、跑跑楼梯，看看有没有裂缝。但这只能发现“这里有问题”，不能保证“其他地方绝对没问题”。
形式化验证（数学证明）： 这要求你在盖楼之前，就用数学公式证明每一块砖、每一根钢筋在逻辑上都是完美的，保证大楼永远不可能倒塌。

痛点：
虽然这种方法最安全，但太累了。

以前的证明过程就像让一个人类建筑师，拿着放大镜，手动去检查每一块砖的拼接逻辑。
对于像 seL4 这样的大系统，人类工程师花了几十年的时间，写出的“证明文档”比“大楼图纸”本身还要厚好几倍。
最近，大家想用人工智能（大语言模型，LLM） 来帮忙，让 AI 自动写这些证明。

2. 问题：现有的 AI 为什么“翻车”了？

现在的 AI 助手（比如早期的自动证明工具）在写证明时，就像是一个只会死记硬背的实习生：

它怎么找资料？ 它会在图书馆里搜索关键词。比如你要证明“电梯不能同时停在 1 楼和 2 楼”，它就去找标题里包含“电梯”、“停止”这些词的旧证明。
它的毛病： 它只看表面文字，不看深层逻辑。
- 比喻： 就像你想学做“红烧肉”，实习生去图书馆找了一本叫《红烧肉》的书，但书里讲的是“红烧牛肉”的做法，只是标题写错了。或者它找到的书里，虽然也是做肉，但用的是完全不同的烹饪流派（比如法式煎肉），完全不适合你的中式厨房。
结果： 在简单的数学题上，AI 还能凑合；但一遇到像操作系统这样复杂、环环相扣的大工程，AI 就晕头转向，因为它的参考书（检索到的证明）虽然名字像，但结构完全不对，根本没法用。

3. 解决方案：PROMISE 的“结构模仿”魔法

论文作者提出了 PROMISE 系统。它的核心思想是：不要只模仿“说什么”，要模仿“怎么做”。

核心比喻：从“查字典”变成“看施工流程图”

旧方法（关键词检索）： 就像你在查字典，找“电梯”这个词。
PROMISE 方法（结构检索）： 它不看标题，而是看施工过程中的“状态变化”。

PROMISE 是怎么工作的？

观察“施工状态”：
证明一个定理，就像把一堆杂乱的积木（初始目标）一步步拼成完美的形状（完成证明）。每一步，积木的形状都会变（比如：把一个大目标拆成两个小目标，或者消除一个障碍）。
PROMISE 不关心你拼的是什么积木，它关心的是**“从形状 A 变成形状 B 的这个过程”**。
寻找“同款施工法”：
当 AI 遇到一个难题时，PROMISE 会去数据库里找：“以前有没有人遇到过类似的‘形状变化’？”
- 比如：现在的状态是“需要把一个大房间拆成两个小房间”，PROMISE 会找到以前有人用“拆墙法”成功处理过类似情况的记录。
- 哪怕那个旧案例是处理“厨房”的，而你现在处理的是“卧室”，只要**“拆墙”的逻辑结构是一样的**，PROMISE 就能把那个成功的“拆墙步骤”借过来用。
像人类专家一样思考：
人类专家在盖楼时，不会死记硬背“电梯”这个词，而是会想：“哦，这个情况和我上次处理‘楼梯承重’时的逻辑结构很像，当时我是先加固地基，再拆掉临时支撑。我也应该这么干。”
PROMISE 就是模拟了这种**“结构模仿”**的能力。

4. 实验结果：真的有用吗？

作者拿 seL4 操作系统这个“超级大工程”来测试：

对手： 以前的 AI 助手（Selene, Rango），它们还在用“查关键词”的老办法。
PROMISE： 用“看结构”的新办法。

结果：

PROMISE 的成功率比对手高出了186%（在某些测试中）。
即使换用不同能力的 AI 模型（有的强，有的弱），PROMISE 都能保持很高的成功率，说明它很稳健。
它甚至能帮那些不太聪明的 AI 模型（比如只有 70 亿参数的模型）发挥出接近顶级模型的水平。

5. 总结：一句话看懂

如果把自动证明看作**“教 AI 盖摩天大楼”**：

以前的 AI 是拿着关键词索引去找旧图纸，结果经常拿错图纸，导致大楼盖歪了。
PROMISE 是教 AI 看施工流程图，只要发现现在的“施工难点”和以前某个成功的“施工步骤”在结构上长得像，就直接把那个成功的步骤“复制粘贴”过来，不管大楼的名字叫什么。

PROMISE 证明了：在复杂的系统工程中，模仿人类专家的“思考路径（结构）”，比模仿人类的“说话内容（文字）”要重要得多。 这让 AI 真正具备了处理大规模、高难度软件验证的能力。

1. 研究背景与问题 (Problem)

核心挑战：
尽管大型语言模型（LLM）在自然语言处理和代码生成等领域取得了巨大成功，但在**形式化验证（Formal Verification）**领域，特别是针对大规模系统软件（如操作系统内核、编译器）的自动化证明生成方面，仍面临严峻挑战。

现有方法的局限性：

人工成本高： 形式化验证（如 seL4 微内核）需要专家花费数年甚至数十年的人年进行交互式定理证明（ITP），手动构建详细的证明。
LLM 方法的不足： 现有的 LLM 辅助证明方法通常将证明生成视为单次生成任务（Single-shot）或浅层检索增强（Shallow Retrieval-Augmented）。
- 它们主要基于表面文本相似度（关键词匹配）检索前提或证明片段。
- 这种方法在处理小型、局部上下文时有效，但在面对大规模、高度相互依赖的验证工件（如操作系统内核）时迅速失效。
- 它们无法捕捉证明过程中深层的结构依赖（如文件间、模块间、抽象层间的依赖）以及证明状态演化的动态模式。
结果： 在 seL4 等基准测试中，现有方法的证明覆盖率通常低于 30%，且随着模型规模增加，性能提升并不显著，说明单纯提升模型能力不足以解决可扩展性问题。

2. 核心方法论 (Methodology)

论文提出了 PROMISE (PROof MIning via Structural Embeddings)，这是一个结构感知的证明挖掘框架。其核心理念是将证明生成重新定义为基于结构相似证明引导的有状态、迭代搜索过程，而非简单的文本生成。

2.1 核心思想：从“检索工件”到“检索状态演化”

人类证明工程师在构建证明时，并非仅依赖关键词匹配，而是关注证明状态的演化模式（Proof-state transitions）。PROMISE 模仿这一过程：

证明状态（Proof State）： 包含当前目标（Goals）、假设（Assumptions）和上下文。
状态转移（State Transitions）： 通过应用策略（Tactics）将当前状态转化为新状态的过程。
结构相似性： 检索那些在状态演化路径上与当前目标相似的已解决证明片段，而不仅仅是语义相似的定理。

2.2 系统架构与流程

PROMISE 采用**束搜索（Beam Search）**策略，在 Isabelle/HOL 环境中进行增量式证明构建。

检索增强上下文构建 (Retrieval-Augmented Context)：
- 结构检索 (Structural Retrieval)： 这是 PROMISE 的核心。系统构建了一个包含证明中间状态（Intermediate Goals）及其后续策略后缀（Proof Suffixes）的数据库。
  - 检索过程：解析当前目标 -> 在数据库中查找结构相似的中间状态 -> 根据语义相似度重排序 -> 提取对应的策略模板作为 Few-shot 示例。
  - 评分机制：结合结构相似度（嵌入距离、常量重叠）和语义相似度（目标相似度、常量重叠）进行重排序，确保检索到的模板既结构相似又语义相关。
- 名称检索 (Name Retrieval)： 检索当前上下文中可用的具体定理名称和定义（如 _def 结尾的引理），确保生成的策略引用是合法且上下文相关的。
命令生成器 (Command Generator C)：
- 利用检索到的结构模板和定理名称，构建 Grounded Few-shot Prompt。
- 提示 LLM 生成多样化的候选策略序列（通常 1-2 条命令）。
- 多样性控制： 强制模型覆盖不同的策略家族（如 simp, rule, wp），避免陷入单一策略的重复。
机器检查与验证 (Machine-Checked Verification)：
- 所有候选策略通过 Scala-Isabelle 桥接在 Isabelle 中执行。
- 静态过滤： 在运行前过滤语法错误、无效引用。
- 执行验证： 只有成功推进证明状态（减少子目标数量）或完成证明的候选项才会被保留。
- 全局一致性检查： 即使局部证明完成，也必须通过整个理论库（Whole-theory）的构建检查，确保没有引入未定义的依赖。
束搜索策略 (Beam Search)：
- 维护一个大小为 $B$ 的束（Beam），包含当前最优的多个部分证明路径。
- 评分函数： 基于子目标减少量（Progress）、证明长度（Compactness）和策略多样性（Diversification）对节点进行评分。
- 自适应调整： 根据超时压力和证明进度动态调整束宽度和候选预算。

3. 主要贡献 (Key Contributions)

证明生成的新视角： 提出将自动化证明生成视为基于证明状态转移的过程推理问题，而非基于关键词的检索或战术预测。将“结构化的证明演化”作为大规模验证中的首要推理信号。
PROMISE 框架： 开发了一个模型无关（Model-agnostic）的框架，通过检索和利用证明状态转移模式来指导有状态的证明搜索。它不依赖特定 LLM 的微调，可直接应用于现有的开源或闭源模型。
全面的实证评估： 在 seL4 微内核验证基准（包含 223 个 Isabelle/HOL 定理）上进行了广泛评估。
- 对比了 Selene（基于单次生成/浅层检索）和 Rango（基于关键词检索的迭代搜索）。
- 测试了多种 LLM 后端（Qwen2.5-Coder-7B, GPT-3.5-Turbo, GPT-4.1）。

4. 实验结果 (Results)

在 seL4 基准测试中，PROMISE 在绝大多数设置下显著优于现有方法：

性能提升：
- 在 Qwen2.5-Coder-7B 上，P1 任务成功率从 Selene 的 30% 提升至 77%（提升 47 个百分点），Rango 为 57%。
- 在 GPT-3.5-Turbo 上，P1 任务成功率达到 85%，相比 Selene 提升 43 个百分点。
- 在 GPT-4.1 上，P1 任务成功率为 69%，Rango 为 47%。
- 总体表现： PROMISE 在所有 7 种模型/任务组合中，有 6 种取得了最佳成绩。平均成功率达到 55.7%，远高于 Rango (34.0%) 和 Selene (26.8%)。
鲁棒性： PROMISE 在不同能力的模型间表现出更强的稳定性。例如，在 Qwen2.5 (7B) 和 GPT-3.5 之间，PROMISE 的性能差距很小，而基线方法在不同模型间波动巨大。
P3 任务（高难度）： 在仅使用 Qwen2.5-Coder-7B 的情况下，PROMISE 成功证明了 7 个 P3 级引理，是表现第二好的基线（Rango，3 个）的两倍多。
唯一例外： 在 GPT-4.1 处理 P2 任务时，Rango 略胜一筹（35% vs 33%）。作者分析认为，GPT-4.1 极强的指令遵循能力可能使其过度受限于 PROMISE 的复杂提示结构，而 Rango 较简单的提示反而给了模型更多自由探索的空间。

5. 意义与影响 (Significance)

解决可扩展性瓶颈： 证明了单纯依靠提升 LLM 的推理能力无法解决大规模系统验证的扩展性问题。关键在于检索机制的粒度和对证明结构的理解。
超越文本相似度： 揭示了在形式化验证中，结构相似性（证明如何一步步演化）比文本相似性（关键词匹配）更能有效指导证明生成。
实用价值： 为自动化 seL4 等关键安全系统（如操作系统内核、编译器）的验证提供了可行的技术路径，有望大幅降低形式化验证的人力成本，推动其在工业界的落地。
方法论启示： 为未来的 LLM 辅助定理证明研究指明了方向：需要结合状态感知（State-aware）、结构检索（Structural Retrieval）和迭代搜索（Iterative Search），而非简单的单次生成。

总结： PROMISE 通过将证明生成重构为基于结构状态转移的搜索过程，成功克服了现有 LLM 方法在大规模形式化验证中的局限性，显著提升了自动化证明的成功率和鲁棒性，是迈向大规模系统软件自动化验证的重要一步。