Fast Neural Network Verification via Shadow Prices

Abstract

To use neural networks in safety-critical settings it is paramount to provide assurances on their runtime operation. Recent work on ReLU networks has sought to verify whether inputs belonging to a bounded box can ever yield some undesirable output. Input-splitting procedures, a particular type of verification mechanism, do so by recursively partitioning the input set into smaller sets. The efficiency of these methods is largely determined by the number of splits the box must undergo before the property can be verified. In this work, we propose a new technique based on shadow prices that fully exploits the information of the problem yielding a more efficient generation of splits than the state-of-the-art. Results on the Airborne Collision Avoidance System (ACAS) benchmark verification tasks show a considerable reduction in the partitions generated which substantially reduces computation times. These results open the door to improved verification methods for a wide variety of machine learning applications including vision and control.

References in corpus (8)

• Playing Atari with Deep Reinforcement Learning
• End to End Learning for Self-Driving Cars
• Convolutional Neural Networks for Sentence Classification
• On the Number of Linear Regions of Deep Neural Networks
• Certified Defenses against Adversarial Examples
• Formal Security Analysis of Neural Networks using Symbolic Intervals
• An approach to reachability analysis for feed-forward ReLU neural networks
• Reachable Set Computation and Safety Verification for Neural Networks with ReLU Activations

Cited by in corpus (10)

• How to Certify Machine Learning Based Safety-critical Systems? A Systematic Literature Review
• Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers
• Branch and Bound for Piecewise Linear Neural Network Verification
• Algorithms for Verifying Deep Neural Networks
• Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition
• Verification of Neural Network Control Policy Under Persistent Adversarial Perturbation
• Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees
• Contraction-Guided Adaptive Partitioning for Reachability Analysis of Neural Network Controlled Systems
• Constrained Feedforward Neural Network Training via Reachability Analysis
• Neural Network Branch-and-Bound for Neural Network Verification