NNV Design Studio
NNV Design Studio

Exploration tool for Neural Network Verification (NNV) tool from Verivital Labs, Vanderbilt University.

nnv (Matlab Toolbox for Neural Network Verification)  This toolbox implements reachability methods for analyzing neural networks, particularly with a focus on closed-loop controllers in autonomous cyber-physical systems (CPS).

Tools and Related Features

This toolbox makes use of the neural network model transformation tool (nnmt) and for closed-loop systems analysis, the hybrid systems model transformation and translation tool (HyST).

Novel Features

Vertical view of a generic example of the ACAS Xu benchmark set

Exact reachable set of an ACAS Xu network

Verification time (VT) can be reduced by increasing the number of cores (N)

Reachable set of an ACAS Xu network with different methods

Complete Set of Counter Inputs of an ACASXu network

Reachable set of a network with Sigmoid activation functions

Neural Network Adaptive Cruise Control System

Reachable set of the neural network adaptive cruise control system

A falsification trace of the neural network adaptive cruise control system

Advanced Emergency Braking System with Reinforcement Controller

Reachable set of the advanced emergency braking system with reinforcement controller

Safe initial condition of the advanced emergency braking system with reinforcement controller

VGG16 under adversarial attacks

VGG19 exact output ranges corresponding to FGSM adversarial attack

nnv generates counter examples for VGG19 corresponding to FGSM adversarial attack

  1. NNV can compute and visualize the exact reachable sets of feedforward neural networks with ReLU/Saturation activation functions. The computation can be accelerated using parallel computing in Matlab. The computed reachable set can be used for safety verification of the networks.
  2. NNV can construct and visualize the complete counter inputs of feedforward neural networks with ReLU/Saturation activation functions.
  3. NNV can compute and visualize the over-approximate reachable sets of feedforward neural networks with Tanh, Sigmoid activation functions.
  4. NNV can compute and visualize the reachable sets of neural network control systems, i.e., systems with plant + neural network controllers which can be used to verify or falsify safety properties of the systems.
  5. New feature: Our nnv now supports robustness verification for very large convolutional neural networks such as VGG16, VGG19 under adversarial attacks (FGSM, DeepFoll, etc.)
Important!

You must first be logged into the portal. If you have no account, you can create one here.

Acknowledgements

This work is supported in part by the  DARPA Assured Autonomy  program.

Contacts

Taylor Johnson

ORGANIZATION

Vanderbilt University, Nashville, TN, USA

References
Tran, H. -D., Yang, X., Lopez, D. M., Musau, P., Nguyen, L. V., Xiang, W., et al. (2020). NNV: A Tool for Verification of Deep Neural Networks and Learning-Enabled Autonomous Cyber-Physical Systems. In 32nd International Conference on Computer-Aided Verification 2020. Los Angeles, California, USA: Springer, Cham. http://doi.org/10.1007/978-3-030-53288-8_1
Tran, H. -D., Bak, S., Xiang, W., & Johnson, T. T. (2020). Verification of Deep Convolutional Neural Networks Using ImageStars. In 32nd International Conference on Computer-Aided Verification 2020. Los Angeles, California, USA: Springer, Cham. http://doi.org/10.1007/978-3-030-53288-8_2
Tran, H. -D., Xiang, W., & Johnson, T. T. (2019). Verification Approaches for Learning-Enabled Autonomous Cyber-Physical Systems. The IEEE Design \& Test 2019.
Tran, H. -D., Lopez, D. M., Musau, P., Yang, X., Nguyen, L. V., Xiang, W., & Johnson, T. T. (2019). Star-Based Reachability Analsysis for Deep Neural Networks. In The 23rd International Symposium on Formal Methods (FM). Porto, Portugal: Springer, Cham. http://doi.org/10.1007/978-3-030-30942-8_39
Tran, H. -D., Cai, F., Lopez, D. M., Musau, P., Johnson, T. T., & Koutsoukos, X. D. (2019). Safety Verification of Cyber-Physical Systems with Reinforcement Learning Control. In The International Conference on Embedded Software (EMSOFT). New York, New York, USA: ACM. http://doi.org/10.1145/3358230
Tran, H. -D., Musau, P., Lopez, D. M., Yang, X., Nguyen, L. V., Xiang, W., & Johnson, T. T. (2019). Parallelizable Reachability Analsysis Algorithms for FeedForward Neural Networks. In 7th International Conference on Formal Methods in Software Engineering. Montreal, Quebec, Canada: IEEE. http://doi.org/10.1109/FormaliSE.2019.00012
Xiang, W., Tran, H. -D., & Johnson, T. T. (2018). Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks. Ieee Transactions On Neural Networks And Learning Systems, 29, 5777-5783. http://doi.org/10.1109/TNNLS.2018.2808470
Xiang, W., Tran, H. -D., & Johnson, T. T. (2018). Reachable Set Computation and Safety Verification for Neural Networks with ReLU Activations. Retrieved from https://www.researchgate.net/publication/322048764_Reachable_Set_Computation_and_Safety_Verification_for_Neural_Networks_with_ReLU_Activations
Xiang, W., Lopez, D. M., Musau, P., & Johnson, T. T. (2018). Reachable Set Estimation and Verification for Neural Network Models of Nonlinear Dynamic Systems. Unmanned System Technologies: Safe, Autonomous And Intelligent Vehicles. Retrieved from https://www.researchgate.net/publication/323141736_Reachable_Set_Estimation_and_Verification_for_Neural_Network_Models_of_Nonlinear_Dynamic_Systems
Xiang, W., & Johnson, T. T. (2018). Reachability Analysis and Safety Verification for Neural Network Control Systems. Arxiv. Retrieved from https://arxiv.org/abs/1805.09944
Xiang, W., Musau, P., Wild, A. A., Lopez, D. M., Hamilton, N., Yang, X., et al. (2018). Verification for Machine Learning, Autonomy, and Neural Networks Survey. Arxiv. Retrieved from https://arxiv.org/abs/1810.01989
Xiang, W., Tran, H. -D., & Johnson, T. T. (2018). Specification-Guided Safety Verification for Feedforward Neural Networks. Arxiv. Retrieved from https://arxiv.org/abs/1812.06161
Lopez, D. M., Musau, P., Tran, H. -D., & Johnson, T. T. (2019). Verification of Closed-loop Systems with Neural Network Controllers (Benchmark Proposal). In 6th International Workshop on Applied Verification of Continuous and Hybrid Systems. Montreal, Quebec, Canada. http://doi.org/10.29007/btv1
Lopez, D. M., Musau, P., Tran, H. -D., Dutta, S., Carpenter, T. J., Ivanov, R., & Johnson, T. T. (2019). ARCH-COMP19 Category Report: Artificial Intelligence / Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants. In 6th International Workshop on Applied Verification of Continuous and Hybrid Systems. Montreal, Quebec, Canada. http://doi.org/10.29007/rgv8