Proof-Carrying Plans: a Resource Logic for AI Planning

TL;DR

This paper introduces the Proof Carrying Plans (PCP) logic, a novel resource logic inspired by existing logics, designed to verify AI plans through a formal, type-theoretic approach, with a complete Agda implementation.

Contribution

It presents the first formalization and proof of soundness for PCP logic, enabling plan verification via a Curry-Howard style approach with an automated plan-to-proof parser.

Findings

PCP logic is sound relative to AI planning semantics

Complete Agda formalization of PCP logic and its soundness proof

Automated plan parsing into Agda proofs demonstrated

Abstract

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.