Property-Guided LLM Program Synthesis for Planning¶

会议: NeurIPS 2026
arXiv: 2605.16142
论文: https://arxiv.org/abs/2605.16142
领域: 代码智能
关键词: 程序合成、大语言模型、经典规划、反例引导归纳合成、启发式函数

一句话总结¶

本文提出基于性质引导的大语言模型程序合成框架，针对经典规划领域合成 Python 启发式函数，通过验证启发式是否满足形式化的“直接性”（Direct）性质并在违例时提供具体反例状态驱动反向修复，相比采样筛选基线生成候选程序数减少 7.4 倍、验证算力降低约 3 个数量级，且无需组合搜索即可通过爬山法直接求解规划任务。

研究背景与动机¶

利用大语言模型（LLM）进行程序合成在竞赛编程、数学发现和算法挖掘中取得了引人注目的进展，但现有方法大多依赖基于测试通过率或目标函数值的纯数值标量反馈来评估与筛选候选程序。这种数值分数只表明程序“表现好坏”，完全无法解释程序“为何失败”，导致合成框架只能在大规模候选池中盲目采样评估，带来了巨大的模型推理成本与测试执行开销。

在形式化方法领域，反例引导的归纳合成（CEGIS）通过验证器检查候选程序是否满足形式化规范，并在失败时返回导致违例的具体反例输入供合成器定向修复。将这种思想迁移到复杂组合推理问题——特别是经典规划（Classical Planning）中，具有极高的理论与应用价值。在可满足规划任务中，理想的启发式函数应当引导贪婪局部搜索算法（如爬山法 Hill Climbing, HC）从初始状态一路无回溯地行进至目标状态，而不陷入局部最优或平台区；然而，在整个状态空间要求所有存活状态都具备单调下降后继的“下降且避开死胡同”（Descending and Dead-End Avoiding, DDA）性质过于严苛，甚至要求对搜索根本不会访问的无关子图做保证。

本文的切入点在于将形式化验证的判定目标放宽至“直接启发式”（Direct Heuristic / Wet DDA）：仅要求从初始状态出发、沿启发式值严格改善轨迹所能到达的存活状态，必须存在至少一个严格改善的后继状态。核心 idea：将 LLM 嵌入到以直接性质验证为核心的反例引导修复闭环中，一旦候选启发式在训练任务上破坏直接性质便提前终止验证并提取具体违例状态作为结构化反馈，引导模型精准定位逻辑缺陷并合成具有强域外泛化能力的规划启发式函数。

方法详解¶

整体框架¶

该框架的核心是一个以 LLM 为合成器、以深度优先搜索性质校验器为验证器的反例引导修复循环（Counterexample-Driven Repair Loop）。其工作流程分为四个主要阶段：

初始提示与候选生成：向 LLM 输入 PDDL 规划领域的领域定义文件、该领域最小与最大规模的训练任务、两个不相交领域的启发式参考代码以及规范清单，由 LLM 生成首个候选启发式 Python 代码；
深度优先直接性质验证：验证器利用候选代码在领域训练任务集上执行深度优先搜索（DFS），严格检验直接性；
早停与反例抽取：一旦在某个训练任务中检测到性质违例（即扩展到非目标状态却不存在严格改善后继，或者步入死胡同），立即中止后续任务评估，提取违例状态、其启发式值及全部后继状态的启发式值；
历史感知的反例修复提示：将违例任务、具体反例及全部历史尝试代码与失败反馈注入修复提示词，要求 LLM 修复启发式直至通过全量训练任务验证或耗尽迭代预算。

整体流水线如下图所示：

%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}}}%%
flowchart TD
    A["PDDL 领域定义 + 训练任务"] --> B["候选启发式生成"]
    B --> C["深度优先搜索性质验证"]
    C -->|发现反例违例| D["早停与反例状态提取"]
    D --> E["反例引导修复提示构建"]
    E -->|迭代修复提示| B
    C -->|全量训练集通过| F["输出验证通过的直接启发式"]

关键设计¶

1. 目标性质放宽：从全局 DDA 到可达直接启发式（Direct Heuristic）

