---
_id: '12510'
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."
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).
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Sophie A.
  full_name: Gruenbacher, Sophie A.
  last_name: Gruenbacher
- first_name: Mathias
  full_name: Lechner, Mathias
  id: 3DC22916-F248-11E8-B48F-1D18A9856A87
  last_name: Lechner
- first_name: Ramin
  full_name: Hasani, Ramin
  last_name: Hasani
- first_name: Daniela
  full_name: Rus, Daniela
  last_name: Rus
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000-0002-2985-7724
- first_name: Scott A.
  full_name: Smolka, Scott A.
  last_name: Smolka
- first_name: Radu
  full_name: Grosu, Radu
  last_name: Grosu
citation:
  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>'
  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>'
  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.'
  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.'
  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>.'
  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.
date_created: 2023-02-05T17:27:42Z
date_published: 2022-06-28T00:00:00Z
date_updated: 2023-09-26T10:46:59Z
day: '28'
department:
- _id: ToHe
doi: 10.1609/aaai.v36i6.20631
ec_funded: 1
external_id:
  arxiv:
  - '2107.08467'
intvolume: '        36'
issue: '6'
keyword:
- General Medicine
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/2107.08467
month: '06'
oa: 1
oa_version: Preprint
page: 6755-6764
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: Proceedings of the AAAI Conference on Artificial Intelligence
publication_identifier:
  eissn:
  - 2374-3468
  isbn:
  - '978577358350'
  issn:
  - 2159-5399
publication_status: published
publisher: Association for the Advancement of Artificial Intelligence
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'GoTube: Scalable statistical verification of continuous-depth models'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 36
year: '2022'
...