Verification of Neural Networks: Enhancing Scalability through Pruning
This work addresses the problem of scalability in formal verification for safety-critical applications, representing an incremental improvement by combining existing pruning and verification methods.
The paper tackles the challenge of verifying deep neural networks by introducing a training pipeline that uses network pruning to balance accuracy and robustness, making networks more amenable to formal verification tools, with experimental results showing success for specific network types and technique combinations.
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.