传统消除局部极小和平台区依赖下降且避开死胡同（DDA）性质，即要求状态空间中所有存活状态（可达、可解且非目标）都存在严格改进后继 \(h(s') < h(s)\)。这一条件过于苛刻，强制启发式对规划器从不展开的分支赋予下降保证。本文放宽该约束，聚焦于弱下降避死胡同性质（WDDA，简记为直接启发式 Direct Heuristic）：设 \(S_\downarrow\) 为从初始状态 \(s_0\) 出发、仅通过启发式严格下降转移 \(h(s_{i+1}) < h(s_i)\) 所能到达的存活状态集合。直接性质仅要求：对任意 \(s \in S_\downarrow\)，存在至少一个后继 \(s' \in \text{succ}(s)\) 满足 \(h(s') < h(s)\)，且所有此类改进后继要么是目标状态，要么自身仍属于 \(S_\downarrow\)。这一放宽不仅保留了爬山法（HC）沿贪婪路径必达目标的完备性保证，同时极大缩小了合法启发式的搜索空间，使基于验证的反例反馈具有高度局部性与针对性。

2. 深度优先搜索早停与结构化反例提取

为了在多项式时间内检验候选启发式是否满足直接性质，系统在每个训练任务上自初始状态 \(s_0\) 启动深度优先搜索（DFS）。DFS 的入栈规则严格限定为仅推入满足 \(h(s') < h(s)\) 的严格改善后继状态；若当前出栈的非目标状态 \(s\) 没有任何严格更小的后继，说明直接性质被破坏。此时验证程序立即早停（Early Stopping），避免遍历指数级增长的搜索空间，并提取两类结构化反例之一： - 局部极小 / 平台反例：记录违例状态 \(s\)、其启发式估值 \(h(s)\)，以及全部候选后继状态 \(s'\) 及其对应的启发式估值 \(h(s')\)，明确指示模型为何无法继续下降； - 死胡同反例：当 DFS 通过严格改善转移步入无任何可用动作的非目标死胡同状态 \(s\) 时，记录 \(s\)、父状态 \(s'\) 及其估值，并给出显式约束反馈——建议 \(h(s) \ge h(s')\)，促使爬山法未来在父节点不会贪婪步入该分支。

3. 累积历史感知的上下文修复提示机制

在每次反例修复迭代中，提示词不仅呈现当前的违例任务 PDDL 和结构化反例诊断，还完整保留先前所有迭代生成的代码版本及其对应的反例反馈。这种上下文累积使 LLM 能够进行反思性推理（Reflective Reasoning）：分析之前版本为何修复了局部反例却引入了新平台区，从而避免在相似的启发式拓扑缺陷间来回振荡。例如在 Blocksworld 中，模型能够观察到独立动作惩罚与持块状态惩罚的不一致，进而演进为构造积木依赖图并进行环路检测。

一个完整示例：Blocksworld 依赖环路修复过程¶

以积木世界（Blocksworld）领域的修复过程为例，展示反例反馈如何驱动启发式从局部贪婪计数演进为拓扑推理：

初始启发式（Iteration 0）：模型提出一个简单计数启发式，对每个放错位置的积木计 2 步（拿起+放下），若机械臂当前持块则减 1；同时检测死锁，当桌面上积木的目标底座未就绪时加惩罚 2；
违例暴露：在任务 p06.pddl 中，状态为机械臂持块 \(b_3\)，桌上有 \(b_1, b_2\)，估值 \(h=3\)。然而所有可用动作（将 \(b_3\) 堆叠到 \(b_1\) 或 \(b_2\)，或将 \(b_3\) 放置到桌面）的后继估值分别变为 6、6、4，没有任何后继小于 3，直接性破缺；
反例反馈与演进：验证器将当前状态特征、动作转移增删命题及后继估值注入修复提示；模型发现手持状态和机械臂清空状态下的惩罚条件存在语义不一致；
最终直接启发式：经过 3 轮修复后，LLM 合成了构造积木依赖图的 Python 函数：为相互阻碍的积木建立有向边，通过检测依赖环路在机械臂为空时即预判出死锁并加入 +2 罚分，彻底消除了局部极小，在全量 90 道复杂测试题上实现直接下降。

实验关键数据¶

主实验¶

实验基于 IPC 2023 学习赛道（Learning Track）的 10 个经典规划领域展开，测试集包含 900 个完全域外（OOD）的大规模任务（每个领域 90 题）。对比基线包括：经典删除松弛启发式 FF，以及 Corrêa 等人（2025）提出的前代最佳 LLM 启发式生成方法“采样与筛选”（Sample-and-Select, S&S，固定采样 25 个候选并选用训练集覆盖率最高者，使用相同 Gemini 3.1 Pro 重新运行评测）。搜索算法对比贪婪最佳优先搜索（GBFS）与爬山法（HC）。指标为任务求解覆盖数（Coverage，满分 900）。

领域（各 90 题）	FF (GBFS)	FF (HC)	S&S (GBFS)	S&S (HC)	覆盖率消融 Cov. (HC)	本文 Direct (HC)
Blocksworld	23	0	84	90	49.7	77.3
Childsnack	12	0	58	70	46.7	71.7
Ferry	45	0	67	71	49.3	72.3
Floortile	11	0	30	0	15.7	40.7
Miconic	61	1	83	7	34.0	90.0
Rovers	29	2	44	12	20.7	42.7
Satellite	35	17	57	60	57.3	55.7
Sokoban	29	1	30	0	12.7	30.0
Spanner	30	6	66	79	79.0	75.0
Transport	23	3	54	41	47.3	68.0
总计 (900 题)	298	30	573	430	412.3	623.3

消融实验与开销对比¶

为剥离“直接性质检查”与“单纯交互式修复反馈”的影响，消融实验（Cov.）在相同修复循环中用训练任务覆盖数及展开节点数等数值反馈替换直接性质验证。下表展示了性能与合成/评估代价的对比：

方法配置	LLM 平均生成候选数 (次/Run)	评估时间 (CPU 时间/领域)	HC 测试覆盖数 (总分 900)	GBFS 测试覆盖数 (总分 900)
S&S 基线 [16]	25.0 (固定预算)	206.25 CPU 小时	430.0	573.0
数值覆盖率反馈消融 (Cov.)	~3.5	~15 分钟	412.3 ± 41.9	572.7 ± 16.0
本文方法 (Direct)	3.37 ± 2.99	10.75 分钟	623.3 ± 6.7	- (无需搜索)

关键发现¶

零搜索求解超越经典搜索：本文合成的直接启发式配合纯贪婪爬山法（HC，完全不维护 Open 列表，不进行组合回溯），在 900 个 OOD 测试任务上求解了 623.3 题，显著高于 S&S 结合全功能 GBFS 搜索的 573 题；而 FF 启发式在 HC 下仅能求解 30 题，证实了直接性质对消除局部极小的决定性作用；
合成与验证算力呈数量级缩减：借助反例引导与验证早停，本文平均每个领域仅需生成 3.4 个程序候选即可收敛（相比 S&S 节省约 7.4 倍 LLM 调用），评估时间从 S&S 的 206.25 CPU 小时大幅缩减至 10.75 分钟（降低约 1150 倍）；
强大的域外直接性泛化：虽然直接性仅在小规模训练任务上通过 bounded DFS 检验，但在 900 个大规模 OOD 测试任务的 2700 次独立测试运行中，仅有 1 次因违反直接性质在非死胡同处停滞（出现在 Floortile 领域），其余失败均系超时。即使在 PSPACE 完全的推箱子（Sokoban）领域，也未发生过一次直接性质违例。

亮点与洞察¶

反例早停打破状态空间爆炸诅咒：传统规划验证面临指数级展开困难，本文利用直接性质的违例特性，在遇到第一个无改进后继的存活状态时立即掐断搜索并提取反例，以极低代价完成了原本难以负担的模型诊断；
从标量打分到结构化语义 Debugging：现有 LLM 算法合成（如 FunSearch、AlphaCode）依赖黑盒适应度标量，导致“盲人摸象”式的大规模试错；本文证明了形式化反例能够使 LLM 洞悉状态转移层面的语义断层，进而合成带有图分析与序列依赖的高阶算法；
确定性形式化性质引导的程序发现范式：任何具备可高效检验的形式化性质（如单调性、拟凸性、守恒律）的合成任务，均可借鉴这种将验证器早停反例反馈与 LLM 递归修复结合的架构，摆脱单纯依靠数值 Reward 的暴力搜索。

局限与展望¶

依赖高效可检验的形式化性质：若应用领域不存在类似于直接启发式这样具有局部反例对应关系的明确性质，或者训练任务无法暴露关键反例，本方法将退化为普通的数值试错机制；
小样本验证无全域直接性证明：在有限训练集上通过 DFS 检验并不能在理论上完全保证任意规模任务上的严格直接性，虽然经验上泛化极佳，但极端实例仍存在违例可能；
非受限 Python 代码的可解释性与安全性验证：生成的启发式为任意 Python 脚本，虽表现强大，但相比具有受限语法的线性电位启发式（Potential Heuristics），更难使用自动化定理证明器进行全域形式化验证。未来可探索将反例修复与神经定理证明结合，直接输出可机检的完备证明。

评分¶

新颖性: ⭐⭐⭐⭐⭐ 首次将反例引导的形式化性质检验引入 LLM 规划启发式合成，构建了高效的早停修复闭环。
实验充分度: ⭐⭐⭐⭐⭐ 覆盖 IPC 2023 学习赛道 10 个领域、900 个 OOD 测试任务，包含多轮独立运行、标准差报告、消融及细致代码案例分析。
写作质量: ⭐⭐⭐⭐⭐ 概念阐述清晰严谨，从形式化定义到算法实现与案例递进自然流畅。
价值: ⭐⭐⭐⭐⭐ 为符号规划求解提供了极其高效的启发式生成手段，并为代码智能领域的程序合成范式提供了极具推广价值的架构思路。