Over the last two decades, there has been a blossom in artificial intelligence (AI), with implications reaching everywhere from healthcare, marketing, banking, gaming to the automotive industry. Although AI is powerful and performs even better than humans on many complicated tasks, it has stimulated a longstanding debate for many years between researchers, tech companies, and lawmakers as to whether we can bet human lives on AI? To be able to use AI in safety-critical applications, there is an urgent need for methods that can prove the safety of AI systems. Conventional methods for demonstrating the safety of AI systems using extensive simulation and rigorous testing are usually costly and incomplete. For example, to achieve the catastrophic failure rates of less than one per hour, autonomous vehicle systems need to perform billions of miles of test- driving. More importantly, these driving tests do not cover all corner-cases that may arise in the field. Consequently, new approaches based on formal methods, safe planning and synthesis, and robust learning are urgently needed for not only proving but also enhancing the safety and reliability of AI systems. In principle, these new approaches can automatically explore all unforeseen scenarios when verifying or falsifying the safety of AI systems. They also can generate provably correct planning decisions, safe control actions, and improve the robustness of AI systems under uncertain scenarios and adversarial attacks.

This talk will present NNV, a novel framework for safety and robustness verification of deep neural networks (DNNs) and autonomous cyber-physical systems with learning-enabled components under adversarial attacks, sensing, actuating, and model uncertainties. The crux of our framework is reachability algorithms that can efficiently compute the reachable sets of a DNN or a neural network control system (NNCS). These reachable sets, containing all possible (output) states of the system under uncertainties, are used to verify if the system satisfies its desired properties. I will show the applicability of the NNV framework in a wide range of applications, such as verifying: 1) the safety of ACAS Xu networks, a set of neural networks for supervisory control of the airborne collision avoidance system X, 2) the robustness of the VGG16 and VGG19 perception networks, and 3) the safety of the advanced emergency braking system and adaptive cruise control system in autonomous driving.

 

Bio

 

Dung Tran is an Assistant Professor in the Department of Computer Science and Engineering at the University of Nebraska, Lincoln (UNL). He is a co-director of the NIMBUS Lab at UNL, where he leads the Verification and Validation for Assured Autonomy group (V2A2). He earned a Ph.D. degree in Computer Science at Vanderbilt University in August 2020. His research interests are specification language, formal verification, monitoring, safe control, planning, and learning for autonomous cyber-physical systems (CPS), focusing on in-road and off-road autonomous driving, human-robot-interaction in construction and surgery. His group develops both software and hardware prototypes for their research. Dr. Tran has been developing the NNV (Neural Network Verification) framework for Deep Neural Networks and Learning-enabled CPS. The NNV tool is gaining great attention from industry and academia. It is used in Northrop Grumman for the DARPA Assured Autonomy project and is currently partially supported by Toyota Research. His work on verification of learning-enabled CPS has won the prestigious IEEE TCCPS outstanding dissertation award 2021. 

 

Host

 

Shreyas Sundaram, sundara2@purdue.edu