Formal Methods for Dependable Neural Networks
The deployment of Artificial Neural Networks (ANNs) in safety-critical applications poses a number of new verification and certification challenges. For scenarios such as autonomous driving, it is important to establish sound claims on safety properties over the demonstrated behavior of ANNs. Examples include the absence of tendencies to change to occupied lanes, and resilience of ANNs to noisy or even maliciously manipulated sensory input. In this talk, we highlight some developments as an initial step towards realizing the full potential of formal methods for ANNs and their deployment in new safety-critical functionalities such as self-driving cars. Concretely, we demonstrate concepts such as (1) how to perform automatic verification of ANNs via a reduction to solving mixed integer optimization problems (MIP), and (2) how to monitor and regulate decisions generated by ANNs, by overlaying ANNs with formally synthesized maximal pervasive controllers.
Dr. Chih-Hong Cheng studied Computer Science at Technical University of Munich and obtained his PhD on game-based software synthesis in 2012. After two years working in ABB corporate research as a research scientist, he joined fortiss and is now head of the Software Dependability department. He manages various research projects such as cloud for mission-critical infrastructures, formal methods for dependable machine learning, and techniques for automating software engineering processes.
Georg Nührenberg got a Master’s Degree in Computer Science at ETH Zurich, where he focused on theoretical computer science and mathematical optimization. He wrote his Master’s Thesis at IBM Research Zurich. He obtained his Bachelor’s Degree in Computer Science at FU Berlin. Since November 2016, Georg Nührenberg works in the Software Dependability department of fortiss. His research interests include formal methods for autonomous systems and verification of machine learning algorithms.