Provably Complete Generalized Planning with LLMs

工作流先把 PDDL 语义保持地翻译到 Lean，再要求 LLM 同时产出广义规划程序和覆盖所有满足领域约束实例的证明，最后交给 Lean kernel 检查。GPT-5.6-Sol 在 13 个常用领域里得到 12 个带有效完备性证明的计划。贡献在于把泛化声明从测试集统计提升为内核可验证对象，瓶颈则转移到领域规格和 Lean 形式化的准确性。