TY - JOUR AU - Grunbacher, Sophie AU - Hasani, Ramin AU - Lechner, Mathias AU - Cyranka, Jacek AU - Smolka, Scott A. AU - Grosu, Radu PY - 2021/05/18 Y2 - 2024/03/28 TI - On the Verification of Neural ODEs with Stochastic Guarantees JF - Proceedings of the AAAI Conference on Artificial Intelligence JA - AAAI VL - 35 IS - 13 SE - AAAI Technical Track on Philosophy and Ethics of AI DO - 10.1609/aaai.v35i13.17372 UR - https://ojs.aaai.org/index.php/AAAI/article/view/17372 SP - 11525-11535 AB - We show that Neural ODEs, an emerging class of time-continuous neural networks, can be verified by solving a set of global-optimization problems. For this purpose, we introduce Stochastic Lagrangian Reachability (SLR), an abstraction-based technique for constructing a tight Reachtube (an over-approximation of the set of reachable states over 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. ER -