Governance Node Seminar - Ekaterina Komendantskaya, Heriot Watt University

Speakers: E.Komendantskaya, A.Hill, M.Daggitt.

In this talk, we will consider the “pyramid” of methods deployed in modelling and implementing complex autonomous systems, from the low-level perception methods in the style of statistical machine learning, to the algorithms that do search, planning and reasoning. We will focus in particular on the more enigmatic group of methods situated at the top of the pyramid and responsible for interpretation and verification of the outputs of the algorithms deployed on the lower levels of the pyramid. Our recent work (https://arxiv.org/pdf/2105.11267.pdf) has been focused on developing a safe and correct-by-construction embedding of the outputs of AI planners such as STRIPS into higher-order reasoning and proof environments (such as the dependently-typed language Agda), with a view of  establishing a general methodology for higher-order reasoning, interpretation and verification of complex AI systems. In the second half of the talk, we will discuss some illustrative examples and technical details of this methodology at work.