# On The Verification of Neural ODEs with Stochastic Guarantees

arXiv: https://arxiv.org/abs/2012.08863 · HTML: https://mlsanity.com/paper/2012.08863/

## Key facts

- Cited by 24 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 16 Dec 2020.

## Built on by (most cited first, 24 of 24)

- [Liquid Structural State-Space Models](https://mlsanity.com/paper/2209.12951/) (2022)
- [Closed-form Continuous-time Neural Models](https://mlsanity.com/paper/2106.13898/) (2021)
- [Dataset Distillation with Convexified Implicit Gradients](https://mlsanity.com/paper/2302.06755/) (2023)
- [Causal Navigation by Continuous-time Neural Networks](https://mlsanity.com/paper/2106.08314/) (2021)
- [Adversarial Training is Not Ready for Robot Learning](https://mlsanity.com/paper/2103.08187/) (2021)
- [Evolution of Neural Tangent Kernels under Benign and Adversarial Training](https://mlsanity.com/paper/2210.12030/) (2022)
- [Reachability Analysis of a General Class of Neural Ordinary Differential Equations](https://mlsanity.com/paper/2207.06531/) (2022)
- [GoTube: Scalable Stochastic Verification of Continuous-Depth Models](https://mlsanity.com/paper/2107.08467/) (2021)
- [BarrierNet: A Safety-Guaranteed Layer for Neural Networks](https://mlsanity.com/paper/2111.11277/) (2021)
- [On the Forward Invariance of Neural ODEs](https://mlsanity.com/paper/2210.04763/) (2022)
- [Neural Abstractions](https://mlsanity.com/paper/2301.11683/) (2023)
- [Differentiable Control Barrier Functions for Vision-based End-to-End Autonomous Driving](https://mlsanity.com/paper/2203.02401/) (2022)
- [Safety Verification for Neural Networks Based on Set-boundary Analysis](https://mlsanity.com/paper/2210.04175/) (2022)
- [FI-ODE: Certifiably Robust Forward Invariance in Neural ODEs](https://mlsanity.com/paper/2210.16940/) (2022)
- [Efficient Certified Training and Robustness Verification of Neural ODEs](https://mlsanity.com/paper/2303.05246/) (2023)
- [Bridging Neural ODE and ResNet: A Formal Error Bound for Safety Verification](https://mlsanity.com/paper/2506.03227/) (2025)
- [Mixed Monotonicity Reachability Analysis of Neural ODE: A Trade-Off Between Tightness and Efficiency](https://mlsanity.com/paper/2510.17859/) (2025)
- [Interpreting Neural Policies with Disentangled Tree Representations](https://mlsanity.com/paper/2210.06650/) (2022)
- [Verifying Safety of Neural Networks from Topological Perspectives](https://mlsanity.com/paper/2306.15403/) (2023)
- [LEVIS: Large Exact Verifiable Input Spaces for Neural Networks](https://mlsanity.com/paper/2408.08824/) (2024)
- [TNODEV: Toolbox for Neural ODE Verification](https://mlsanity.com/paper/2606.16567/) (2026)
- [On the Trade-off Between Efficiency and Precision of Neural Abstraction](https://mlsanity.com/paper/2307.15546/) (2023)
- [Robustness Analysis of Continuous-Depth Models with Lagrangian Techniques](https://mlsanity.com/paper/2308.12192/) (2023)
- [Stable Robot Motions on Manifolds: Learning Lyapunov-Constrained Neural Manifold ODEs](https://mlsanity.com/paper/2510.05707/) (2025)

## Abstract (arXiv)

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.