Output Range Analysis for Deep Neural Networks

Abstract

Deep neural networks (NN) are extensively used for machine learning tasks such as image classification, perception and control of autonomous systems. Increasingly, these deep NNs are also been deployed in high-assurance applications. Thus, there is a pressing need for developing techniques to verify neural networks to check whether certain user-expected properties are satisfied. In this paper, we study a specific verification problem of computing a guaranteed range for the output of a deep neural network given a set of inputs represented as a convex polyhedron. Range estimation is a key primitive for verifying deep NNs. We present an efficient range estimation algorithm that uses a combination of local search and linear programming problems to efficiently find the maximum and minimum values taken by the outputs of the NN over the given input set. In contrast to recently proposed "monolithic" optimization approaches, we use local gradient descent to repeatedly find and eliminate local minima of the function. The final global optimum is certified using a mixed integer programming instance. We implement our approach and compare it with Reluplex, a recently proposed solver for deep neural networks. We demonstrate the effectiveness of the proposed approach for verification of NNs used in automated control as well as those used in classification.

Cited by in corpus (28)

• Testing Deep Neural Networks
• Verification for Machine Learning, Autonomy, and Neural Networks Survey
• Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness
• Testing and verification of neural-network-based safety-critical control software: A systematic literature review
• Reachability Analysis and Safety Verification for Neural Network Control Systems
• Algorithms for Verifying Deep Neural Networks
• Certified Robustness for Top-k Predictions against Adversarial Perturbations via Randomized Smoothing
• Exactly Computing the Local Lipschitz Constant of ReLU Networks
• A Survey on Verification and Validation, Testing and Evaluations of Neurosymbolic Artificial Intelligence
• Global Robustness Evaluation of Deep Neural Networks with Provable Guarantees for the $L_0$ Norm
• White Paper Machine Learning in Certified Systems
• Learning Lyapunov Functions for Piecewise Affine Systems with Neural Network Controllers
• Reachability Analysis for Feed-Forward Neural Networks using Face Lattices
• Specification-Guided Safety Verification for Feedforward Neural Networks
• The Partially Observable Games We Play for Cyber Deception
• Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural Network Controllers via Semidefinite Programming
• Learning Approximate Forward Reachable Sets Using Separating Kernels
• Towards the Quantification of Safety Risks in Deep Neural Networks
• Gray-box Adversarial Testing for Control Systems with Machine Learning Component
• Learning Density Distribution of Reachable States for Autonomous Systems
• Reachable Set Estimation for Neural Network Control Systems: A Simulation-Guided Approach
• Formal methods and software engineering for DL. Security, safety and productivity for DL systems development
• A Game Theoretic Analysis of Additive Adversarial Attacks and Defenses
• Insta-RS: Instance-wise Randomized Smoothing for Improved Robustness and Accuracy
• Simplifying Neural Networks using Formal Verification
• Formal controller synthesis for hybrid systems using genetic programming
• Affine Multiplexing Networks: System Analysis, Learning, and Computation
• Learning to Separate Clusters of Adversarial Representations for Robust Adversarial Detection