TNODEV：首个神经 ODE 形式化验证工具箱发布

View PDF HTML (experimental)

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.

Comments:	44 pages, 10 figures, Accepted in TMLR 2026. Code available at this https URL
Subjects:	Artificial Intelligence (cs.AI); Machine Learning (cs.LG); Systems and Control (eess.SY); Dynamical Systems (math.DS)
Cite as:	arXiv:2606.16567 [cs.AI]
	(or arXiv:2606.16567v3 [cs.AI] for this version)
	https://doi.org/10.48550/arXiv.2606.16567 arXiv-issued DOI via DataCite

Submission history

From: Abdelrahman Sayed Sayed [view email]
[v1] Mon, 15 Jun 2026 11:09:06 UTC (1,582 KB)
[v2] Thu, 9 Jul 2026 15:36:14 UTC (1,582 KB)
[v3] Wed, 21 Oct 2026 12:19:35 UTC (2,006 KB)