Formal Reasoning about Golog Programs

Constructing a world-model is a fundamental part of model-based AI, e.g. planning. Usually, such a model is constructed by a human modeller and it should capture the modeller’s intuitive understanding of the world dynamics and how an intelligent agent should behave in the world, e.g. what is its goal and, in some cases, how it should or should not achieve it. Since these models are constructed by human modellers, they can be error-prone. E.g. they might not capture the modellers’ intuition due to a modelling bug. Also, the modeller’s intuition could be flawed, e.g. the model might not capture the world dynamics “correctly” or there might be unintended consequences to the way a goal is specified. All these types of errors impose limits on the applicability of model-based AI in safety-critical applications. 

Although verifying that a model correctly captures the world dynamics or the modeller’s intuition is in many cases impossible, employing formal methods to prove that the model satisfies expected properties can increase the model’s trustworthiness. Previous authors have used formal methods, chiefly automated methods like model- 
checking, to reason about models [5, 9]. However, a limitation of these automated methods arises when reasoning about richer planning formalisms, where proving most relevant properties is undecidable. Examples of that are proving plan validity for planning with continuous change, which amount to deciding solutions to differential equations [15], or the correctness of Golog programs, of which limited versions amounts to undecidable theorem proving problems [1] [9, Chapter 5]. 

In this project you would investigate the use of interactive theorem provers (ITPs) to formally reason about AI models. To prove a fact in an ITP, the user provides high-level steps of a proof, and the ITP fills in the details, at the level of axioms, culminating in a formal proof. The fact that ITPs can use human expertise is a source of their strength in many applications, e.g. when the properties to prove are undecidable. E.g. ITPs are the most successful approach to implement verified realistic software systems [11, 10, 7], where automated methods stand no chance. In the area of AI modelling, Golog [14] programs are such an application, where human aided-reasoning is necessary to prove interesting properties.  

Golog is a programming language for describing the behaviour of intelligent agents. ITPs have been successful when used as tools to reason about program correctness in a multitude of programming languages [13, 8, 4], so it seems promising to use them to reason about Golog programs. In this work you would use an ITP to implement a 
Hoare logic to reason about Golog programs, perhaps building on previous work [12], and implement tooling in an ITP to ease the reasoning about Golog programs. You could also extend that work to reason about Golog programs with (continuous) probabilistic environments or epistemic state information, which are both active research areas, and build on existing program logics for reasoning about quantitative properties of programs [6, 2, 3] to reason about these richer Golog programs. Outcomes of this research would include practical tools to formally reason about Golog programs, making it more likely to use Golog in safety-critical applications. Theoretical outcomes include comparing the ITP’s logic, e.g. Higher-Order Logic, as a framework to formalise semantics of Golog versus situation calculus, which is the current way Golog semantics are usually modelled. This project would also be interesting from a programming language theory perspective, since Golog would be the first fifth-generation language to formalise an ITP.