LFCS Seminar: Tuesday, 29 October - Samuel Teuber
Title: Provably Safe Neural Network Controllers via Differential Dynamic Logic
Abstract: While neural networks (NNs) have a large potential as goal-oriented controllers for Cyber-Physical Systems, verifying the safety of neural network based control systems (NNCSs) poses significant challenges for the practical use of NNs – especially when safety is needed for unbounded time horizons. One reason for this is the intractability of NN and hybrid system analysis. We introduce VerSAILLE (Verifiably Safe AI via Logically Linked Envelopes): The first approach for the combination of differential dynamic logic (dL) and NN verification. By joining forces, we can exploit the efficiency of NN verification tools while retaining the rigor of dL. The NN verification properties resulting from VerSAILLE typically require nonlinear arithmetic while efficient NN verification tools merely support linear arithmetic. To overcome this divide, we present Mosaic: The first sound and complete verification approach for polynomial real arithmetic properties on piece-wise linear NNs. Mosaic lifts off-the-shelf tools for linear properties to the nonlinear setting. An evaluation on case studies, including adaptive cruise control and airborne collision avoidance, demonstrates the versatility of VerSAILLE and Mosaic: It supports the certification of infinite-time horizon safety and the exhaustive enumeration of counterexample regions while significantly outperforming State-of-the-Art tools in closed-loop NNV. Finally, we provide an outlook on challenges with and solutions to extending our techniques to contexts with finite precision arithmetic (e.g. floats) in sensors, neural networks, and/or actuators.
Bio: Samuel Teuber is a PhD student at Karlsruhe Institute of Technology (KIT) in Germany, advised by Bernhard Beckert at the Application-Oriented Formal Verification group. His research interests lie at the intersection of (deductive) software and AI verification with a focus on applications in Cyber-Physical Systems and Algorithmic Fairness. Previously, he obtained an M.Sc. degree in Computer Science at KIT and completed his Master's Thesis in the Logical Systems Lab at Carnegie Mellon University under the supervision of André Platzer.
LFCS Seminar: Tuesday, 29 October - Samuel Teuber
G.03, IF