@article{Gruenbacher_Lechner_Hasani_Rus_Henzinger_Smolka_Grosu_2022, title={GoTube: Scalable Statistical Verification of Continuous-Depth Models}, volume={36}, url={https://ojs.aaai.org/index.php/AAAI/article/view/20631}, DOI={10.1609/aaai.v36i6.20631}, abstractNote={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.}, number={6}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Gruenbacher, Sophie A. and Lechner, Mathias and Hasani, Ramin and Rus, Daniela and Henzinger, Thomas A. and Smolka, Scott A. and Grosu, Radu}, year={2022}, month={Jun.}, pages={6755-6764} }