论文标题
携带证明计划：AI计划的资源逻辑
Proof-Carrying Plans: a Resource Logic for AI Planning
论文作者
论文摘要
AI验证和可解释的AI的最新趋势提出了一个问题，即是否可以验证AI计划技术。在本文中，我们提出了一种新颖的资源逻辑，即携带计划（PCP）逻辑，可用于验证AI计划者制定的计划。 PCP逻辑从现有资源逻辑（例如线性逻辑和分离逻辑）以及HOARE逻辑中汲取灵感，而在建模状态和资源感知计划执行方面。它还利用了库里 - 霍尔德逻辑方法，以将计划作为功能和计划前后的条件作为类型的处理。本文提出了两个主要结果。从理论的角度来看，我们表明PCP逻辑相对于AI计划中使用的标准世界语义是合理的。从实际的角度来看，我们提供了PCP逻辑及其健全性证明的完整AGDA形式化。此外，我们通过补充AI计划自动将AI计划解析为AGDA的证明的库来展示此实现的咖喱咖啡馆或功能性价值。我们提供该库和由此产生的AGDA功能的评估。
Recent trends in AI verification and Explainable AI have raised the question of whether AI planning techniques can be verified. In this paper, we present a novel resource logic, the Proof Carrying Plans (PCP) logic that can be used to verify plans produced by AI planners. The PCP logic takes inspiration from existing resource logics (such as Linear logic and Separation logic) as well as Hoare logic when it comes to modelling states and resource-aware plan execution. It also capitalises on the Curry-Howard approach to logics, in its treatment of plans as functions and plan pre- and post-conditions as types. This paper presents two main results. From the theoretical perspective, we show that the PCP logic is sound relative to the standard possible world semantics used in AI planning. From the practical perspective, we present a complete Agda formalisation of the PCP logic and of its soundness proof. Moreover, we showcase the Curry-Howard, or functional, value of this implementation by supplementing it with the library that parses AI plans into Agda's proofs automatically. We provide evaluation of this library and the resulting Agda functions.
