Abstractions for Scalable Verification of AI-Controlled Cyber-Physical Systems

Speaker: Pavithra Prabhakar

Abstract

Traditional feedback controllers in cyber-physical systems (CPS) are being increasingly replaced by learning based components such as artificial neural networks (NN). Given the safety criticality of AI-controlled CPS such as autonomous vehicles, rigorous analysis techniques such as formal verification have become imperative. While there is a rich body of work on formal verification of traditional CPS in the realm of hybrid systems, the area of rigorous testing and analysis of CPS controlled by AI components such as neural networks is still in its nascent stages. One of the main challenges with formal verification of neural network controlled CPS is the scalability of the analysis methods to large networks and complex dynamics. We present a novel abstraction technique for neural network size reduction that provides soundness guarantees for safety analysis, and indicates a promising direction for scalable analysis of of the closed loop system. In particular, our abstraction consists of constructing a simpler neural network with fewer neurons, albeit with interval weights called interval neural network (INN), which over-approximates the output range of the given neural network. We reduce the output range analysis problem on the INNs to solving a mixed integer linear programming problem. Our experimental results highlight the trade-off between the computation time and the precision of the computed output range.

Bio

Pavithra Prabhakar is a professor of computer science at the Kansas State University, where she holds the Peggy and Gary Edwards Chair in Engineering. She obtained her doctorate in Computer Science from the University of Illinois at Urbana-Champaign (UIUC), and was a CMI (Center for Mathematics of Information) fellow at Caltech. She has previously held a faculty position at the IMDEA Software Institute, in Madrid, Spain. Her main research interest is in the Formal Analysis of Cyber-Physical Systems, with emphasis on both theoretical and practical methods for verification and synthesis of hybrid control systems. She is the recipient of a Marie Curie Career Integration Grant from the European Union, an NSF CAREER Award and an ONR Young Investigator Award.