NASA Logo, National Aeronautics and Space Administration

SafeDNN logo

SafeDNN

The SafeDNN project explores new techniques and tools to ensure that systems that use Deep Neural Networks (DNN) are safe, robust and interpretable. Research directions we are pursuing in this project include: symbolic execution for DNN analysis, label-guided clustering to automatically identify input regions that are robust, parallel and compositional approaches to improve formal SMT-based verification, property inference and automated program repair for DNNs, adversarial training and detection, probabilistic reasoning for DNNs.

Key Benefits

  • Provide strong guarantees wrt safety and robustness for DNNs, making them amenable for use in safety critical domains (particular autonomy).
  • Obtain compact, formal explanations of DNN behavior.
  • Improve testing, debugging and maintenance of DNNs.

Applications

We have applied our techniques to the analysis of deep neural networks designed to operate as controllers in the next-generation Airborne Collision Avoidance Systems for unmanned aircraft (ACAS Xu). We have also studied image classification networks (MNIST, CIFAR) and sentiment networks (for text classification).

Tools

  • Prophecy: property inference for neural networks
  • NeuroSPF: symbolic analysis of neural networks using Symbolic PathFinder

Publications

Ismet Burak Kadron, Divya Gopinath, Corina S. Pasareanu and Huafeng Yu, "Case Study: Analysis of Autonomous Center line Tracking Neural Networks,"
[VSTTEā€™21 (to appear)]

Muhammad Usman, Divya Gopinath, Youcheng Sun, Yannic Noller, Corina S. Pasareanu, "NNrepair: Constraint-Based Repair of Neural Network Classifiers,"
[CAV (1) 2021: 3-25]

Muhammad Usman, Yannic Noller, Corina S. Pasareanu, Youcheng Sun, Divya Gopinath, "NEUROSPF: A Tool for the Symbolic Analysis of Neural Networks,"
[ICSE (Companion Volume) 2021: 25-28]

Edward Kim, Divya Gopinath, Corina S. Pasareanu, Sanjit A. Seshia, "A Programmatic and Semantic Approach to Explaining and Debugging Neural Network Based Object Detectors,"
[CVPR 2020: 11125-11134]

Haoze Wu, Alex Ozdemir, Aleksandar Zeljic, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina S. Pasareanu, Clark W. Barrett, "Parallelization Techniques for Verifying Neural Networks,"
[FMCAD 2020: 128-137]

Corina S. Pasareanu, Hayes Converse, Antonio Filieri, Divya Gopinath, "On the probabilistic analysis of neural networks,"
[SEAMS@ICSE 2020: 5-8]

Hayes Converse, Antonio Filieri, Divya Gopinath, Corina S. Pasareanu, "Probabilistic Symbolic Analysis of Neural Networks,"
[ISSRE 2020: 148-159]

Divya Gopinath, Hayes Converse, Corina S. Pasareanu, Ankur Taly, "Property Inference for Deep Neural Networks,"
[ASE 2019: 797-809]

Divya Gopinath, Mengshi Zhang, Kaiyuan Wang, Ismet Burak Kadron, Corina S. Pasareanu, Sarfraz Khurshid, "Symbolic Execution for Importance Analysis and Adversarial Generation in Neural Networks,"
[ISSRE 2019: 313-322]

Divya Gopinath, Guy Katz, Corina S. Pasareanu, Clark W. Barrett, "DeepSafe: A Data-Driven Approach for Assessing Robustness of Neural Networks,"
[ATVA 2018: 3-19]

Updated 10 September 2021

Project Members

Corina Pasareanu
Divya Gopinath

Collaborators

Clark Barrett (Stanford)
Hayes Converes (UT Austin)
Rishi Dange (Princeton Univ.)
Burak Kadron (UC Santa Barbara)
Guy Katz (Stanford)
Sarfraz Khurshid (UT Austin)
Eddie Kim (UC Berkeley)
Luca Manolache (Palo Alto Highschool)
Ankur Taly (Google)
Muhammad Usman (UT Austn)
Haoze Wu (Stanford)

First Gov logo
NASA Logo - nasa.gov