GoTube: Scalable Statistical Verification of Continuous-Depth Models


  • Sophie A. Gruenbacher TU Wien
  • Mathias Lechner IST Austria
  • Ramin Hasani MIT
  • Daniela Rus MIT CSAIL
  • Thomas A. Henzinger IST Austria
  • Scott A. Smolka Stony Brook University
  • Radu Grosu TU Wien



Machine Learning (ML)


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.




How to Cite

Gruenbacher, S. A., Lechner, M., Hasani, R., Rus, D., Henzinger, T. A., Smolka, S. A., & Grosu, R. (2022). GoTube: Scalable Statistical Verification of Continuous-Depth Models. Proceedings of the AAAI Conference on Artificial Intelligence, 36(6), 6755-6764.



AAAI Technical Track on Machine Learning I