PV4 ⊧ NNV: Neural Network Verificationchecks whether the given network is safeSet-based verification framework for deep neural networks (DNNs) and learning-enabled cyber-physical systems (CPS).
- Neural network
- Deep neural networks
- Neural network verification
Type of toolNeural network verifier
- Network configuration
- Plant configuration
Format:? (it is a toolbox for Matlab)
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.
- 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).