TNODEV: Toolbox for Neural ODE Verification
2026-06-15 • Artificial Intelligence
Artificial IntelligenceMachine Learning
AI summaryⓘ
The authors developed TNODEV, a tool that can check if neural ordinary differential equations (neural ODEs) behave safely and correctly. Unlike previous tools, TNODEV repeatedly refines input data and uses several methods to more accurately verify the system's safety. It works with different types of neural ODEs and can handle safety and classification tasks, such as ensuring a system stays within a safe range or classifies data correctly. They tested TNODEV on various benchmarks and compared it to other verification tools, showing its usefulness in safety-critical settings.
neural ordinary differential equationsformal verificationreachability analysisinterval methodsmixed monotonicityinput set refinementsafety verificationclassification robustnessneural network controllerautomated verification tools
Authors
Abdelrahman Sayed Sayed, Pierre-Jean Meyer, Mohamed Ghazel
Abstract
Neural ordinary differential equations (neural ODE) have started to appear in safety critical settings such as continuous-time controllers for cyber-physical systems and classifiers integrated into automated decision pipelines, raising the question of 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 sound 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 NNV2.0 on MNIST general neural ODE classifiers.