# GoTube: Scalable Stochastic Verification of Continuous-Depth Models

arXiv: https://arxiv.org/abs/2107.08467 · HTML: https://mlsanity.com/paper/2107.08467/

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- Builds on 37 of its 90 references that are in the map.
- First posted on arXiv 18 Jul 2021.

## Builds on (most cited first, 30 of 37)

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Neural Ordinary Differential Equations](https://mlsanity.com/paper/1806.07366/) (2018)
- [Obfuscated Gradients Give a False Sense of Security: Circumventing Defenses to Adversarial Examples](https://mlsanity.com/paper/1802.00420/) (2018)
- [A Review of Uncertainty Quantification in Deep Learning: Techniques, Applications and Challenges](https://mlsanity.com/paper/2011.06225/) (2020)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networks](https://mlsanity.com/paper/1906.04893/) (2019)
- [Scalable Gradients for Stochastic Differential Equations](https://mlsanity.com/paper/2001.01328/) (2020)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Adversarial Risk and the Dangers of Evaluating Against Weak Attacks](https://mlsanity.com/paper/1802.05666/) (2018)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [Liquid Time-constant Networks](https://mlsanity.com/paper/2006.04439/) (2020)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks](https://mlsanity.com/paper/1902.08722/) (2019)
- [Learning Long-Term Dependencies in Irregularly-Sampled Time Series](https://mlsanity.com/paper/2006.04418/) (2020)
- [The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification](https://mlsanity.com/paper/2006.14076/) (2020)
- [Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition](https://mlsanity.com/paper/2104.06718/) (2021)
- [Global optimization of Lipschitz functions](https://mlsanity.com/paper/1703.02628/) (2017)
- [Infinitely Deep Bayesian Neural Networks with Stochastic Differential Equations](https://mlsanity.com/paper/2102.06559/) (2021)
- [Lagrangian Decomposition for Neural Network Verification](https://mlsanity.com/paper/2002.10410/) (2020)
- [Hypersolvers: Toward Fast Continuous-Depth Models](https://mlsanity.com/paper/2007.09601/) (2020)
- [Scalable Verification of Quantized Neural Networks (Technical Report)](https://mlsanity.com/paper/2012.08185/) (2020)
- [On The Verification of Neural ODEs with Stochastic Guarantees](https://mlsanity.com/paper/2012.08863/) (2020)
- [Causal Navigation by Continuous-time Neural Networks](https://mlsanity.com/paper/2106.08314/) (2021)
- [Adversarial Training is Not Ready for Robot Learning](https://mlsanity.com/paper/2103.08187/) (2021)
- [LipBaB: Computing exact Lipschitz constant of ReLU networks](https://mlsanity.com/paper/2105.05495/) (2021)
- [On-Off Center-Surround Receptive Fields for Accurate and Robust Image Classification](https://mlsanity.com/paper/2106.07091/) (2021)
- [TIRA: Toolbox for Interval Reachability Analysis](https://mlsanity.com/paper/1902.05204/) (2019)

## Built on by (most cited first, 12 of 12)

- [Stability Verification in Stochastic Control Systems via Neural Network Supermartingales](https://mlsanity.com/paper/2112.09495/) (2021)
- [Reachability Analysis of a General Class of Neural Ordinary Differential Equations](https://mlsanity.com/paper/2207.06531/) (2022)
- [BarrierNet: A Safety-Guaranteed Layer for Neural Networks](https://mlsanity.com/paper/2111.11277/) (2021)
- [A Simple and Efficient Sampling-based Algorithm for General Reachability Analysis](https://mlsanity.com/paper/2112.05745/) (2021)
- [On the Forward Invariance of Neural ODEs](https://mlsanity.com/paper/2210.04763/) (2022)
- [Neural Abstractions](https://mlsanity.com/paper/2301.11683/) (2023)
- [Differentiable Control Barrier Functions for Vision-based End-to-End Autonomous Driving](https://mlsanity.com/paper/2203.02401/) (2022)
- [Safety Verification for Neural Networks Based on Set-boundary Analysis](https://mlsanity.com/paper/2210.04175/) (2022)
- [Verifying Safety of Neural Networks from Topological Perspectives](https://mlsanity.com/paper/2306.15403/) (2023)
- [TNODEV: Toolbox for Neural ODE Verification](https://mlsanity.com/paper/2606.16567/) (2026)
- [On the Trade-off Between Efficiency and Precision of Neural Abstraction](https://mlsanity.com/paper/2307.15546/) (2023)
- [Robustness Analysis of Continuous-Depth Models with Lagrangian Techniques](https://mlsanity.com/paper/2308.12192/) (2023)

## Abstract (arXiv)

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.