Vertex-based reachability analysis for verifying ReLU deep neural networks

TL;DR

This paper introduces three novel reachability algorithms for verifying ReLU neural networks, with one providing exact results and the others offering over-approximations, all utilizing V-polytope inputs, improving verification performance.

Contribution

The paper presents new reachability algorithms for ReLU networks that outperform existing methods, especially the EPNM algorithm for exact reachable set computation.

Findings

EPNM surpasses state-of-the-art in ACAS Xu verification

Algorithms handle V-polytope inputs effectively

Exact and over-approximate methods demonstrated on neural network verification

Abstract

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.