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 (34)

• Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness
• Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective
• Certified Robustness for Top-k Predictions against Adversarial Perturbations via Randomized Smoothing
• 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
• 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
• 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 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
• Reachable Set Estimation for Neural Network Control Systems: A Simulation-Guided Approach
• A Mixed Integer Programming Approach for Verifying Properties of Binarized Neural Networks
• Accelerating Robustness Verification of Deep Neural Networks Guided by Target Labels
• Certified Defense via Latent Space Randomized Smoothing with Orthogonal Encoders
• Fast Falsification of Neural Networks using Property Directed Testing
• Fast and Stable Interval Bounds Propagation for Training Verifiably Robust Models
• Reachability Analysis of Convolutional Neural Networks
• Run-Time Safety Monitoring of Neural-Network-Enabled Dynamical Systems
• Work In Progress: Safety and Robustness Verification of Autoencoder-Based Regression Models using the NNV Tool
• BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks
• Network Moments: Extensions and Sparse-Smooth Attacks
• ReLUSyn: Synthesizing Stealthy Attacks for Deep Neural Network Based Cyber-Physical Systems
• Regularized Training and Tight Certification for Randomized Smoothed Classifier with Provable Robustness
• A Primer on Multi-Neuron Relaxation-based Adversarial Robustness Certification
• Learning to Separate Clusters of Adversarial Representations for Robust Adversarial Detection
• Neural Network Repair with Reachability Analysis