NASA Logo, National Aeronautics and Space Administration

+NASA Home

+Ames Home

Corina Pasareanu Gives Invited Talk on Formal Analysis for Neural Networks at ATVA 2018
Intelligent Systems Division Banner

Corina Pasareanu Gives Invited Talk on Formal Analysis for Neural Networks at ATVA 2018

Dr. Corina Pasareanu of the Robust Software Engineering (RSE) group, gave an invited talk and tutorial at the 16th International Symposium on Automated Technology for Verification and Analysis (ATVA 2018), which was held October 7-10, 2018, in Los Angeles, California. In her keynote talk Corina described new techniques, developed in collaboration with Carnegie Mellon University and Stanford University, for the formal analysis of neural networks.

BACKGROUND: Deep neural networks have achieved impressive results in many complex applications, including classification tasks for image and speech recognition, and pattern analysis or perception in self-driving vehicles. However, it has been observed that even highly-trained networks are very vulnerable to adversarial perturbations. Adding minimal changes to inputs that are correctly classified can lead to wrong predictions, raising serious security and safety concerns. Existing techniques for checking robustness against such perturbations only consider searching locally around a few individual inputs, providing limited guarantees.

In her talk, Dr. Pasareanu described DeepSafe, a novel approach for automatically assessing the overall robustness of a neural network. DeepSafe applies clustering over known labeled data and leverages off-the-shelf constraint solvers to automatically identify and check safe regions in which the network is robust, i.e., all the inputs in the region are guaranteed to be classified correctly. DeepSafe also introduces the concept of targeted robustness, which ensures that the neural network is guaranteed not to misclassify inputs within a region to a specific target (adversarial) label.

DeepSafe was evaluated on a neural network implementation of a controller for the next-generation Airborne Collision Avoidance System for unmanned aircraft (ACAS Xu), and for the well known Modified National Institute of Standards and Technology (MNIST) network. For these networks, DeepSafe identified input regions that were safe, and also found adversarial inputs that were confirmed by the developers. Corina also reviewed newer techniques that use symbolic execution and formal verification to derive "explanations" of neural network behavior, with provable guarantees.

POINT OF CONTACT: Corina Pasareanu,

First Gov logo
NASA Logo -