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.

翻译：神经常微分方程（神经ODE）已开始出现在安全关键场景中，例如用于信息物理系统的连续时间控制器和集成到自动决策流水线中的分类器，这引发了一个问题：其行为是否能够被形式化验证？现有的专用于神经ODE的工具仅提供单一可达性调用，缺乏迭代输入集精化能力，导致其判决精度局限于单次可达性调用的结果。我们提出TNODEV，这是首个用于神经ODE的可靠形式化验证器，它将反例检测器、基于连续时间混合单调性的快速区间可达性后端、具备三种输入集分割启发式策略的验证与精化循环机制，以及并行调度器整合到单一端到端流水线中。TNODEV支持纯神经ODE的安全集包含验证、与神经网络控制器闭环的神经ODE以及通用神经ODE（GNODE），安全集可指定为区间或由目标分类标签导出的半空间交集。我们在涵盖安全集包含和分类鲁棒性属性的多个基准上评估TNODEV，包括与NNV 2.0和CORA的直接可达性比较，以及基于MNIST通用神经ODE分类器的与NNV2.0的验证性能对比。