Proof-Carrying Plans: a Resource Logic for AI Planning

Plans can now be formally verified like mathematical proofs: The paper introduces Proof-Carrying Plans (PCP) logic, which allows AI planners' outputs to be verified for correctness, similar to how mathematicians verify theorems. This addresses a key concern in responsible AI about whether we can trust the decisions AI systems make.

Resource constraints are now built into plan verification: Unlike previous approaches, PCP logic explicitly tracks how resources (time, money, materials, etc.) are used throughout a plan's execution. This is critical for responsible AI because it ensures plans don't make impossible promises about resource availability, which could lead to real-world failures.

The approach has been rigorously tested: The authors provide a complete formal proof that their logic is "sound"—meaning verified plans will actually work as intended in the real world. They also created a working implementation in the Agda programming language with automatic parsing of AI plans, demonstrating this isn't just theoretical.

This bridges explainability and verification: By treating AI plans as formal proofs with clear pre-conditions and post-conditions (what must be true before and after each step), the approach makes it easier to explain why an AI planner chose a particular course of action—a key requirement for responsible AI deployment in high-stakes domains.