--- res: bibo_abstract: - "We show that Neural ODEs, an emerging class of timecontinuous neural networks, can be verified by solving a set of global-optimization problems. For this purpose, we introduce Stochastic Lagrangian Reachability (SLR), an\r\nabstraction-based technique for constructing a tight Reachtube (an over-approximation of the set of reachable states\r\nover a given time-horizon), and provide stochastic guarantees in the form of confidence intervals for the Reachtube bounds. SLR inherently avoids the infamous wrapping effect (accumulation of over-approximation errors) by performing local optimization steps to expand safe regions instead of repeatedly forward-propagating them as is done by deterministic reachability methods. To enable fast local optimizations, we introduce a novel forward-mode adjoint sensitivity method to compute gradients without the need for backpropagation. Finally, we establish asymptotic and non-asymptotic convergence rates for SLR.@eng" bibo_authorlist: - foaf_Person: foaf_givenName: Sophie foaf_name: Grunbacher, Sophie foaf_surname: Grunbacher - foaf_Person: foaf_givenName: Ramin foaf_name: Hasani, Ramin foaf_surname: Hasani - foaf_Person: foaf_givenName: Mathias foaf_name: Lechner, Mathias foaf_surname: Lechner foaf_workInfoHomepage: http://www.librecat.org/personId=3DC22916-F248-11E8-B48F-1D18A9856A87 - foaf_Person: foaf_givenName: Jacek foaf_name: Cyranka, Jacek foaf_surname: Cyranka - foaf_Person: foaf_givenName: Scott A foaf_name: Smolka, Scott A foaf_surname: Smolka - foaf_Person: foaf_givenName: Radu foaf_name: Grosu, Radu foaf_surname: Grosu bibo_issue: '13' bibo_volume: 35 dct_date: 2021^xs_gYear dct_isPartOf: - http://id.crossref.org/issn/2159-5399 - http://id.crossref.org/issn/2374-3468 - http://id.crossref.org/issn/978-1-57735-866-4 dct_language: eng dct_publisher: AAAI Press@ dct_title: On the verification of neural ODEs with stochastic guarantees@ ...