Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter

Verification has emerged as a means to provide formal guarantees onlearning-based systems incorporating neural network before usingthem in safety-critical applications. This paper proposes a newverification approach for deep neural networks (DNNs) with piecewiselinear activation functions using reachability analysis. The core ofour approach is a collection of reachability algorithms using starsets (or shortly, stars), an effective symbolic representation ofhigh-dimensional polytopes. The star-based reachability algorithmscompute the output reachable sets of a network with a given inputset before using them for verification. For a neural network withpiecewise linear activation functions, our approach can constructboth exact and over-approximate reachable sets of the neuralnetwork. To enhance the scalability of our approach, a star set isequipped with an outer-zonotope (a zonotope over-approximation ofthe star set) to quickly estimate the lower and upper bounds of aninput set at a specific neuron to determine if splitting occurs atthat neuron. This zonotope pre-filtering step reduces significantlythe number of linear programming optimization problems thatmust be solved in the analysis, and leads to a reduction incomputation time, which enhances the scalability of the star setapproach. Our reachability algorithms are implemented in a softwareprototype called the neural network verification tool, and canbe applied to problems analyzing the robustness of machine learningmethods, such as safety and robustness verification of DNNs. Ourexperiments show that our approach can achieve runtimes twenty to1400 times faster than Reluplex, a satisfiability modulotheory-based approach. Our star set approach is also lessconservative than other recent zonotope and abstract domainapproaches.