教LLM提问：面向欠指定推理的自查询范畴论规划

使用大语言模型进行的推理时规划在部分可观测性下经常失败：当任务关键的前提条件在查询时未被指定，模型倾向于幻觉出缺失事实或产出违反硬约束的计划。我们提出自查询双向范畴规划（SQ-BCP），它显式表示前提状态（Sat/Viol/Unk），并通过（i）向oracle/用户发起有针对性的自查询，或（ii）通过附加动作建立缺失条件的桥接假设来消解未知项。SQ-BCP执行双向搜索，并调用基于拉回的验证器作为目标兼容性的范畴论证书，而基于距离的分数仅用于排序和剪枝。我们证明，当验证器成功且硬约束通过确定性检查时，被接受的计划与目标要求兼容；在有界分支和有限消解深度下，若存在可接受计划，SQ-BCP能找到它。在隐瞒前提条件的WikiHow和RecipeNLG任务上，SQ-BCP将资源违反率降至14.9%和5.8%（最佳基线分别为26.0%和15.7%），同时保持有竞争力的参考质量。