1: \begin{abstract}

2: 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., ReLU. 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,

3: %, quantitatively comparing the robustness of different model structures, 

4: and generating the ground-truth adversarial example. %Moreover, we theoretically prove that modern neural networks are mostly Lipschitz continuous. 

5: 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. Our tool is available at \url{https://github.com/TrustAI/DeepAgn} 

6: \keywords{Verification \and Deep Learning \and Model-agnostic \and Reachability}

7: \end{abstract}

8: