[{"main_file_link":[{"url":"https://arxiv.org/abs/2107.08467","open_access":"1"}],"quality_controlled":"1","month":"06","keyword":["General Medicine"],"language":[{"iso":"eng"}],"external_id":{"arxiv":["2107.08467"]},"volume":36,"oa_version":"Preprint","type":"journal_article","date_published":"2022-06-28T00:00:00Z","intvolume":"        36","status":"public","department":[{"_id":"ToHe"}],"project":[{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"},{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"}],"doi":"10.1609/aaai.v36i6.20631","scopus_import":"1","fulldoi":"https://doi.org/10.1609/aaai.v36i6.20631","acknowledgement":"SG is funded by the Austrian Science Fund (FWF) project number W1255-N23. ML and TH are supported in part by FWF under grant Z211-N23 (Wittgenstein Award) and the ERC-2020-AdG 101020093. SS is supported by NSF awards DCL-2040599, CCF-1918225, and CPS-1446832. RH and DR are partially supported by Boeing. RG is partially supported by Horizon-2020 ECSEL Project grant No. 783163 (iDev40).","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2023-02-05T17:27:42Z","publisher":"Association for the Advancement of Artificial Intelligence","article_type":"original","issue":"6","citation":{"short":"S.A. Gruenbacher, M. Lechner, R. Hasani, D. Rus, T.A. Henzinger, S.A. Smolka, R. Grosu, Proceedings of the AAAI Conference on Artificial Intelligence 36 (2022) 6755–6764.","chicago":"Gruenbacher, Sophie A., Mathias Lechner, Ramin Hasani, Daniela Rus, Thomas A Henzinger, Scott A. Smolka, and Radu Grosu. “GoTube: Scalable Statistical Verification of Continuous-Depth Models.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Association for the Advancement of Artificial Intelligence, 2022. <a href=\"https://doi.org/10.1609/aaai.v36i6.20631\">https://doi.org/10.1609/aaai.v36i6.20631</a>.","ieee":"S. A. Gruenbacher <i>et al.</i>, “GoTube: Scalable statistical verification of continuous-depth models,” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 36, no. 6. Association for the Advancement of Artificial Intelligence, pp. 6755–6764, 2022.","mla":"Gruenbacher, Sophie A., et al. “GoTube: Scalable Statistical Verification of Continuous-Depth Models.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 36, no. 6, Association for the Advancement of Artificial Intelligence, 2022, pp. 6755–64, doi:<a href=\"https://doi.org/10.1609/aaai.v36i6.20631\">10.1609/aaai.v36i6.20631</a>.","apa":"Gruenbacher, S. A., Lechner, M., Hasani, R., Rus, D., Henzinger, T. A., Smolka, S. A., &#38; Grosu, R. (2022). GoTube: Scalable statistical verification of continuous-depth models. <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v36i6.20631\">https://doi.org/10.1609/aaai.v36i6.20631</a>","ama":"Gruenbacher SA, Lechner M, Hasani R, et al. GoTube: Scalable statistical verification of continuous-depth models. <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. 2022;36(6):6755-6764. doi:<a href=\"https://doi.org/10.1609/aaai.v36i6.20631\">10.1609/aaai.v36i6.20631</a>","ista":"Gruenbacher SA, Lechner M, Hasani R, Rus D, Henzinger TA, Smolka SA, Grosu R. 2022. GoTube: Scalable statistical verification of continuous-depth models. Proceedings of the AAAI Conference on Artificial Intelligence. 36(6), 6755–6764."},"oa":1,"publication_identifier":{"isbn":["978577358350"],"eissn":["2374-3468"],"issn":["2159-5399"]},"_id":"12510","year":"2022","page":"6755-6764","abstract":[{"lang":"eng","text":"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.\r\n 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.\r\n 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":[{"first_name":"Sophie A.","full_name":"Gruenbacher, Sophie A.","last_name":"Gruenbacher"},{"first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","last_name":"Lechner","full_name":"Lechner, Mathias"},{"first_name":"Ramin","last_name":"Hasani","full_name":"Hasani, Ramin"},{"last_name":"Rus","full_name":"Rus, Daniela","first_name":"Daniela"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724"},{"first_name":"Scott A.","last_name":"Smolka","full_name":"Smolka, Scott A."},{"last_name":"Grosu","full_name":"Grosu, Radu","first_name":"Radu"}],"publication":"Proceedings of the AAAI Conference on Artificial Intelligence","title":"GoTube: Scalable statistical verification of continuous-depth models","arxiv":1,"date_updated":"2025-04-15T06:26:14Z","ec_funded":1,"article_processing_charge":"No","day":"28","publication_status":"published"}]