A Unified View of Piecewise Linear Neural Network Verification

Abstract

The success of Deep Learning and its potential use in many safety-critical applications has motivated research on formal verification of Neural Network (NN) models. Despite the reputation of learned NN models to behave as black boxes and the theoretical hardness of proving their properties, researchers have been successful in verifying some classes of models by exploiting their piecewise linear structure and taking insights from formal methods such as Satisifiability Modulo Theory. These methods are however still far from scaling to realistic neural networks. To facilitate progress on this crucial area, we make two key contributions. First, we present a unified framework that encompasses previous methods. This analysis results in the identification of new methods that combine the strengths of multiple existing approaches, accomplishing a speedup of two orders of magnitude compared to the previous state of the art. Second, we propose a new data set of benchmarks which includes a collection of previously released testcases. We use the benchmark to provide the first experimental comparison of existing algorithms and identify the factors impacting the hardness of verification problems.

arXiv commentUpdated version of "Piecewise Linear Neural Network verification: A comparative study"

Cited by in corpus (52)

• Optimization Problems for Machine Learning: A Survey
• Maximizing information from chemical engineering data sets: Applications to machine learning
• Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers
• The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results
• Reliably-stabilizing piecewise-affine neural network controllers
• Robustness Verification of Tree-based Models
• Robustness Verification for Transformers
• DNNV: A Framework for Deep Neural Network Verification
• Certified Robustness for Top-k Predictions against Adversarial Perturbations via Randomized Smoothing
• Algorithms for Verifying Deep Neural Networks
• Efficient Exact Verification of Binarized Neural Networks
• The RFML Ecosystem: A Look at the Unique Challenges of Applying Deep Learning to Radio Frequency Applications
• Formal Verification of Decision-Tree Ensemble Model and Detection of its Violating-input-value Ranges
• Verifying Individual Fairness in Machine Learning Models
• Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition
• On the Impact of Applying Machine Learning in the Decision-Making of Self-Adaptive Systems
• Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming
• CAQL: Continuous Action Q-Learning
• Partition-based formulations for mixed-integer optimization of trained ReLU neural networks
• Strategy to Increase the Safety of a DNN-based Perception for HAD Systems
• Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees
• Lagrangian Decomposition for Neural Network Verification
• Refactoring Neural Networks for Verification
• Towards the Quantification of Safety Risks in Deep Neural Networks
• From Shallow to Deep Interactions Between Knowledge Representation, Reasoning and Machine Learning (Kay R. Amel group)
• Scaling the Convex Barrier with Sparse Dual Algorithms
• Almost Tight L0-norm Certified Robustness of Top-k Predictions against Adversarial Perturbations
• An efficient nonconvex reformulation of stagewise convex optimization problems
• Identification of Unexpected Decisions in Partially Observable Monte-Carlo Planning: a Rule-Based Approach
• Scalable Verification of Quantized Neural Networks (Technical Report)
• Sequential Randomized Smoothing for Adversarially Robust Speech Recognition
• Pruning and Slicing Neural Networks using Formal Verification
• DeepSearch: A Simple and Effective Blackbox Attack for Deep Neural Networks
• Certified Robustness of Graph Neural Networks against Adversarial Structural Perturbation
• Traversing the Local Polytopes of ReLU Neural Networks: A Unified Approach for Network Verification
• GoTube: Scalable Stochastic Verification of Continuous-Depth Models
• Neural Network Branch-and-Bound for Neural Network Verification
• Computing Linear Restrictions of Neural Networks
• A Review of Formal Methods applied to Machine Learning
• ANCER: Anisotropic Certification via Sample-wise Volume Maximization
• Insta-RS: Instance-wise Randomized Smoothing for Improved Robustness and Accuracy
• Fast and Stable Interval Bounds Propagation for Training Verifiably Robust Models
• Lyapunov-stable neural-network control
• Reachability Analysis of Convolutional Neural Networks
• Knowing When to Stop: Evaluation and Verification of Conformity to Output-size Specifications
• Worrisome Properties of Neural Network Controllers and Their Symbolic Representations
• Certifying Strategyproof Auction Networks
• Towards Safety Verification of Direct Perception Neural Networks
• Identifying and Exploiting Structures for Reliable Deep Learning
• Learning to Separate Clusters of Adversarial Representations for Robust Adversarial Detection
• Neural Network Repair with Reachability Analysis
• Reachability Is NP-Complete Even for the Simplest Neural Networks