PV4 ⊧ NNV: Neural Network Verificationchecks whether the given network is safe

Set-based verification framework for deep neural networks (DNNs) and learning-enabled cyber-physical systems (CPS).

Application domain/field

• Neural network
• Deep neural networks
• Neural network verification

Type of tool

Neural network verifier

Expected input

• Network configuration
• Plant configuration

Format:

? (it is a toolbox for Matlab)

Expected output

SAT or UNSAT which indicates whether the network is safe, i.e. the reachable sets do not violate any of the safety properties. If the network is unsafe then it will provide a complete set of counter-examples that show all possible unsafe initial inputs and states. It is possible for the tool to report UNK in case the result is unknown.

Internals

• NNV consists of a set of reachability algorithms that can be used to reason about deep neural networks (DNNs), specifically for sequential FFNNs (feed forward neural networks) and CNNs (convolutional neural networks), as well as NNCS (neural network control systems) with FFNN controllers.
• These reachability algorithms can be used to compute exact and over-approximate reachable sets of DNNs and neural network control systems (NNCSs).

Uses MPT, CORA, NNMT, HyST, YALMIP, MatConvNet

Comments

The repository calls it a "Matlab Toolbox for Neural Network Verification". It requires the user to install Matlab and use it from within Matlab.