Verification of Neural Networks: Enhancing Scalability through Pruning

TL;DR

This paper introduces a pruning-based training pipeline that improves the scalability of neural network verification tools, making formal analysis more feasible for larger, practical networks.

Contribution

We propose a novel pruning approach during training that balances accuracy and robustness, enhancing neural network verifiability without significant performance loss.

Findings

Pruning improves neural network verifiability.

Certain pruning and verification combinations are highly effective.

Our method enables formal verification of larger neural networks.

Abstract

Verification of deep neural networks has witnessed a recent surge of interest, fueled by success stories in diverse domains and by abreast concerns about safety and security in envisaged applications. Complexity and sheer size of such networks are challenging for automated formal verification techniques which, on the other hand, could ease the adoption of deep networks in safety- and security-critical contexts. In this paper we focus on enabling state-of-the-art verification tools to deal with neural networks of some practical interest. We propose a new training pipeline based on network pruning with the goal of striking a balance between maintaining accuracy and robustness while making the resulting networks amenable to formal analysis. The results of our experiments with a portfolio of pruning algorithms and verification tools show that our approach is successful for the kind of networks we consider and for some combinations of pruning and verification techniques, thus bringing deep neural networks closer to the reach of formally-grounded methods.