1: \begin{abstract}

2: We show that \emph{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 \emph{Stochastic Lagrangian Reachability} (SLR), an abstraction-based technique for constructing a tight \emph{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. 

3: 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. 

4: To enable fast local optimizations, we introduce a novel forward-mode adjoint sensitivity method to compute gradients without the need for backpropagation.

5: Finally, we establish asymptotic and non-asymptotic convergence rates for SLR.

6: \end{abstract}

7: