TNODEV: Toolbox for Neural ODE Verification
Abstract
Neural ordinary differential equations (neural ODE) gained attention in safety critical settings such as continuous-time controllers for cyber-physical systems and classifiers integrated into automated decision pipelines, raising the question whether their behavior can be formally verified. Existing tools dedicated to neural ODE provide only a single reachability call without iterative input-set refinement, limiting the precision of their verdicts to whatever one reachability call can deliver. We present TNODEV, the first formal verifier for neural ODE that integrates a falsification checker, a fast interval-based reachability backend based on continuous-time mixed monotonicity, a verification and refinement loop with three input-set splitting heuristics, and a parallel scheduler in a single end-to-end pipeline. TNODEV supports safe-set inclusion verification on pure neural ODE, neural ODE in closed loop with a neural network controller and general neural ODE (GNODE), with the safe set specified either as an interval or as the half-space intersection induced by a target classification label. We evaluate TNODEV on a range of benchmarks across safe-set inclusion and classification-robustness properties, including a direct reachability comparison against NNV 2.0 and CORA and a verification comparison against NNV 2.0 on MNIST general neural ODE classifiers.
Related
- Complexity of Reachability and Verification Problems in Neural Networks
- Split Quaternion Toolbox: A MATLAB Implementation
- Quantum Fourier transform toolbox
- Scen-Opt: A Scenario Optimization Toolbox for Data-Driven Convex Programming
- TRISDUCTION: A Linguistically, Topologically, and Mathematically Sealed Verification Architecture · Triaxial Orthogonality, Twelve-Gate Closure, the Quaternionic Completion, the Root Axiom, and the Master Pre-Sealed Proposition Ledger
BibTeX
@misc{sayed2026tnodev,
title = {{TNODEV: Toolbox for Neural ODE Verification}},
author = {Abdelrahman Sayed Sayed and Pierre-Jean Meyer and Mohamed Ghazel},
howpublished = {Transactions on Machine Learning Research},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2606.16567},
eprint = {2606.16567},
archivePrefix = {arXiv},
url = {https://hal.science/hal-05661783v3},
note = {CC BY-NC-SA 4.0},
}
RIS
TY - UNPB
TI - TNODEV: Toolbox for Neural ODE Verification
AU - Abdelrahman Sayed Sayed
AU - Pierre-Jean Meyer
AU - Mohamed Ghazel
PY - 2026
DA - 2026/10/21
PB - Transactions on Machine Learning Research
DO - 10.48550/arxiv.2606.16567
UR - https://hal.science/hal-05661783v3
AB - Neural ordinary differential equations (neural ODE) gained attention in safety critical settings such as continuous-time controllers for cyber-physical systems and classifiers integrated into automated decision pipelines, raising the question whether their behavior can be formally verified. Existing tools dedicated to neural ODE provide only a single reachability call without iterative input-set refinement, limiting the precision of their verdicts to whatever one reachability call can deliver. We present TNODEV, the first formal verifier for neural ODE that integrates a falsification checker, a fast interval-based reachability backend based on continuous-time mixed monotonicity, a verification and refinement loop with three input-set splitting heuristics, and a parallel scheduler in a single end-to-end pipeline. TNODEV supports safe-set inclusion verification on pure neural ODE, neural ODE in closed loop with a neural network controller and general neural ODE (GNODE), with the safe set specified either as an interval or as the half-space intersection induced by a target classification label. We evaluate TNODEV on a range of benchmarks across safe-set inclusion and classification-robustness properties, including a direct reachability comparison against NNV 2.0 and CORA and a verification comparison against NNV 2.0 on MNIST general neural ODE classifiers.
SN - 2835-8856
ER -