On the Verification of Neural ODEs with Stochastic Guarantees
Sophie Grunbacher, Ramin Hasani, Mathias Lechner, Jacek Cyranka, Scott A. Smolka, Radu Grosu
Abstract
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.
BibTeX
@inproceedings{aaai2021_ontheverificatio,
title = {On the Verification of Neural ODEs with Stochastic Guarantees},
author = {Sophie Grunbacher and Ramin Hasani and Mathias Lechner and Jacek Cyranka and Scott A. Smolka and Radu Grosu},
booktitle = {AAAI 2021},
year = {2021}
}