GoTube: Scalable Stochastic Verification of Continuous-Depth Models
arXiv:2107.08467
Abstract
We introduce a new stochastic verification algorithm that formally quantifies the behavioral robustness of any time-continuous process formulated as a continuous-depth model. Our algorithm solves a set of global optimization (Go) problems over a given time horizon to construct a tight enclosure (Tube) of the set of all process executions starting from a ball of initial states. We call our algorithm GoTube. Through its construction, GoTube ensures that the bounding tube is conservative up to a desired probability and up to a desired tightness. GoTube is implemented in JAX and optimized to scale to complex continuous-depth neural network models. Compared to advanced reachability analysis tools for time-continuous neural networks, GoTube does not accumulate overapproximation errors between time steps and avoids the infamous wrapping effect inherent in symbolic techniques. We show that GoTube substantially outperforms state-of-the-art verification tools in terms of the size of the initial ball, speed, time-horizon, task completion, and scalability on a large set of experiments. GoTube is stable and sets the state-of-the-art in terms of its ability to scale to time horizons well beyond what has been previously possible.
arXiv commentAccepted to the Thirty-Sixth AAAI Conference on Artificial Intelligence (AAAI-22)
References in corpus (20)
- A Review of Uncertainty Quantification in Deep Learning: Techniques, Applications and Challenges
- Adversarial Risk and the Dangers of Evaluating Against Weak Attacks
- Efficient Neural Network Robustness Certification with General Activation Functions
- Evaluating Robustness of Neural Networks with Mixed Integer Programming
- On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models
- Scalable Gradients for Stochastic Differential Equations
- A Unified View of Piecewise Linear Neural Network Verification
- A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks
- CAPD::DynSys: a flexible C++ toolbox for rigorous numerical analysis of dynamical systems
- The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification
- Reachability Analysis of Deep Neural Networks with Provable Guarantees
- Causal Navigation by Continuous-time Neural Networks
- Hypersolvers: Toward Fast Continuous-Depth Models
- Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition
- Infinitely Deep Bayesian Neural Networks with Stochastic Differential Equations
- Deep Evidential Regression
- Non-Associative Learning Representation in the Nervous System of the Nematode Caenorhabditis elegans
- On The Verification of Neural ODEs with Stochastic Guarantees
- Sparse Flows: Pruning Continuous-depth Models
- Liquid Time-constant Networks