证明携带计划：一种用于AI规划的资源逻辑

近期AI验证与可解释AI的趋势提出了AI规划技术是否可验证的问题。在本文中，我们提出一种新颖的资源逻辑——证明携带计划（PCP）逻辑，可用于验证AI规划器生成的计划。PCP逻辑在建模状态与资源感知的计划执行方面，受到现有资源逻辑（如线性逻辑与分离逻辑）以及霍尔逻辑的启发。它还利用逻辑上的柯里-霍华德方法，将计划视为函数、将计划的前置与后置条件视为类型。本文给出两个主要结果。从理论角度看，我们证明PCP逻辑相对于AI规划中使用的标准可能世界语义是可靠的。从实践角度看，我们给出PCP逻辑及其可靠性证明的完整Agda形式化。此外，我们通过补充一个将AI计划自动解析为Agda证明的库，展示了该实现的柯里-霍华德（或函数式）价值。我们对该库及所得Agda函数进行了评估。