Towards Verified Reinforcement Learning for Cyber-physical Tasks

Deep reinforcement learning has made giant leaps in the last few years and even reaches super-human capabilities at tasks like game playing. It is increasingly applied to cyber-physical tasks in the real world, yet whether deep RL systems can be entirely safe for cyber-physical tasks remains an open question. I will talk about how the safety of deep RL systems can be phrased as formal verification question for neural networks. Unfortunately, existing methods for neural network verification are inherently bounded in time and thus inappropriate for RL in cyber-physical domains. I will present a novel formal verification method for neural networks which, for the first time, can assure the safety of a neural network controlling a dynamical system up to unbounded time, thus enabling an entirely new spectrum of verification questions for learned systems.