# Efficient Certified Training and Robustness Verification of Neural ODEs

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 34 of its 58 references that are in the map.
- First posted on arXiv 9 Mar 2023.

## Builds on (most cited first, 30 of 34)

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Fashion-MNIST: a Novel Image Dataset for Benchmarking Machine Learning Algorithms](https://mlsanity.com/paper/1708.07747/) (2017)
- [Auto-Encoding Variational Bayes](https://mlsanity.com/paper/1312.6114/) (2013)
- [Neural Ordinary Differential Equations](https://mlsanity.com/paper/1806.07366/) (2018)
- [On the Properties of Neural Machine Translation: Encoder-Decoder Approaches](https://mlsanity.com/paper/1409.1259/) (2014)
- [Obfuscated Gradients Give a False Sense of Security: Circumventing Defenses to Adversarial Examples](https://mlsanity.com/paper/1802.00420/) (2018)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Evasion Attacks against Machine Learning at Test Time](https://mlsanity.com/paper/1708.06131/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [GRU-ODE-Bayes: Continuous modeling of sporadically-observed time series](https://mlsanity.com/paper/1905.12374/) (2019)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Towards Stable and Efficient Training of Verifiably Robust Neural Networks](https://mlsanity.com/paper/1906.06316/) (2019)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Latent ODEs for Irregularly-Sampled Time Series](https://mlsanity.com/paper/1907.03907/) (2019)
- [Semidefinite relaxations for certifying robustness to adversarial examples](https://mlsanity.com/paper/1811.01057/) (2018)
- [Torchattacks: A PyTorch Repository for Adversarial Attacks](https://mlsanity.com/paper/2010.01950/) (2020)
- [Monotone operator equilibrium networks](https://mlsanity.com/paper/2006.08591/) (2020)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [Stable Neural ODE with Lyapunov-Stable Equilibrium Points for Defending Against Adversarial Attacks](https://mlsanity.com/paper/2110.12976/) (2021)
- [On Robustness of Neural Ordinary Differential Equations](https://mlsanity.com/paper/1910.05513/) (2019)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming](https://mlsanity.com/paper/2010.11645/) (2020)
- [Certified Training: Small Boxes are All You Need](https://mlsanity.com/paper/2210.04871/) (2022)
- [LyaNet: A Lyapunov Framework for Training Neural ODEs](https://mlsanity.com/paper/2202.02526/) (2022)
- [On The Verification of Neural ODEs with Stochastic Guarantees](https://mlsanity.com/paper/2012.08863/) (2020)
- [Adversarial Robustness of Stabilized NeuralODEs Might be from Obfuscated Gradients](https://mlsanity.com/paper/2009.13145/) (2020)

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

- [Adversarially Robust Out-of-Distribution Detection Using Lyapunov-Stabilized Embeddings](https://mlsanity.com/paper/2410.10744/) (2024)
- [Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exits](https://mlsanity.com/paper/2512.20755/) (2025)
- [Modeling Neural Networks with Privacy Using Neural Stochastic Differential Equations](https://mlsanity.com/paper/2501.06686/) (2025)

## Abstract (arXiv)

Neural Ordinary Differential Equations (NODEs) are a novel neural architecture, built around initial value problems with learned dynamics which are solved during inference. Thought to be inherently more robust against adversarial perturbations, they were recently shown to be vulnerable to strong adversarial attacks, highlighting the need for formal guarantees. However, despite significant progress in robustness verification for standard feed-forward architectures, the verification of high dimensional NODEs remains an open problem. In this work, we address this challenge and propose GAINS, an analysis framework for NODEs combining three key ideas: (i) a novel class of ODE solvers, based on variable but discrete time steps, (ii) an efficient graph representation of solver trajectories, and (iii) a novel abstraction algorithm operating on this graph representation. Together, these advances enable the efficient analysis and certified training of high-dimensional NODEs, by reducing the runtime from an intractable O(exp(d)+exp(T)) to O(d+T2 log2T) in the dimensionality d and integration time T. In an extensive evaluation on computer vision (MNIST and FMNIST) and time-series forecasting (PHYSIO-NET) problems, we demonstrate the effectiveness of both our certified training and verification methods.