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.

翻译：验证在安全关键系统的形式化分析中扮演着重要角色。当前大多数验证方法在处理深度神经网络时具有特定要求：它们要么针对特定网络类别（如前馈神经网络），要么针对具有特定激活函数（如ReLU）的网络。本文开发了一种称为DeepAgn的模型无关验证框架，并证明其可应用于前馈神经网络、递归神经网络或两者的混合结构。在Lipschitz连续性假设下，DeepAgn基于一种具有全局收敛保证的新型优化方案分析深度神经网络的可达性，无需访问网络内部结构（如层和参数）。通过可达性分析，DeepAgn能够解决多个众所周知的鲁棒性问题，包括计算给定输入的最大安全半径以及生成真实对抗样本。我们还通过实验证明，相较于其他最先进的验证方法，DeepAgn在处理更广泛的深度神经网络（包括包含极深层结构与数百万神经元的前馈神经网络和递归神经网络）时具有更优越的能力和效率。