Document Type
Article
Publication Date
8-2021
Publication Source
Formal Aspects of Computing
Abstract
Verification has emerged as a means to provide formal guarantees on learning-based systems incorporating neural network before using them in safety-critical applications. This paper proposes a new verification approach for deep neural networks (DNNs) with piecewise linear activation functions using reachability analysis. The core of our approach is a collection of reachability algorithms using star sets (or shortly, stars), an effective symbolic representation of high-dimensional polytopes. The star-based reachability algorithms compute the output reachable sets of a network with a given input set before using them for verification. For a neural network with piecewise linear activation functions, our approach can construct both exact and over-approximate reachable sets of the neural network. To enhance the scalability of our approach, a star set is equipped with an outer-zonotope (a zonotope over-approximation of the star set) to quickly estimate the lower and upper bounds of an input set at a specific neuron to determine if splitting occurs at that neuron. This zonotope pre-filtering step reduces significantly the number of linear programming optimization problems that must be solved in the analysis, and leads to a reduction in computation time, which enhances the scalability of the star set approach. Our reachability algorithms are implemented in a software prototype called the neural network verification tool, and can be applied to problems analyzing the robustness of machine learning methods, such as safety and robustness verification of DNNs. Our experiments show that our approach can achieve runtimes twenty to 1400 times faster than Reluplex, a satisfiability modulo theory-based approach. Our star set approach is also less conservative than other recent zonotope and abstract domain approaches.
Inclusive pages
519-545
ISBN/ISSN
0934-5043
Document Version
Published Version
Publisher
ASSOC Computing Machinery
Volume
33
Peer Reviewed
yes
Issue
4-5
eCommons Citation
Tran, Hoang-Dung; Pal, Neelanjana; Lopez, Diego Manzanas; Musau, Patrick; Yang, Xiaodong; Nguyen, Luan Viet; Xiang, Weiming; Bak, Stanley; and Johnson, Taylor T., "Verification of Piecewise Deep Neural Networks: A Star Set Approach with Zonotope Pre-filter" (2021). Computer Science Faculty Publications. 199.
https://ecommons.udayton.edu/cps_fac_pub/199
Comments
This open-access article is provided for download in compliance with the publisher’s policy on self-archiving. To view the version of record, use the DOI: https://doi.org/10.1007/s00165-021-00553-4