Vertex-based reachability analysis for verifying ReLU deep neural networks
Neural networks achieved high performance over different tasks, i.e. image identification, voice recognition and other applications. Despite their success, these models are still vulnerable regarding small perturbations, which can be used to craft the so-called adversarial examples. Different approaches have been proposed to circumvent their vulnerability, including formal verification systems, which employ a variety of techniques, including reachability, optimization and search procedures, to verify that the model satisfies some property. In this paper we propose three novel reachability algorithms for verifying deep neural networks with ReLU activations. The first and third algorithms compute an over-approximation for the reachable set, whereas the second one computes the exact reachable set. Differently from previously proposed approaches, our algorithms take as input a V-polytope. Our experiments on the ACAS Xu problem show that the Exact Polytope Network Mapping (EPNM) reachability algorithm proposed in this work surpass the state-of-the-art results from the literature, specially in relation to other reachability methods.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems
This paper presents the Neural Network Verification (NNV) software tool, a set-based verification framework for deep neural networks (DNNs) and learning-enabled cyber-physical systems (CPS). The crux of NNV is a collecti…
The FABRIC Strategy for Verifying Neural Feedback Systems
Forward reachability analysis is a dominant approach for verifying reach-avoid specifications in neural feedback systems, i.e., dynamical systems controlled by neural networks, and a number of directions have been propos…
Time-to-reach Bounds for Verification of Dynamical Systems Using the Koopman Spectrum
In this work, we present a novel Koopman spectrum-based reachability verification method for nonlinear systems. Contrary to conventional methods that focus on characterizing all potential states of a dynamical system ove…
A New Strategy for Verifying Reach-Avoid Specifications in Neural Feedback Systems
Forward reachability analysis is the predominant approach for verifying reach-avoid properties in neural feedback systems (dynamical systems controlled by neural networks). This dominance stems from the limited scalabili…
POLAR-Express: Efficient and Precise Formal Reachability Analysis of Neural-Network Controlled Systems
Neural networks (NNs) playing the role of controllers have demonstrated impressive empirical performances on challenging control problems. However, the potential adoption of NN controllers in real-life applications also …