GPT-5.6-Sol 在 Lean 中为 12 个规划域自动证明广义计划完备

Provably Complete Generalized Planning with LLMs

Katharina Stein, Chaahat Jain, Jörg Hoffmann, Alexander Koller

cs.AI

2026-09-23

萨尔大学把 PDDL 语义保真编进 Lean，用 GPT-5.6-Sol 同时生成广义计划与完备性证明。13 个常用基准域中 12 个通过 kernel 核验，仅 Transport 失败。

这篇在解决什么

广义规划要的不是一道题的解，是一段带循环和分支的策略程序，能解同一个 PDDL 域里所有合法实例。Silver 等人 2024 年和同一组作者 Stein 等人 2026 年已经让 LLM 直接写 Python 广义计划，后者在 14 个基准域的测试集上覆盖率做到 100%。测试集过了，并不等于域里每一道题都过。Stein 2026 自己是人工翻代码、手工证完备的。

自动证完备此前也有路。Hu 和 Levesque 2010 年只覆盖一类「一维」问题。Cui 等人 2023 年能自动证明抽象可靠，从而推出广义计划完备，但实证只到 Blocksworld 清一块积木、IPC Gripper、单车 Logistics 这种规模。萨尔大学和 DFKI 这篇要把这件事做到 IPC 常用域上，并且让证明进 Lean kernel，不再靠人眼。

方法

输入是 PDDL 域，外加用户写好的实例合法性约束和状态不变量。流水线分三步。

确定性的 PDDL 到 Lean 转换器把对象编成自然数，谓词编成布尔函数，动作编成归纳类型的构造子。状态拆成静态部分和动态部分：动作改不了的，比如地点之间的 link，放静态，其余放动态。目标用 Option Bool，none 表示不约束。动作可应用性和状态转移分别写成 actionPre 和 actionApply，再递归抬到动作序列上的 ValidPlan 和 runPlan。转换保持语义：Lean 里一条计划对转换后实例正确，当且仅当对应的 PDDL 计划对原实例正确。
LLM 拿到 Stein 2026 的伪代码策略（必要时人工改过）和完整 Lean 域编码，写出 solve 函数。静态检查是 Lean 过类型，动态检查是拿 6 道小实例跑出来的计划转回 PDDL，用 VAL 验证。最多调试 4 轮。
再让 LLM 证定理：对任意满足 ValidInit 和 ValidGoal 的实例，solve 返回的计划逐步可应用，且执行后满足目标。简单域用整篇生成、整篇改；模型自己说一次写不完时，改成先出证明草稿、逐条 lemma 过 Lean，局部修、不整篇重来。这套迭代改法跟 Ospanov 等人 2025 年的 APOLLO 同一思路。

防作弊有四道门：禁止改解析规则的 notation 和 macro；最终文件必须含原文那条完备性定理；证明不得依赖标准公理以外的公理；整份代码从零重建，用 Lean 独立检查器再过一遍。完备性是相对于用户给的约束来说的。约束写漏了可解性，定理根本不存在。不变量理论上能从初始条件和动作推出来，这里直接写进 ValidState，免得模型从零重推。每个动作模式还会自动生成「合法状态上执行后仍合法」的 lemma。

转换器只覆盖合取条件加否定、无动作代价的 PDDL 片段。类型域会把类型编译成一元谓词。

结果

模型是 GPT-5.6-Sol，温度 1，reasoning 设 high。13 个域来自 Stein 2026 的 17 个域：去掉和 Grippers 太像的 Gripper、LLM 本来就写不出策略的 Beluga，以及可解性不好写约束的 Minigrid 和 Visitall。除 Rovers 外，Stein 2026 已经人工证过这些域的 Python 广义计划完备。

13 个域全部写出 Lean 接受、6 道调试实例全部 VAL 通过的广义计划。10 个域一次过，另外 3 个各调一轮。策略是现成的，计划侧调试少是预期内的。

证明侧：整篇生成最多 6 轮，7/13 过 kernel。剩下 6 个模型第一次就说一次写不完。改成逐声明调试后，又过了 5 个，只剩 Transport。Transport 的计划在 IPC Learning 2023 的 easy 和 medium 测试划分上覆盖率仍是满分。缺的是证明，不是测试表现。

域	证明方式	LLM 交互（计划/证明）	总耗时
Heavy	整篇	1 / 3	9 分钟
Delivery、Ferry、Grippers、Hiking	整篇	1–2 / 2–3	11–13 分钟
Logistics	整篇	1 / 3	20 分钟
Satellite	整篇	1 / 4	27 分钟
Miconic	迭代	1 / 11	25 分钟
Blocksworld	迭代	2 / 24	30 分钟
Goldminer、Spanner	迭代	1 / 36	47–49 分钟
Rovers	迭代	1 / 45	54 分钟
Transport	失败	1 / -	计划 4 分钟

证明 Lean 代码明显更厚。Rovers 提示里已有 293 条声明，模型自己再写 66 条；Heavy 证明侧模型只写 9 条。

论文没有和 Cui 2023 在同一组域上做对照实验。对照是规模：前人自动证明停在 Gripper 量级，这里到了 Rovers、Satellite、Logistics。

为什么重要

给做规划、做 LLM 写代码、做形式化验证的人同一条消息：测试集 100% 和「所有实例都对」之间，现在可以自动填一截。信任根是 Lean kernel，不是模型自己说对。

能直接拿来用的前提很硬。你要会写域约束和不变量，PDDL 还得落在合取加否定这段子集里，策略最好已经有了。这不是「丢一个域文件进去就吐可证程序」的产品。对已经有伪代码策略、需要把人工完备性证明换成机器检查的实验室设置，12/13 过线是可用的。

局限与存疑

策略不是搜出来的，是 Stein 2026 的伪代码改写进 Lean。完备性证明自动化了，策略发现没有。

约束和不变量是人写的。写宽了，定理可能根本证不出；写窄了，证明只覆盖你圈出来的实例族，不是 PDDL 语法上所有问题。论文没有报告约束写错时系统会怎样失败。

只测了一个模型。Transport 为什么卡死，没有错误分类。防作弊规则是他们自己列的清单，没有报告实际拦下过多少次投机证明。

PDDL 覆盖面窄。排除的 4 个域里有两个是可解性约束不好写，等于把「约束语言本身够不够用」留在了评测集之外。

术语

广义规划 (generalized planning)：求一段对整个域成立的策略程序，而不是单实例动作序列。
PDDL：规划域定义语言，用谓词和动作模式描述状态空间。
完备广义计划：对约束圈定的每一个合法实例，程序都返回逐步可应用且达目标的计划。
Lean kernel：Lean 里那一小段被信任的类型检查器。证明项过 kernel，命题才算成立。
VAL：把计划放回 PDDL 语义里检查可应用性和目标达成的外部验证器。

原文与代码

社区讨论

论文提出用 LLM 做「可证明完备」的广义规划新方法 JFPuget