Simplifying Neural Networks using Formal Verification

TL;DR

This paper introduces a tool that uses formal verification engines to simplify deep neural networks by reducing their size while maintaining accuracy, demonstrated on aircraft collision avoidance models.

Contribution

It presents a novel application of neural network verification engines for network simplification, enabling size reduction without accuracy loss.

Findings

DNN size reduced by up to 10%

Effective verification-based simplification demonstrated on real-world models

Potential for wider adoption of verification tools in model optimization

Abstract

Deep neural network (DNN) verification is an emerging field, with diverse verification engines quickly becoming available. Demonstrating the effectiveness of these engines on real-world DNNs is an important step towards their wider adoption. We present a tool that can leverage existing verification engines in performing a novel application: neural network simplification, through the reduction of the size of a DNN without harming its accuracy. We report on the work-flow of the simplification process, and demonstrate its potential significance and applicability on a family of real-world DNNs for aircraft collision avoidance, whose sizes we were able to reduce by as much as 10%.