Speaker: Joost-Pieter Katoen

Title: Facing Uncertainty in AI: From Verification To Synthesis

Abstract: Uncertainties occur in different forms: data may be noisy, mechanisms may be inherently randomised, the visibility (of e.g. a robot) may not be optimal, and the environment in which a system needs to operate may behave in an unknown manner. The central question that we will address is « Can we guarantee that AI systems are safe and resilient in the presence of such uncertainty?’’ We advocate using model-based, formal verification and synthesis with a particular focus on automation. We will present techniques to verify uncertainty aspects modeled as randomness and to use formal synthesis to complete partial designs. Several example AI models — Bayesian networks, partially observable Markov decision processes, and probabilistic programs — will illustrate the capabilities of these approaches.