Formal Verification of Artificial Intelligence Planning Languages

Verification of Artificial Intelligence (AI) is becoming increasingly important due to AI's ever-growing presence across society. AI is already seen in image recognition, financial applications and self-driving vehicles. The correctness of AI is therefore inextricably linked to safety and security in the real world. AI planning is used by robots to create plans to accomplish real-world tasks. The planning is done in a virtual world model where the robot is given a set of actions, an initial state and a goal state and the robot has to compose a plan of sequential actions to reach the goal state. Before any robot carries out real-life execution plans we want to ensure the validity of them. Whilst current planners such as Planning Domain Definition Language (PDDL) run tests to check these plans, they do not supply any proof evidence that the plans are correct. To be truly confident about an AI generated plan we need plans to have proof evidence that can be checked in some formal system.

We have implemented a formal system in the dependently-typed programming language Agda that allow us to write PDDL specifications of planning problems. In this system the specifications of planning problems, usually written in first-order logic, are expressed naturally as types and executable PDDL plans are formalised as programs that inhabit those types. The Curry-Howard correspondence tells us that type checking these specifications in our system thus verifies the correctness of plans as well as supplying proof evidence for the verification. This thesis will focus on a look at what it means for AI planning to be sound, possible logics for representing AI planning specifications as well as the challenges in implementing and proving this in a formal system.