Model-Agnostic Reachability Analysis on Deep Neural Networks
This addresses the need for formal verification in safety-critical systems by providing a more flexible and efficient approach for a broader class of deep neural networks, though it is incremental as it builds on existing verification concepts.
The paper tackles the problem of verifying deep neural networks with a model-agnostic framework called DeepAgn, which can analyze reachability for various network types like FNNs and RNNs under Lipschitz continuity, and empirically shows superior capability and efficiency in handling large networks compared to state-of-the-art methods.
Verification plays an essential role in the formal analysis of safety-critical systems. Most current verification methods have specific requirements when working on Deep Neural Networks (DNNs). They either target one particular network category, e.g., Feedforward Neural Networks (FNNs), or networks with specific activation functions, e.g., RdLU. In this paper, we develop a model-agnostic verification framework, called DeepAgn, and show that it can be applied to FNNs, Recurrent Neural Networks (RNNs), or a mixture of both. Under the assumption of Lipschitz continuity, DeepAgn analyses the reachability of DNNs based on a novel optimisation scheme with a global convergence guarantee. It does not require access to the network's internal structures, such as layers and parameters. Through reachability analysis, DeepAgn can tackle several well-known robustness problems, including computing the maximum safe radius for a given input, and generating the ground-truth adversarial examples. We also empirically demonstrate DeepAgn's superior capability and efficiency in handling a broader class of deep neural networks, including both FNNs, and RNNs with very deep layers and millions of neurons, than other state-of-the-art verification approaches.