DeepAbstract: Neural Network Abstraction for Accelerating Verification

TL;DR

DeepAbstract introduces a neuron clustering-based abstraction framework for neural networks, reducing network size while maintaining accuracy, thereby enhancing the scalability of verification algorithms for complex architectures.

Contribution

It presents a novel abstraction method for neural networks based on neuron clustering, including error bounds for ReLU networks, improving verification scalability.

Findings

Reduces network size without losing accuracy

Enables transfer of verification results from abstract to original network

Provides error bounds for ReLU network abstraction

Abstract

While abstraction is a classic tool of verification to scale it up, it is not used very often for verifying neural networks. However, it can help with the still open task of scaling existing algorithms to state-of-the-art network architectures. We introduce an abstraction framework applicable to fully-connected feed-forward neural networks based on clustering of neurons that behave similarly on some inputs. For the particular case of ReLU, we additionally provide error bounds incurred by the abstraction. We show how the abstraction reduces the size of the network, while preserving its accuracy, and how verification results on the abstract network can be transferred back to the original network.