An approach to reachability analysis for feed-forward ReLU neural networks

Abstract

We study the reachability problem for systems implemented as feed-forward neural networks whose activation function is implemented via ReLU functions. We draw a correspondence between establishing whether some arbitrary output can ever be outputed by a neural system and linear problems characterising a neural system of interest. We present a methodology to solve cases of practical interest by means of a state-of-the-art linear programs solver. We evaluate the technique presented by discussing the experimental results obtained by analysing reachability properties for a number of benchmarks in the literature.

Cited by in corpus (60)

• Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness
• Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective
• Reachability Analysis of Neural Feedback Loops
• A Safety Framework for Critical Systems Utilising Deep Neural Networks
• RAB: Provable Robustness Against Backdoor Attacks
• The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification
• Robustness Verification of Quantum Classifiers
• Certified Robustness for Top-k Predictions against Adversarial Perturbations via Randomized Smoothing
• Multi-Label Classification Neural Networks with Hard Logical Constraints
• Randomized Smoothing of All Shapes and Sizes
• Efficient Exact Verification of Binarized Neural Networks
• Learning Security Classifiers with Verified Global Robustness Properties
• Exactly Computing the Local Lipschitz Constant of ReLU Networks
• AI Research Considerations for Human Existential Safety (ARCHES)
• A Survey on Verification and Validation, Testing and Evaluations of Neurosymbolic Artificial Intelligence
• Provable Certificates for Adversarial Examples: Fitting a Ball in the Union of Polytopes
• Towards Robust, Locally Linear Deep Networks
• Learning Lyapunov Functions for Piecewise Affine Systems with Neural Network Controllers
• Partition-based formulations for mixed-integer optimization of trained ReLU neural networks
• Orthogonalizing Convolutional Layers with the Cayley Transform
• Reachability Analysis for Feed-Forward Neural Networks using Face Lattices
• Specification-Guided Safety Verification for Feedforward Neural Networks
• On Certifying Non-uniform Bound against Adversarial Attacks
• Safe Control with Neural Network Dynamic Models
• Second-Order Provable Defenses against Adversarial Attacks
• Improving the Tightness of Convex Relaxation Bounds for Training Certifiably Robust Classifiers
• Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural Network Controllers via Semidefinite Programming
• Verification of Neural Networks: Enhancing Scalability through Pruning
• Verification of Binarized Neural Networks via Inter-Neuron Factoring
• Robustness Certificates Against Adversarial Examples for ReLU Networks
• Towards the Quantification of Safety Risks in Deep Neural Networks
• Learning Approximate Forward Reachable Sets Using Separating Kernels
• Data-Dependent Randomized Smoothing
• Almost Tight L0-norm Certified Robustness of Top-k Predictions against Adversarial Perturbations
• Enhancing Certified Robustness via Smoothed Weighted Ensembling
• Pruning and Slicing Neural Networks using Formal Verification
• Formal Verification of Robustness and Resilience of Learning-Enabled State Estimation Systems
• Reachable Set Estimation for Neural Network Control Systems: A Simulation-Guided Approach
• Debona: Decoupled Boundary Network Analysis for Tighter Bounds and Faster Adversarial Robustness Proofs
• A Mixed Integer Programming Approach for Verifying Properties of Binarized Neural Networks
• Accelerating Robustness Verification of Deep Neural Networks Guided by Target Labels
• Certifiable Robustness to Adversarial State Uncertainty in Deep Reinforcement Learning
• Constrained Discrete Black-Box Optimization using Mixed-Integer Programming
• ANCER: Anisotropic Certification via Sample-wise Volume Maximization
• Fast and Stable Interval Bounds Propagation for Training Verifiably Robust Models
• Evaluating the Safety of Deep Reinforcement Learning Models using Semi-Formal Verification
• Reachability Analysis of Convolutional Neural Networks
• Fast Falsification of Neural Networks using Property Directed Testing
• Certified Defense via Latent Space Randomized Smoothing with Orthogonal Encoders
• Insta-RS: Instance-wise Randomized Smoothing for Improved Robustness and Accuracy
• Continuous Safety Verification of Neural Networks
• ReLUSyn: Synthesizing Stealthy Attacks for Deep Neural Network Based Cyber-Physical Systems
• Run-Time Safety Monitoring of Neural-Network-Enabled Dynamical Systems
• BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks
• Network Moments: Extensions and Sparse-Smooth Attacks
• Work In Progress: Safety and Robustness Verification of Autoencoder-Based Regression Models using the NNV Tool
• Neural Network Repair with Reachability Analysis
• A Primer on Multi-Neuron Relaxation-based Adversarial Robustness Certification
• Learning to Separate Clusters of Adversarial Representations for Robust Adversarial Detection
• Regularized Training and Tight Certification for Randomized Smoothed Classifier with Provable Robustness