An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks

TL;DR

This paper introduces Cnn-Abs, an abstraction-refinement framework that enhances the scalability of verifying convolutional neural networks by simplifying the verification problem and integrating with existing verification tools.

Contribution

It presents a novel abstraction-refinement approach specifically designed for convolutional neural network verification, improving scalability and performance.

Findings

Reduces verification runtime by 15.7% on average.

Successfully applies abstraction-refinement to convolutional networks.

Enhances existing verification engines with the Cnn-Abs framework.

Abstract

Convolutional neural networks have gained vast popularity due to their excellent performance in the fields of computer vision, image processing, and others. Unfortunately, it is now well known that convolutional networks often produce erroneous results - for example, minor perturbations of the inputs of these networks can result in severe classification errors. Numerous verification approaches have been proposed in recent years to prove the absence of such errors, but these are typically geared for fully connected networks and suffer from exacerbated scalability issues when applied to convolutional networks. To address this gap, we present here the Cnn-Abs framework, which is particularly aimed at the verification of convolutional networks. The core of Cnn-Abs is an abstraction-refinement technique, which simplifies the verification problem through the removal of convolutional connections in a way that soundly creates an over-approximation of the original problem; and which restores these connections if the resulting problem becomes too abstract. Cnn-Abs is designed to use existing verification engines as a backend, and our evaluation demonstrates that it can significantly boost the performance of a state-of-the-art DNN verification engine, reducing runtime by 15.7% on average.