Model-Agnostic Reachability Analysis on Deep Neural Networks
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.
Code (0)
등록된 구현이 없습니다.
Tasks
modelSimilar Papers 제목 키워드 기반
Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training
The intrinsic complexity of deep neural networks (DNNs) makes it challenging to verify not only the networks themselves but also the hosting DNN-controlled systems. Reachability analysis of these systems faces the same c…
Decision MakingReinforcement Learning (RL)Locality Does Not Imply Reachability: Boundary Repair in Block-Sparse Causal Attention
Sparse causal attention is usually described by sequence locality: nearby tokens should remain easy to access, while distant tokens may be dropped to reduce cost. This paper studies a mismatch between sequence locality a…
Data-Driven Reachability Analysis Using Matrix Zonotopes
In this paper, we propose a data-driven reachability analysis approach for unknown system dynamics. Reachability analysis is an essential tool for guaranteeing safety properties. However, most current reachability analys…
Reachability Analysis Using Constrained Polynomial Logical Zonotopes
In this paper, we propose reachability analysis using constrained polynomial logical zonotopes. We perform reachability analysis to compute the set of states that could be reached. To do this, we utilize a recently intro…
Computational EfficiencyIndexing Context-Sensitive Reachability
Many context-sensitive data flow analyses can be formulated as a variant of the all-pairs Dyck-CFL reachability problem, which, in general, is of sub-cubic time complexity and quadratic space complexity. Such high comple…