# Reachability Analysis of a General Class of Neural Ordinary Differential Equations

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

## Key facts

- Cited by 13 papers in the map (data through 14 Oct 2026).
- Builds on 24 of its 45 references that are in the map.
- First posted on arXiv 13 Jul 2022.

## Builds on (most cited first, 24 of 24)

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Neural Ordinary Differential Equations](https://mlsanity.com/paper/1806.07366/) (2018)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Neural Controlled Differential Equations for Irregular Time Series](https://mlsanity.com/paper/2005.08926/) (2020)
- [Augmented Neural ODEs](https://mlsanity.com/paper/1904.01681/) (2019)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Dissecting Neural ODEs](https://mlsanity.com/paper/2002.08071/) (2020)
- [Neural Rough Differential Equations for Long Time Series](https://mlsanity.com/paper/2009.08295/) (2020)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Reachability Analysis of Deep Neural Networks with Provable Guarantees](https://mlsanity.com/paper/1805.02242/) (2018)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [ANODE: Unconditionally Accurate Memory-Efficient Gradients for Neural ODEs](https://mlsanity.com/paper/1902.10298/) (2019)
- [On Robustness of Neural Ordinary Differential Equations](https://mlsanity.com/paper/1910.05513/) (2019)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [On Second Order Behaviour in Augmented Neural ODEs](https://mlsanity.com/paper/2006.07220/) (2020)
- [JuliaReach: a Toolbox for Set-Based Reachability](https://mlsanity.com/paper/1901.10736/) (2019)
- [ReachNN: Reachability Analysis of Neural-Network Controlled Systems](https://mlsanity.com/paper/1906.10654/) (2019)
- [On The Verification of Neural ODEs with Stochastic Guarantees](https://mlsanity.com/paper/2012.08863/) (2020)
- [Case Study: Verifying the Safety of an Autonomous Racing Car with a Neural Network Controller](https://mlsanity.com/paper/1910.11309/) (2019)
- [GoTube: Scalable Stochastic Verification of Continuous-Depth Models](https://mlsanity.com/paper/2107.08467/) (2021)
- [Lagrangian Reachtubes: The Next Generation](https://mlsanity.com/paper/2012.07458/) (2020)
- [Reachability of Black-Box Nonlinear Systems after Koopman Operator Linearization](https://mlsanity.com/paper/2105.00886/) (2021)

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

- [Neural Abstractions](https://mlsanity.com/paper/2301.11683/) (2023)
- [ModelVerification.jl: a Comprehensive Toolbox for Formally Verifying Deep Neural Networks](https://mlsanity.com/paper/2407.01639/) (2024)
- [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)
- [Value Approximation for Two-Player General-Sum Differential Games with State Constraints](https://mlsanity.com/paper/2311.16520/) (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)
- [Deep active learning for nonlinear system identification](https://mlsanity.com/paper/2302.12667/) (2023)
- [Verifying Safety of Neural Networks from Topological Perspectives](https://mlsanity.com/paper/2306.15403/) (2023)
- [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)
- [Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features](https://mlsanity.com/paper/2609.30079/) (2026)

## Abstract (arXiv)

Continuous deep learning models, referred to as Neural Ordinary Differential Equations (Neural ODEs), have received considerable attention over the last several years. Despite their burgeoning impact, there is a lack of formal analysis techniques for these systems. In this paper, we consider a general class of neural ODEs with varying architectures and layers, and introduce a novel reachability framework that allows for the formal analysis of their behavior. The methods developed for the reachability analysis of neural ODEs are implemented in a new tool called NNVODE. Specifically, our work extends an existing neural network verification tool to support neural ODEs. We demonstrate the capabilities and efficacy of our methods through the analysis of a set of benchmarks that include neural ODEs used for classification, and in control and dynamical systems, including an evaluation of the efficacy and capabilities of our approach with respect to existing software tools within the continuous-time systems reachability literature, when it is possible to do so.