Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks

TL;DR

This paper introduces an abstraction-refinement method for scalable and exact verification of neural networks, significantly improving verification efficiency and accuracy by combining over-approximation with counterexample-guided refinement.

Contribution

It proposes a novel abstraction-refinement framework that enhances existing verification tools, enabling scalable and precise neural network verification with substantial performance gains.

Findings

Boosts verification performance on benchmarks

Reduces verification time by up to 86.3%

Faster than existing abstraction-refinement approaches

Abstract

As a new programming paradigm, deep neural networks (DNNs) have been increasingly deployed in practice, but the lack of robustness hinders their applications in safety-critical domains. While there are techniques for verifying DNNs with formal guarantees, they are limited in scalability and accuracy. In this paper, we present a novel abstraction-refinement approach for scalable and exact DNN verification. Specifically, we propose a novel abstraction to break down the size of DNNs by over-approximation. The result of verifying the abstract DNN is always conclusive if no spurious counterexample is reported. To eliminate spurious counterexamples introduced by abstraction, we propose a novel counterexample-guided refinement that refines the abstract DNN to exclude a given spurious counterexample while still over-approximating the original one. Our approach is orthogonal to and can be integrated with many existing verification techniques. For demonstration, we implement our approach using two promising and exact tools Marabou and Planet as the underlying verification engines, and evaluate on widely-used benchmarks ACAS Xu, MNIST and CIFAR-10. The results show that our approach can boost their performance by solving more problems and reducing up to 86.3% and 78.0% verification time, respectively. Compared to the most relevant abstraction-refinement approach, our approach is 11.6-26.6 times faster.