@article{12510,
  abstract     = {We introduce a new statistical 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.},
  author       = {Gruenbacher, Sophie A. and Lechner, Mathias and Hasani, Ramin and Rus, Daniela and Henzinger, Thomas A and Smolka, Scott A. and Grosu, Radu},
  isbn         = {978577358350},
  issn         = {2374-3468},
  journal      = {Proceedings of the AAAI Conference on Artificial Intelligence},
  keywords     = {General Medicine},
  number       = {6},
  pages        = {6755--6764},
  publisher    = {Association for the Advancement of Artificial Intelligence},
  title        = {{GoTube: Scalable statistical verification of continuous-depth models}},
  doi          = {10.1609/aaai.v36i6.20631},
  volume       = {36},
  year         = {2022},
}