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+T^2 \log^2T)$ 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.

翻译：神经常微分方程（NODEs）是一种新颖的神经架构，基于通过推理过程中求解的带有学习动力学的初值问题构建。尽管被认为对对抗性扰动具有固有的鲁棒性，但近期研究表明它们易受强对抗攻击的影响，凸显了形式化保证的必要性。然而，尽管在前馈架构的鲁棒性验证方面取得了显著进展，高维NODEs的验证仍是一个开放问题。本文针对这一挑战，提出了GAINS——一种结合三大关键思想的NODEs分析框架：(i) 基于可变但离散时间步的新型ODE求解器，(ii) 求解器轨迹的高效图表示，及(iii) 作用于该图表示的创新抽象算法。这些进展通过将运行时间从难以处理的$O(\exp(d)+\exp(T))$降低至${O}(d+T^2 \log^2T)$（其中$d$为维度，$T$为积分时间），实现了高维NODEs的高效分析与认证训练。在计算机视觉（MNIST和FMNIST）及时间序列预测（PHYSIO-NET）问题的广泛评估中，我们验证了所提出的认证训练和验证方法的有效性。