NNV Demo: A Neural Network Verification Tool

Authors: Hoang-Dung Tran, Diego Manzanas Lopez, Xiaodong Yang, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, Taylor T. Johnson

Please view the presentation and slides before commenting.

ABSTRACT

NNV (Neural Network Verification) is a frame-work for the verification of deep neural networks (DNNs) and learning-enabled cyber-physical systems (CPS) inspired by a collection of reachability algorithms that make use of a variety of set representations such as the star set. NNV supports exact and over-approximate reachability algorithms used to verify the safety and robustness of feed-forward neural networks(FFNNs). These two analysis schemes are also used for learning enabled CPS, i.e., closed-loop systems, and particularly in neural network control systems with linear models and FFNN controllers with piecewise-linear activation functions. Additionally, NNV supports over-approximate analysis for nonlinear plant models by combining the star set analysis used for FFNNs with the zonotope-based analysis for nonlinear plant dynamics provided by CORA. This demo paper demonstrates NNV'scapabilities by considering a case study of the verification of a learning-enabled adaptive cruise control system.

~~

Please note you must be logged in to the DESTION site to join the discussion. The DESTION organizers are happy to provide you with credentials. Please email: DESTION@cps-vo.org for access.