Efficient Certified Training and Robustness Verification of Neural ODEs
Authors: Mustafa Zeqiri
Mark Niklas Mueller
Marc Fischer
Martin Vechev
Venue: ICLR 2023 poster (2023)
Keywords: Neural ODEs
Adversarial Robustness
Certified Robustness
Robustness Verification
Certified Training

Abstract: 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 $\mathcal{O}(\exp(d)+\exp(T))$ to $\mathcal{O}(d+T^2\log^2T)$ in the dimensionality $d$ and integration time $T$.  In an extensive evaluation on computer vision (MNIST and Fashion-MNIST) and time-series forecasting (Physio-Net) problems, we demonstrate the effectiveness of both our certified training and verification methods.

Published as a conference paper at ICLR 2023
EFFICIENT CERTIFIED TRAINING AND ROBUSTNESS VERIFICATION OF NEURAL ODES
Mustafa Zeqiri, Mark Niklas Müller, Mare Fischer & Martin Vechev
Department of Computer Science ETH Zurich, Switzerland mzeqiri@ethz.c ch, (mark. muelle mark.. fischer, martin vechev)@inf wwtgiin..ehz.....
ABSTRACT
Neural Ordinary Differential Equations (NODEs) are 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 strong adversarial attacks, high- lighting the need for formal guarantees. However, despite significant progress 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) 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 intractable (exx(d) + exp(T)) Odd + 7 log2 T)) in the dimensionality d and integration time T. In an exten- sive evaluation on computer vision (MNIST and FMNIST) and time-series fore- casting (PHysIO-Ne) -ET) problems, demonstrate the effectiveness of both certified training and verification methods.
INTRODUCTION
As deep learning-enabled enabled systems are increasingly deployed in safety-critict domains, developing neural architectures and specialized training methods that increase their robustness against adversar- ial examples (Szegedy et al., 2014 Biggio et al. 2013) imperceptible input perturbations, causing model failures is more important than ever. standard neural networks suffer from severely reduced accuracies when trained for robustness, novel architectures with inherent robustness prop-
erties have recently received increasing attention (Winston & Kolter 2020 Müller et al. 2021).
Neural Ordinary Differential Equations One particularly interesting such architecture ral ODEs (NODEs) (Chen et al. 2018). Built around solving initial value problems with learned dynamics, they are uniquely suited time-series-based problems (Rubanova et al. 2019 Brouwer et al. 2019) but have also been successfully applied to image classification (Chen et al. 2018). More importantly, NODEs have been observed exhibit inherent robustness properties against adversarial attacks Yan et al. 2020 Kang et al. 2021 Rodriguez et al. 2022 Zakwan et al. (022). However, recently Huang et al. (2020) found that this robustness is greatly diminished against stronger attacks. They suggest that adaptive ODE solvers, used to solve the underlying initial value problems, cause gradient obfuscation (Athalye et al. (2018). which, in turn, causes weaker adversarial attacks fail. This highlights the need for formal robustness guarantees to rigorously evaluate the true robustness of model or architecture.
Robustness Verification For standard neural networks, many robustness verification methods have been proposed (Katz et al. 2017 Tjeng et al. 2019 Singh et al. 2018b Raghunathan et al, 2018 Wang al. 2021 Ferrari al. 2022). One particularly successful class of such methods (Gehr et al.) 2018; Singh et al.) 22019) Zhang et al. 2018) propagates convex shapes through the neural network that capture the reachable sets of every neuron's values and uses them check

---

Published as a conference paper at ICLR 2023
Standard NODE ($
So go(=(t), t)dt
Learned Dynamics
Adaptive ODE Solver
Standard Inference
This Work
So go(z(t),t)dt
Learning Provable Dynamics 5$5
Controlled Adaptive ODE Solver (CAS; $4
NODE Verifier: GAINS ($5
Inference
W. Guarantees
Figure I: Overview of NODE inference in both the standard and certified (our) setting. In both settings ODE solvers are used evaluate learned dynamics. introduce controlled adaptive solvers (CAS) modifi- cation of adaptive solvers, which reduce the reachable time/step-size pairs from continuous area to discrete points. This enables GAINS to compute worst-case bounds NODE outputs given small input ranges, allow- ing both inferenee with guarantees and provable training. For example, in the time-series forecasting setting shown on the right, standard NODE inference predicts the blue points given the conerete red inputs. In contrast GAINS computes all possible outputs (blue error bars), for inputs in the red input ranges.
whether given robustness property holds. Unfortunately, NODEs as the underlying adaptive solvers yield a continuous range of possible step-sizes (illustrated in the top panel of Fig. [ which existing analysis techniques
of these methods be applied to
not handle. First works towards NODE verification (Lopez et al., (022) have avoided this issue by disregarding the solver behavior and analyzing only the underlying NODE dynamics in extremely low dimensional settings. How- ever, both scaling to nigh-dimensional NODE architectures and taking the effect of ODE solvers into account remain open problems preventing NODE robustness verification.
This Work We tackle both of these problems, thereby enabling the systematic verification and study of NODE robustness (illustrated in Fig. [ as follows: (i) We introduce novel class ODE solvers, based on the key insight that minimal impact on solver efficiency, while obtaining a finite number of time/step-size trajectories from the initial to final state (see the second column in Fig, Dp. We call these Controlled Adaptive ODE Solvers (CAS). Unfortunately. CAS solvers still yield exponentially many trajectories in the integration time. (ii) We, therefore, introduce efficient graph representation, allowing trajectories to be merged, reducing their number to quadratically many. (iii) We develop a novel algorithm for the popular DEEPPOLY convex relaxation (Singh al. 2019a). effective for standard neural network verification, that enables the efficient application of DEEPPOLY to the trajectory graph by handling trajectory splitting linear instead of exponential time. Combining these core ideas, we propose G novel framework for certified training and verification of NODEs that leverages key algorithmic advances to achieve polynomial runtimes and allows us to faithfully assess the robustness of NODEs.
restrict step-sizes to exponentially spaced grid with
Main Contributions Our main contributions are:
novel class of ODE solvers, CAS solvers, retaining the efficiency of adaptive step size solvers while enabling verification ($4)
An efficient linear bound propagation based framework, GAINS, which leverages CAS to enable the efficient training and verification of NODES (55).
An extensive empirical evaluation demonstrating the effectiveness of method in abla- tion studies and on image classification and time-series problems (%)).
Graph hased Abstract Interpretation for NODEs
2

---

Published as a conference paper at ICLR 2023
2 ADVERSARIAL ROBUSTNESS
In this section, we discuss the necessary background relating to adversarial robustness.
Adversarial Robustness We consider both classification and regression models fo: Rd + R with parameters 0 that, given an imput æ E X C R predict numerical values y := fæx) inter- preted as class confidences or predictions of the regression values, respectively. In the classification setting, we call f adversarially robust on an l--norm ball 8 (1)) of radius 6p. if it predicts target class for all perturbed inputs x' E B37 (z:). More formally, we define adversarial robustness as: arg max h(a'); 1, Var E B3 ==
(a' E X ||
a''lp S pp)
(1)
In the regression setting, we evaluate v- p-d-robustness by checking whether the worst-case mean absolute error MA (a)) for x' E 187 (a:) is linearly bounded by the original input's MAE(x)): MAEn (2)) < (1+ MAE(Ø) + 5, with MAE = max MAE(x'). (2)
of E'E (2)
Adversarial Attacks aim to disprove robustness properties by finding a concrete counterexample x.. A particularly successful such method is the PGD attack (Madry et al. 2018), which computes æ' by initializing o'g uniformly at random in 8p" (a:) and then updating it in the direction of the gradient sign of an auxiliary loss function L, using N projected gradient descent steps:
x t 87 (=))²², xi, + sign( Vvg ae ((fo (alff((')))))) ()),
(3)
where ITg denotes projection S and a the step size. We say input is empirically robust if no counterexample x' is found.
Neural Network Verification aims decide whether the robustness properties defined above hold. To this end, wide range of methods has been proposed, many relying on bound propagation, i.e., determining lower and upper bound for each neu- ron I < < u. or in vector notation for the whole layer 1 < x S u. Here, we discuss two ways of obtaining such bounds: First, Interval Bound Propa- gation (Gehr et al. 2018; Mirman et al. 2018) where and u are constants, bounding the reachable values of neurons. For details, we refer to Gowal et al. (2018). Second, Linear Bound Propagation
U -.- La)
y = max x0
y 2 Ar
Mix
Figure 2: Linear bounds for ReLU(x).
MMrmmn
(Singh et al. 2019a; Zhang et al. 2018 where every layer's neurons I; are lower- and upper- bounded depending only on the previous layer's neurons:
A, x,-111 + C, =: 4 xi, x; A/
x;
(4)
Given these linear constraints, can recursively substitute x,-1 with its linear bounds in terms of æ;-2 until we have obtained bounds depending only on the input zy- This allows us to compute concrete bounds I and any linear expression
network neurons.
For a linear layer x, W + by we simply have A = W, and ct = b, For a ReLU function a; ReLLU(Z-1)),
first compute the input bounds 1 S æ;-1 S. u. the ReLU is stably inactive, ie. u S 0, we can replace it with the zero-function. can replace it with the identity-function If the ReLU is unstable, i.e., < 0 < u, we compute a convex relaxation with parameter À as illustrated in Fig. Using this backsubstitution approach, we can now lower bound the difference Yt - y/, Vi * to determine whether the target class logit yo is always greater than all other logits in the classification setting and similarly bound the elementwise output range in the regression setting-
the ReLU is stably active, i.e. 2 O, we In both cases, we can use the bounding for linear layer.
Provable Training Special training is necessary to obtain networks that are provably robust, Con- sidering the classification setting with data distribution (x, t) ~ D. Provable training now aims to choose the network parametrization 0 that minimizes the expected worst case loss:
P arg min ED
max EE
LCE (e()) with Leely, t) = In (1+ Σ exp(y Sap(y-90)) exp())-y))). (5)
(2)
ifft
The inner maximization problem is generally intractable, but can be upper bounded using bound
propagation (Mirman et al. 2018 Gowal al. 2018 Zhang al. 2020 Müller et al. 2023
3

---

Published as a conference paper at ICLR 2023
3 NEURAL ORDINARY DIFFERENTIAL EQUATIONS
In this section, we discuss the necessary background relating to NODEs Chen et al. 2018).
Neural Ordinary Differential Equations are built around an initial value problem (IVP), defined by an input state =0) = Zu and a neural network ge defining the dynamics of an ordinary differential equation (ODE) V v==(t) (t) (o .t.. t). We obtain its solution (T) at time T as
zTT) = z()) + I." go(z(1), ()dt.
(6)
Generally, 2 can either be the raw input come from encoder neural network. For both clas- sification and regression tasks, we output y = (Tema)))) for an input 2 and a predefined Tends where f is additional decoder, usually a linear layer.
Time series forecasting is a special case of the regression setting where the input is time-series atf { f=1 defined as sequence of L entries, each consisting of data point æ; E R and an observation time tj. We aim to predict the value of the last observed data point æt, using only the first L' L data points as input. To this end, employ the so-called latent-ODE architecture, where a recurrent encoder network reads the data sequence {(x,,ty) t,) and outputs the initial state zo for decoder NODE that is then integrated up to the desired time-step Tend = 4 before its output 2t, is passed through a linear layer f. For further details, we refer to App.
ODE Solvers are employed to approximate Eq. (6). as analytical solutions often don't I exist. These solvers split the integration interval [0. into sub-intervals, for which the integral is numerically approximated by evaluating ge at multiple points and taking their weighted average. We let [( denote the trajectory of an ODE solver, which we define as the sequence of tuples (1, h) with time t and step-size h.
ODE solvers are characterized by their order p. indicating how quickly approximation errors dimin- ish the step size is reduced (Shampine] 2005). We distinguish between fixed (h constant) (Euler 1792 Runge (895) and adaptive solvers (h varies; discussed below) (Dormand Prince 1980 Bogacki & Shampine| 1989). Note that for adaptive solvers, the trajectory depends on the exact input. Huang et al. (2020 found that the supposedly inherent robustness of NODEs to adversarial attacks (Kagg et al. 2021 Yan et al., 2020) is only observed for adaptive ODE solvers and may stem, partially or entirely, from gradient obfuscation (Athalye et al. 2018) caused by the solver.
Adaptive ODE Solvers Adaptive step-size solvers (Dormand & Prince 1980 Bogacki & Shampine 1989 use two methods of different order to compute the proposal solutions [t + h) and (t + h) and derive an error estimate å (=((--))=="((+))
[| normalized by the absolute error tolerance т. This error estimate is then used to update the step size <- hd h/8'// Next, we discuss the challenges this poses for robustness verification and how we tackle them.
4 CONTROLLED ADAPTIVE ODE SOLVERS
Size
Adaptive ODE solvers (AS) update their step-size h continuously depend- ing the eπror estimate 6. For continuous input regions, this generally yields infinitely many trajectories, making their abstraction intractable. We illustrate this in Fig. (details in App. C.2). where the blue regions (m) mark all (time, step-size) tuples that are reachable after two steps. To over- come this, propose controlled adaptive solvers (CAS), which restrict step-sizes to a discrete set (O), making them amenable to certification ($5). Next, we show how any adaptive ODE solver can be converted into cor- responding CAS solver.
Figure 3: We pare CAS adaptive solvers (AS) with re- spect to the reachable time/step-size tuples af- ter solver steps
Step-Size Update h a, h h/a,
We modify the step-size update rule of any AS
i < Tas if < < otherwise.
2 + h) 2 h)
h
8
and two
4

---

Published as a conference paper at ICLR 2023
with update factor N and the a-induced decision threshold To a. Intuitively, we increase the step size by a factor a if we expect the normalized error after this increase to still be acceptable, i.c., d I P, we decrease the step size by a factor and repeat the step if the error exceeds our tolerance, i.e., 6 > 1, and we keep the same step size otherwise. If the time t + after the next step would exceed the final time Tend, we clip the step size to h min(h, Tand t)- Additionally, we enforce a minimum step-size. For more details, see App. C.I
We contrast the update behaviors of CAS and AS solvers in Fig. 3 We initialize both solvers with the same state and after one step, the CAS solver can reach exactly three different states while the adaptive solver can already reach continuous states (L.. After two steps this difference
becomes even more clear with the CAS solver reaching only 9 states while the adaptive solver can reach a large region of time/step-size combinations
Initial Step-Size During training. the initial step size ho is computed based on the initial state and corresponding gradient. To avoid this dependence during inference, we always use its exponentially weighted average, computed during training (details in App. C.I..
Comparison to Adaptive Solvers CAS solvers can be seen as adaptive solvers with discretized step-sizes of the same order. Due to the exponen- tially spaced step-sizes, CAS can approximate any step-size chosen by an AS up to factor of at most a, with the CAS always choosing the smaller steps. Thus, CAS will need at most a- a-times as many steps as an adaptive solver, assuming that the adaptive solver will never update the step size by more than a in one step. Empirically, we confirm this on a conventional non-linear ODE, plotting mean absolute errors over the mean number of solver steps depending on the error threshold in Fig. 4 There, we see that a dopri5-based CAS solver performs similarly to an unmodified dopri5 (AS). For more details and additional comparisons between the solvers, we refer to App. C.2 and App. H.I
Absolute Error
10a.
CAS
10-2
10-0
# Solver Steps
Figure 4: AS and CAS error over solver steps.
VERIFICATION OF NEURAL ORDINARY DIFFERENTIAL EQUATIONS
While the discrete step sizes of CAS, discussed in $ yield a finite number of trajectories for any input region, there are still exponentially many in the integration time. Naively computing bounds for all of them independently is thus still intractable. To tackle this challenge, introduce the analysis framework GAINS, short for Graph based Abstract Interpretation for NODEs, which allows us efficiently propagate bounds through the ODE solver using graph representation of all trajectories. We discuss two instantiations, one using interval bounds, the other linear bounds.
Let us consider NODE with input 2, either obtained from encoder or directly from the data. We now define the trajectory graph g( = (V, E), representing all trajectories T(2)) for z E Z. The nodes V represent solver states (t, h) with time and step-size h and aggregate interval bounds on the corresponding z(t). The directed edges e E & connect consecutive states in possible solver trajectories. This representation allows us to merge states =(t) with identical time and step-size, regardless of the trajectory taken to reach them. This reduces the number of trajectories or rather solver steps we have to consider from exponential O (exx((Tan)) to quadratic O (TTn)) (given most (Tend log(Tend)) nodes in V as derived in App. B making the analysis tractable.
Verification with Interval Bounds We first note that each solver step only consists of computing the weighted sum of evaluations of the network g, allowing standard interval bound propagation to be used for its abstraction. We call this evaluation of a solver on set of inputs an abstract solver step. Now, given an input 2, we construct our trajectory graph (22) as follows: We do an abstract solver step, compute the interval bounds of the local error estimate d(t, and check which step size updates (increase, accept, or decrease) could be made according to the CAS. Depending on the looseness of the bounds, multiple updates might be chosen; we call this case trajectory splitting. For each possible update, we obtain a new state tuple (t', hh) and add the node (t', h!) to V and an edge from (t, /t) to (t', h') to E. If the node (t', A') already existed, update its state to contain the convex hull of the interval bounds. We repeat this procedure until all trajectories have reached the termination node (Tend, 0). This yields complete trajectory graph and interval bounds for 2 (Tend)-
5

---

Published as a conference paper at ICLR 2023
0.
(8)
(d)
Figure 5: An example trajectory graph ((2) construction for controlled adaptive ODE solver with ho 2
2 and Tend = I. Note how trajectory splitting occurs in all vertices except the last two states.
If there are further layers after the NODE, standard interval propagation can be employed to obtain the network output y.
We illustrate this construction process in Fig. 5) where we highlight newly added edges and nodes in red and the processed node blue: We initialize the graph with the node (0, ho). in our case ho 1/2 (see Fig. a)). We now do an abstract solver step for this node and find that å > Ta Thus, we either accept the step, yielding the next node (1/2, 1/2), or we reject the step and decrease the step- size by 2, yielding the node (0, 1/4), both are connected to the current node (see Fig. (b)). We now choose among the nodes without outgoing edges the one with the smallest current time t and largest step-size h (in that order), (0, 1/4) in case, and do another abstract solver step, yielding < 1. We thus either accept the step. yielding the node (1/4, 1/4), or additionally increase the step- size, yielding the node (1/4, 1/2) (see Fig. (c)). We proceed this way until the only node without outgoing edges is the termination node (Tond, 0) with Tend = 1 in our case (see Fig, S (d))
Verification with Linear Bounds compute more pre- cise linear bounds =Tenn)) we first construct the trajectory graph ((Z) as discussed above, using either interval bounds or the linear bounding procedure described below, retaining crete element-wise upper and lower bounds at every state. We can now derive linear bounds on ((Ten)) in terms of the NODE input 2o by recursively substituting bounds from intermediate computation steps. Starting with the bounds for (Tens, 0), backsubstitute them along every incoming edge, yielding set of bounds in every preceding node. We recursively repeat this procedure until we arrive at the input node. We illustrate this Fig. [6] where we, starting at Tends backsubstitute y to ( and t2, obtaining bounds in terms of z and #2. In contrast to the standard DEEPPOLY backward substitution procedure, node in (( can have multiple successors which reach the final node via different trajectories. We can thus obtain several sets of linear constraints bounding the same expression with respect to the same state, which need to merge in sound manner without losing too much precision. We call this the linear constraint aggregation problem (LCAP) and observe that arises Fig. after an additional backsubstitution step lo yields two bounds, u and u², on y both in terms of 2g-
Asdi to:
at i- A'so t
M S wil to a of A
Tou
N Agte 4
Figure Example upper bounds for = =(Tena) via GAINS. (Lower bounds analogous.) Blue arrows show the backward substitution resulting in LCAP to.
Linear Constraint Aggregation Problem The LCAP requires us to soundly merge a set of different linear constraints bounding the same variable. As an example, we consider a variable y = x(T) for which have upper bounds (w) J=s linear in 2p, which in turn can take values in 2. In this case, we want obtain single linear upper bound y S azo + that minimizes the volume between the constraint and the y 0 plane over 2n aprr-opproi all constraints. More formally, we want solve:
00
30
(b)
72 162 223
Figure 7: Visualization of the ICAP with m 3, shown in (a). In (b) the constraints u u² (dashed) over-approximated by 112 via CURLS, which also bounds ut (dotted).
while soundly
( azo + edzo, s.l. azg + e max a 20 + +c, Vzo E 2.
arg min /

---

Published as a conference paper at ICLR 2023
Table 1: Means und standard deviations of the standard (Std.), adversarial (Adv.), and certified (Cert.) accuracy ohtained with GAINS depending on the training method und evaluated on the first 1000 test set samples.
0.10
0.15
Dataset
Training Method
Std. [%]
Adv. [%]]
Cert. [8]]
Adv. [%]]
Cert. [%]
Adv. [%]
Cert. [%c]
Standard
98.8-0.4
23.2
0,040.0
2.541.6
0.049.0
0,3
0,0
MNIST
Adv.
0.11
99,2
95.4 20.4
0,0
88.3
0.0
59.4
0
GAINS
0.11
0.22
91,8=1.3
95.5
88,5#1.
91.5-206
89.0=1.1
86.8 86.8-20
84,0=27
86,8#2.1
47,247.9
83,742.3
84,5
21,4411
79,743.4
0,2402
Standard
88.6
0,1
0,0
0
0.0
FMNIST
Adv.
0.11
80,920.7
70.2
0,0
47,1
0.0299.0
0.11
75.1
65.7#1.0
62.5-1.1
21.1
13.349.1
GAINS
0.16
71.5=1.7
64.0#2.7
61.3-27
60.1
55,0
While this can be cast as linear program by enumerating all exponentially many comers of Z, this becomes intractable even modest dimensions. To overcome this challenge, we propose Constraint Unification via ReLU Simplification (CURLS), translating the max u² } into composition of ReLUUs, which can be handled using the efficient DEFPPOLY primitive proposed by [Singh et al. 2019a). For pair of constraints u. ut we can rewrite their maximum as
max ii u + max(0, uf ui = u + ReLU(u, v JE1,2
(8)
In the case of m constraints, this rewrite can be applied multiple times. We note that lower bounds can be merged analogously and visualize CURLS for 1-d problem in Fig. There, the first iteration already yields the constraint u 1 dominating the remaining u².
Training In order train NODEs amenable verification we utilize the box bounds discussed above and sample x trajectories form G(Z). For more details, please see App. B
Bound Calculation During the computation of the bounds, GAINS combines verification with interval and linear bounds by using the tighter bound of either approach (more details in App. C.3
6 EXPERIMENTAL EVALUATION
We implement GAINS in PyTorch (Paszke et al. 2019) and evaluate all benchmarks using single NVIDIA RTX 2080Ti. We conduct experiments on MNIST (LeCun et al.) 1998), FMNIST (Xiao et al. 2017), and PHYSIO-NET (Silva et al. 2012). 3) For image classification. we use architecture consisting of two convolutional and one NODE layer (see Table 5 in App. D for more details). For time-series forecasting, we use latent ODE (see Table o in App. for more
Experimental Setup
details). We provide detailed hyperparameter choices in App. D and E
6.1 CLASSIFICATION
We train NODE based networks with standard, adversarial, and provable training (c, E (0.11, 0.22))
and certify robustness to foe -norm bounded perturbations of radius defined in Eq. ( We report means and standard deviations across three runs at different perturbation levels (e E (O.T, 0.15, 0.2)) depending the training method in Table Both for MNIST and FMNIST, adversarial accura- cies are low (0.0% to 23.2 23.2%) for standard trained NODEs, agrecing well with recent observations showing vulnerabilities to strong attacks (Huang et al. 2020). While adversarial training can sig- nificantly improve robustness even against these stronger attacks, we can not certify any robustness. Using provable training with GAINS significantly improves certifiable accuracy (to up to 89% de- pending on the setting) while reducing standard accuracy only moderately. This trade-off becomes more pronounced as we consider increasing perturbation magnitudes for training and certification.
6.2 TIME TEME-SERIES FORECASTING
For time-series forecasting, we consider the PIYSIO-NET (iilaa et al., 2012) dataset, containing 000 time-series of up to 48 hours 35 irregularly sampled features. We rescale most features
We release our code https: https:://githhub.co///tt Srİ/GAINS

---

Published as a conference paper at ICLR 2023
Table 2: Comparisen of the mean absolute entors for the unperturbed samples (Sud. MAB). and the adversarial (Adv),, and certifiable (Cert.) v-á rohustness with v 0.1 and oblained using different provable training methods on the full PHYSIO NET test set.
0.05
0.10
= 0.20
Setting
Training Method
Std. MAE [x10-²]
Adv.
Cert.
Adv. [%}
Cert. [%}
Adv. [8]]
Cert. [96]
Standard
47,4
54,3#5.5
0.0
13.7429
0.0
2,3
0.0
6h
0.1
$1.1
97,740.
93.0+27
77,0
60.4=10.9
42,0=11.
24,2
GAINS
0.2
57,6*26
100.0#0.0
99,8+0.1
96.4+21
93.1=4.6
80.1=117
70,5+118.
Standard
49.9202
65.2420
0.0
16.6 4255
0.0
2.0
0.0
12h
0.1
50,9204
98,040a
94,54907
74.349.5
55,841.5
28,9
17,2401
GAINS
0.2
52,950.1
99,1 99,1
98.3
87,8
80,3
52,3
38,5
Standard
51,2
69,741.
0,0
23.6
0.040.
3,741.0
0.049.
24b
0.1
51,5#0.1
97,9#00
96.2*94
78.3+2.
68.0=1a
32,6-000
22,7#10
GAINS
0.2
53,75077
99,740.1
99.1
92.34117
89,4=2.4
59,8=777
50.5
to mean 14 and standard deviation a = (before applying perturbations) and refer to App- for more details. We consider three settings, where we predict the last measurement L, without having access to the preceding 6, 12, or 24 hours of data. In Table 2 we report the mean absolute prediction error (MAE) for the unperturbed samples and y-ô-robustness (see Eq. (2) for relative and absolute error tolerances of v = 0.1 and 5 = 0.01, respectively, at perturbation magnitudes c = {0.05, 0.1, 0.2). We observe only minimal drop in standard precision, when certifiably training with GAINS at moderate perturbation magnitudes (e, = 0.1) while increasing both adversarial and certified accuracies substantially. Interestingly, the drop in standard precision is the biggest for the 6h setting, despite having the shortest forecast horizon among all settings. We hypothesize that this due to the larger number of input points and thus abstracted embedding steps leading to increased approximation errors. Further, while we can again not verify any robustness for standard trained NODEs, they exhibit non-vacuous empirical robustness. However, without guarantees it remains unclear whether this is due to adversarial examples being harder to find or NODEs being inherently more robust. Across settings, we observe that training with larger perturbation magnitudes leads to slightly worse performance on unperturbed data, but significantly improves robustness.
6.3 ABLATION
Trajectory Sensitivity We investigate whether the solver trajectory, i.e., the chosen step-sizes, of CAS solvers are susceptible to adversarial perturbations by conducting adversarial attack aiming directly to change the trajectory l'(z)) (see App. F for more details). In Table we report the success rate of this attack for MNIST, showing that even at moderate perturbation magnitudes (c 0.1) attacks are (al- most) always successful if models are trained using standard or adversarial training. While training with GAINS reduces this susceptibility notably, it remains significant. This highlights the need to con- sider the effect of chosen solver on robustness, motivating both the use of CAS solvers and the trajectory graph-based based approach of GAINS.
Table 3: Mean and standard deviation of the at- tack success [%] on the first 1000 samples of the MNIST test set.
Training
Attack Success (%)
0.15
Standard
98,92993
100.020.1
100.0200
Adversarial
0.11
99,340.1
100.0
100,0=00
0.11
73,4335
86,3435
95.5
GAINS
0:22
65.2477
75,3
22.248.0
Linear Constraint Aggregation To evaluate CURLS the Linear Constraint Aggregation problem (LCAP), we compare it to an LP- based approach based on Eq. 7 and implemented using a commercial LP solver (GUROBI (Gurobi Opti mization, LLC, 2022). However, considering all soundness constraints associated with the 2d corner points use
Volume Ratio vol,
Running Time [s]
1.02-
102
100
1.00
10-2.
0.98
10-4
0
50
100
50
100
d
CURLS
Figure 8: Comparison of the CURLS and LP solution to the LCAP with respect to normalized volume (left) and runtime (right).
is intractable. Therefore, an iterative sampling strategy (see App. for more details).
8

---

Published as a conference paper at ICLR 2023
To compare the obtained relational constraints, consider the volumes induced by the two methods and report mean normalized abstraction volumes vol voILS in Fig. for sets of randomly generated constraints in d = [5, 100] dimensions (see App. G for more details). We observe that while the LP based solutions
more precise for up to 75 dimensional problems, they take around 5 orders of magnitude longer to compute. For higher dimensional problems, CURLS is both faster and more precise. During the certification of single input, we consider multiple hundred up to 512 dimensional LCAP problems, making even the sampling based LP solution infeasible in practice and highlighting the importance of the efficient constraint aggregation via CURLS for the GAINS framework.
RELATED WORK
Empirical Robustness of NODEs Yan al. (2020) introduce TisODEs, by adding regular- ization term to the loss which penalizes differences between neighboring trajectories to improve empirical robustness. A range of work (Kang et al. 202T Rodriguez al., 2022 Huang et al.) 2020 Zakwan et al., 2022) trains NODEs which satisfy different forms of Lyapunov stability (Jus- tus 2008), yielding increased empirical robustness. However, Huang et al. (2020) have shown that these empirical robustness improvements might be due to gradient obfuscation (Athalye et al. 2018) )) caused by the use of adaptive step-size solvers. Furthermore, Carrara et al. (2022) have shown that varying the solver tolerance during inference can increase empirical robustness.
Verification and Reachability Analysis of NODEs Lopez al. (2022) analyze the dynamics of very low dimensional (d < 10) NODEs using CORA (Althoff 2013 and the (polynomial) Zonotope domain, and those of higher dimensional linear NODEs using the star domain. In contrast to work, they analyze only the learned dynamics, excluding the solver behavior, which has a signifi- cant effect on practical robustness (Huang al. 2020p. Grunbacher et al. (202I) introduce stochastic Lagrangian reachability to approximate the reachable sets of NODEs with high confidence by prop- agating concrete points sampled from the boundary of the input region. However, the number of required samples depends exponentially on the dimension of the problem, making it intractable for the -ige-siienni setting we consider. HHuang al.] (2022) propose forward invariance ODE, sampling-bass verification approach leveraging Lyapunov functions. Moreover, when using fixed step size ODE solvers the verification of NODES can be seen as verifying neural network dynamic
models (Admss et al. 2022 Wei & Liu 2022) or by unrolling them even conventional feed-forward neural networks.
Neural Network Verification Deterministic neural network verification methods, typically ei- ther translate the verification problem into linear (Palma et al. 2021; ; Müller al.) 2022] Wang ct al. 2021 Xu et al. 202I), mixed integer TTieng et al. [019 Singh et al. [019b)), or semidefinite (Raghunathan al.] 2018 Dathathri et al. 2020) optimization problem, or propagate abstract ele- ments through the network (Singh et al.] 2019a| Gowal et al.) 2019 Singh et al.. 201 8a) To obtain models amenable to certification, certified training (Mirman et al. 2018] Gowal et al. 2018 Zhang et al. 2020) methods use the latter class of approaches to compute and optimize worst-case over- approximation of the training loss. However, none of these methods support the analysis of NODEs without substantial extensions.
8 CONCLUSION
In this work, we propose the analysis framework GAINS, Graph based Abstract Interpretation for NODEs, which, for the first time, allows the verification and certified training of high dimensional NODEs based on the following key ideas: i) We introduce CAS solvers which retain the efficiency of adaptive solvers but are restricted to discrete instead of continuous step-sizes. ii) We leverage CAS solvers to construct efficient graph representations of all possible solver trajectories given an input region. iii) We build on linear bound propagation based neural network analysis and propose new algorithms to efficiently operate on these graph representations. Combined, these advances enable GAINS analyze NODEs under consideration of solver effects in polynomial time.

---

Published as a conference paper at ICLR 2023
ETHICS STATEMENT
As GAINS, for the first time, enables the certified training and verification of NODEs, it could help make real-world AI systems more robust to both malicious and random interference. Thus any positive and negative societal effects these systems have already could be amplified. Further, while we obtain formal robustness guarantees for & -norm bounded perturbations, this does not (necessarily) indicate sufficient robustness for safety-critical real-world applications, but could give practitioners a false sense of security.
10 REPRODUCIBILITY STATEMENT
We publish our code, all trained models, and detailed instructions on how to reproduce our results https://gi thub. com/eth- sri/GAINS and provide an anonymized version to the reviewers. Further algorithmic details can be found in App. A A B Additionally, in App. App- we provide implemen- tation details and further discussions for our general method, classification tasks, and time-series forecasting tasks resistively, Lastly, details on the adversarial attacks and LCAP dataset used in $6.3 can be found Fnd respectivll
ACKNOWLEDGEMENTS
We would like to thank anonymous reviewers for their constructive comments and insightful questions.
This work has been done part of the EU grant ELSA (European Lighthouse Secure and Safe AI, grant agreement no. 101070617) and the SERI grant SAFEAI (Certified Safe, Fair and Robust Artificial Intelligence, contract MB22.00088). Views and opinions expressed are however those of the authors only and do not necessarily reflect those the European Union or European Com- mission. Neither the European Union nor the European Commission can be held responsible for them.
The work has received funding from the Swiss State Secretariat for Education, Research and Inno- vation (SERI).
10

---

Published as a conference paper at ICLR 2023
REFERENCES
Steven Adams, Morteza Lahijanian, and Luca Laurenti. Formal control synthesis for stochastic neural network dynamic models. IEEE Control Systems Letters, 2022.
Matthias Althoff. Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets. In Proceedings of the 16th international conference on Hybrid systems: computation and control, ISCC 2013, April 8-11, 2013, Philadelphia, PA, USA, 2013. doi:
2,.1445/2461338226611555
Anish Athalye, Nicholas Carlini, and David A. Wagner. Obfuscated gradients give a false sense of security: Circumventing defenses to adversarial examples. In Proc. ICML, volume 80, 2018.
Battista Biggio, Igino Corona, Davide Maiorca, Blaine Nelson, Nedim Srndic, Pavel Laskov, Gior- gio Giacinto, and Fabio Roli. Evasion attacks against machine learning
time. In Machine Learning and Knowledge Discovery in Databases European Conference, ECML PKDD 2013, Prague, Czech Republic, September 23-27, 2013, Proceedings, Part III, volume 8190, 2013. doi: 1110079978---42222 3-442-409994433
Przemyslaw Bogacki and Lawrence Shampine. (2) pair of runge-kutta formulas. Applied Mathematics Letters, 2(4), 1989.
Edward De Brouwer, Jaak Simm, Adam Arany, and Yves Moreau. Gru-ode-bayes: Continuous modeling of sporadically-observee time series. In Advances Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurlPS 2019, December 8-14, 2019, Vancouver, BC, Canada, 2019.
Fabio Carrara, Roberto Caldelli, Fabrizio Falchi, and Giuseppe Amato. Improving the adversarial robustness of neural ode image classifiers by tuning the tolerance parameter. Information, 13(12); 555, 2022.
Tian Qi Chen, Yulia Rubanova, Jesse Bettencourt, and David Duvenaud. Neural ordinary differential equations. In Advances Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurlPS 2018, December 3-8, 2018, Montréal, Canada, 2018
Sumanth Dathathri, Krishnamurthy Dvijotham, Alexey Kurakin, Aditi Raghunathan, Jonathan Ue- sato, Rudy Bunel, Shreya Shankar, Jacob Steinhardt, Ian J. Goodfellow, Percy Liang, and Pushmeet Kohli. Enabling certification of verification-agnosiic networks via memory-efficient semidefinite programming. In Advances in Neural Information Processing Systems 33: Anmual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual, 2020.
John R Dormand and Peter Prince. family of embedded runge-kutta formulae. Journal of computational and applied mathematics. 6(1), 1980.
Leonhard Euler. Institutiones calculi integralis, volume 1. 1792.
Claudio Ferrari, Mark Niklas Müller, Nikola Jovanovic, and Martin T. Vechev. Complete verification via multi-neuron relaxation guided branch-and-bould In The Tenth International Conference Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022. URL htttsss//ooeereveeewwwe///frrrr
1oHa
Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Mar- tin T. Vechev. A12: safety and robustness certification of neural networks with abstract interpreta- tion. In 2018 IEEE Symposium on Security and Privacy, SP 2018, Proceedings, 21-23 May 2018, San Francisco, California, USA, 2018. doi: 10.1 10.1109/SP.2018 8.00058.
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Ue- sato, Relja Arandjelovic, Timothy A. Mann, and Pushmeet Kohli. On the effectiveness interval bound propagation for training verifiably robust models. ArXiv preprint, abs/1810. 12711..111....1111 2018.

---

Published as a conference paper at ICLR 2023
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Ue- sato, Relja Arandjelovic, Timothy Arthur Mann, and Pushmeet Kohli. Scalable verified training for provably robust image classification. In 2019 IEEE/CVF International Conference Com- puter Vision, ICCV 2019, Seoul, Korea (South), October 27 November 2, 2019, 2019. doi: N0.1109//CCV22219000009999
Sophie Grunbacher, Ramin Hasani, Mathias Lechner, Jacek Cyranka, Scott A Smolka, and Radu Grosu. On the verification of neural odes with stochastic guarantees. In Proc. of AAAI, volume 35, 2021.
Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual, 2022.
Yifei Huang, Yaodong Yu, Hongyang Zhang, Yi Ma, and Yuan Yao. Adversarial robustness of stabilized neuralodes might be from obfuscated gradients. ArXiv preprint, Abs/2009.13145, 2020.
Yujia Huang, Ivan Dario Jimenez Rodriguez, Huan Zhang, Yuanyuan Shi, and Yisong Yue. Fi-ode: Certified and robust forward invariance in neural odes. arXiv preprint arXiv: 16.14000 2022.
James Justus. Ecological and Цyарunov stability. Philosophy of Science, 75(4), 2008.
Qiyu Kang, Yang Song, Qinxu Ding, and Wee Peng Tay. Stable neural ode with lyapunov-stable equilibrium points for defending against adversarial attacks. Advances in Neural Information Processing Systems, 34, 2021.
Guy Katz, Clark W. Barrett David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. ArXiv preprint, abs//702.00 135, 2017.
Yann LeCun, Léon Bottou, Yoshua Bengio, and Patrick Haffner. Gradient-based learning applied to document recognition. Proc. IEEE, 86(11), 1998. doi: 10.1109/5.72691.
Diego Manzanas Lopez, Patrick Musau, Nathaniel Hamilton, and Taylor T Johnson. Reach- ability analysis a general class of neural ordinary differential equations. ArXiv preprint, abs/2207.06531, 2022.
Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant to adversarial attacks. In Proc. of ICLR, 2018.
Matthew Mirman, Timon Gehr, and Martin T. Vechev. Differentiable abstract interpretation for provably robust neural networks. In Proc. of ICML, volume 80, 2018.
Mark Niklas Müller, Robin Staab, Mare Fischer, and Martin T. Vechev. Effective certification of monotone deep equilibrium models. ArXiv preprint, awt//110.08266. 2021.
Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Plischel, and Martin T. Vechev. PRIMA: general and precise neural network certification via scalable convex hull approximations. Proc. ACM Program. Lang., 6(POPL), 2022. doi: 10. 145/34987704.
Mark Niklas Müller, Franziska Eckert, Mare Fischer, and Martin Vechev. Certified training: Small boxes are you need. The Eleventh International Conference on Learning Representations, 2023. URL htppt:tt///pppeeeieeee www.nnttntettnttemm http://orrmmmdd77ouuxxtxxtt
Alessandro De Palma, Harkirat S. Behl, Rudy R. Bunel, Philip H. S. Torr, and M. Pawan Kumar. Scaling the convex barrier with active sets. In Proc. of ICLR, 2021.
Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Köpf, Edward Yang. Zachary DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. Pytorch: An imperative style, high-performance deep learning library. In Advances in Neural Information Processing Systems 32: Anmual Con- ference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada, 2019.
12

---

Published as a conference paper at ICLR 2023
Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. Semidefinite relaxations for certifying bustness to adversarial examples. In Advances Neural Information Processing Systems 31: Annual Conference Neural Information Processing Systems 2018, NeurlPS 2018, December 3-8, 2018, Montréal, Canada, 2018
Ivan Dario Jimenez Rodriguez, Aaron Ames, and Yisong Yuc. Lyanet: A Iyapunov framework for training neural odes. In International Conference on Machine Learning. PMLR, 2022.
Yulia Rubanova, Ricky TQ Chen, and David Duvenaud. Latent odes for ireeularly-samplld time series. arxiv. Search in, 2019.
Carl Runge. Über die numerische auflösung von differentialgleichunge. Mathematische Annalen, 46(2), 1895.
Lawrence F Shampine. Error estimation and control for odes. Journal of Scientific Compuling, 25 (1), 2005.
Ikaro Silva, George Moody, Daniel Scott, Leo A Celi, and Roger G Mark. Predicting in-hospital mortality of ieu patients: The physionet/computing in cardiology challenge 2012. In 2012 Com- puting in Cardiology. IEEE, 2012.
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin T. Vechev. Fast and effective robustness certification. In Advances in Neural Information Processing Systems 31; Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada, 2018a.
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin T. Vechev. Fast and effective robustness certification. In Advances in Neural Information Processing Systems 31; Annual Conference on Neural Information Processing Systems 2018, NeurlPS 2018, December 3-8, 2018, Montréal, Canada, 2018b.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certi- fying neural networks. Proceedings of the ACM on Programming Languages, 3(PPLL), 2019a.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin T. Vechev. Boosting robustness certi- fication neural networks. Proc. of ICLR, 2019b.
Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian J. Goodfel- low, and Rob Fergus. Intriguing properties of neural networks. In Proc. of ICLR, 2014.
Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In Proc. of ICLR, 2019.
Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J. Zico Kolter. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. In Advances in Neural Information Processing Systems 34: Annual Con- ference on Neural Information Processing Systems 2021, NeurIPS 2021, December 6-14, 2021, virtual, 2021.
Tianhao Wei and Changliu Liu. Safe control with neural network dynamic models. In Learning for Dynamics and Control Conference, pp. 739-750. PMLR, 2022.
Ezra Winston and Zico Kolter. Monotone operator equilibrium networks. In Advances in Neu- ral Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual, 2020.
Han Xiao, Kashif Rasul, and Roland Vollgraf. mushion-mnise novel image dataset for benchmark- ing machine learning algorithms. ArXiv preprint, abx/1708.00747, 2017.
Kaidi Xu. Huan Zhang, Shiqi Wang. Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsich. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In Proc. of ICLR, 2021.
13

---

Published as a conference paper at ICLR 2023
Hanshu Yan, Jiawei Du, Vincent Y. F. Tan, and Jiashi Feng. On robustness of neural ordinary differential equations. In Proc. of ICLR, 2020.
Muhammad Zakwan, Liang Xu, and Giancarlo Treeaae On robust classification using con- tractive hamiltonian neural odes. ArXiv preprint, abs/2203. 11805 2022.
Huan Zhang, Tsui-Wei Weng, Pin-Ye Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In Advances in Neural Infor- mation Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurlPS 2018, December 3-8, 2018, Montréal, Canada, 2018.
Huan Zhang, Hongge Chen, Chaowei Xiao, Sven Gowal, Robert Stanforth, Bo Li, Duane S. Boning, and Cho-Jui Hsieh. Towards stable and efficient training of verifiably robust neural networks. In Proc. of ICLR, 2020.
14


Reviews:
[{"review_id": "oEnl3-XVzn", "reviewer": "Reviewer_bH4g", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "This paper proposes a method called GAINS to address the robustness certification of neural ODEs via combining ODE solvers with variable steps and an efficient graph representation of solver trajectories. The authors provide some arguments showing the proposed approach significantly reduce the run time.  Numerical study is also performed on MNIST, FMNIST, and Physio-Net to demonstrate the certified robustness of the proposed method. ", "summary_of_the_review": "For now I give a \"6.\" Depending on how the authors address my concerns (on scalability and theoretical novelty), I may either increase or decrease my score. ", "strength_and_weaknesses": "Strength:\n1. The combination of ODE solvers with variable steps and the graph representation of solver trajectories seem to be interesting. \n\n2. The improvement of running time is significant.\n\nWeaknesses:\n\n1. MNIST is a very simple task. Is it possible to run the proposed method for CIFAR10?\n\n2. The theoretical novelty of this paper is unclear. ", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "nZ90qNWcYoA", "reviewer": "Reviewer_CQh5", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "This paper deals with the verification of Neural Ordinary Differential Equations (NODEs), which some papers have claimed to have more inherent robustness than standard neural networks.\nEvaluating a NODE is based on solving the ODE defined by an initial condition (the input to the model) and a dynamics model, given by a trained neural network. Different types of ODE solvers might be used for the solution. This goal of this paper is to be able to obtain bounds on the outputs of the ODE, such that their robustness can be evaluated rigorously.\n\nThis work propose: \n- to restrict the possible values that the step size of the solver can take. This allows to get some of the benefits of adaptive solvers, while maintaining the property that the solver can only go through a finite number of states (a state being determined by a time $t$ and a step size $h$). The fact that only a finite number of states can be reached makes it feasible to evaluate bounds on the network output (it just becomes dependent on computing bounds for each possible state)\n- an algorithm to compute bounds on such a computational graph. Usually, bound computation is done on fixed computational graphs, where you can define exactly the function of each node (broadly, a node in the computational graph to bound is an activation of a network and can only have been produced in a given way). With the proposed formalism, each node (a given state) may have been reached by doing a variable number of steps of the solver, so to obtain a bound, you need to pick the worst case bound across all the possible paths that may have been taken. The author explain how to do this both for simple IBP bounds, as well as for the more complex linear bounds.\n\nEvaluation is performed on image classification, using MNIST and FashionMNIST, as well as on time series regression. ", "summary_of_the_review": "The paper is rigorous and provide a good solution to the question \"how can you propagate bounds through the solving of a Neural ODE\". The method discussed is presented well. The main doubt is whether that question is worth solving in the first place.\n\n\n[Note]\nI trust myself to review the elements of the paper that relate to verification but don't have significant expertise in Neural ODE.", "strength_and_weaknesses": "# Strengths\nThe paper proposes a clearly novel and interesting solution to be able to perform formal verification and bound propagation on a model for which existing methods would not work. The proposed solution is interesting, builds on existing verification research (DeepPoly) while clearly delineating their own contribution, and makes intuitive sense. \nRelevant context (explanation about adversarial robustness and neural ODE) is given to make the paper accessible.\n\nThe author have provided their codebase as supplementary material, and have thoroughly detalied their experiments in the appendix, which makes me think that the work should be quite reproducible.\n\nThe result seems to be what you would expect with more traditional models: models trained without consideration for later verification are hard (or here apparently impossible) to verify, but incorporating the bounding procedure during the training makes it much easier to perform verification, at the cost of some nominal accuracy.\n\n\n# Weakness\nThe part where I am actually a bit hesitant is on the applicability of this research. I'm mostly familiar with research on neural network verification, and less so on Neural ODE. Is there area where they particularly shine? Observing the experiments, what I see is that if I compare the adversarial and certified accuracy obtained on MNIST (83.9% for eps=0.1), they are significantly worse than simple convnets trained with IBP (99.77% for the same eps), in addition to being much more complex.\nAs a consequence, even if the results are technically interesting, I wonder if they are actually important. \n\nI also note that the author make a claim that restricting step sizes to an exponential grid has \"minimal impact on solver efficiency\". I think that this should be evaluated beyond the results of Figure 4., which seems to be only for a single ODE. Would it be possible to perform this evaluation on more complex ODE, such as the one that might be defined by a Neural ODE? \n\n## Question about training.\nIn Section 5., it is described that IBP bounds are used for training, and that trajectory needs to be sampled. Given the description of section 5., it seemed to me that it would be possible to actually compute a true upper bound. Is the decision to sample trajectories based on making the training iterations faster / use less memory, or is there another reason why it's not possible to use the true upper bound?\n\n", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "LbH--HkyXKk", "reviewer": "Reviewer_yJLc", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "### Problem\nThe paper tackled robustness certification and certified training of Neural ODEs.\n\n### Proposed Method\nAuthors claim that directly verifying adaptive solvers is difficult. So authors propose a modified solver called controlled adaptive ODE solver. This essentially restricts the step-sizes to a discrete set, which in turn restricts states that the solver can reach compared to the usual adaptive solvers.\n\nThe authors then propose a novel verification method for this solver, which is built on top of propagation-based verification methods like DeepPoly or CROWN.\n\nAuthors also show how this method can be used for certified training.\n\n### Experiments\nAuthors conduct two sets of experiments, on classification on MNIST and FMNIST, and time-series on Physio-net. ", "summary_of_the_review": "The problem and proposed method are novel. But I am concerned about the scalability of the technique. The bounds don't seem to be very tight on MNIST. Experiments missing on a medium scale dataset like CIFAR-10 make it difficult to validate this. I am on the borderline (5/6) for this reason at the moment and willing to change my rating depending on responses to my concerns.", "strength_and_weaknesses": "### STRENGTHS\n1. Novel Problem:\nThe verification of neural ODEs is an under-explored area.\n2. Novel solution:\nI like that the solution is built on top of a propagation based method, which makes it versatile and easier to develop in the future. Furthermore, it is clear that the authors had to do sufficient work to first make CAS solvers, then \n3. Good writing:\nThe paper is very well written. The figures are also very helpful for understanding the method.\n\n### WEAKNESSES\n1. Validate CAS vs AS on more problems\n- Could you please add experiments on more common problems to compare the two solvers. It is important to make sure that CAS is not much inferior to usual AS solvers.\n2. Certified accuracy of even adversarial trained methods is 0 everywhere\n- This is quite surprising. It would be important to understand why this is happening.  Does this mean that the bounds produced by the method are very weak? I would recommend the following experiments\n- Could you plot a figure similar to Fig.2 from Beta-CROWN 9 (https://arxiv.org/pdf/2103.06624.pdf) as this will help us understand the tightness of the bounds.\n- Can you reduce the epsilon further to see if we can verify adv trained networks at all? \n3. Medium scale experiments missing\n- It would be good to have experiments on CIFAR-10. It is common to use even Imagenet-32 in Neural ODE papers, so running on CIFAR-10 should not be a trouble. Point 2 above scares me that your method might not scale well scale well.\n- Baseline: Would it be possible to add a baseline into the tables? Maybe an inferior version of your own method by removing some component? \n\n", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "Not applicable"}, "extra_text": {}}, {"review_id": "7B9H2cqRNi", "reviewer": "Reviewer_LBBD", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "This paper proposes a framework based on linear bound propagation that takes advantage of a new class of ODE solvers to enable training and verification of Neural Ordinary Differential Equations. Specifically, the proposed new class of adaptive ODE solvers, CAS, is based on variable but discrete time steps such that the solver trajectories can be captured in a graph representation. This reduces the runtime of NODES from intractable exponential computation time to polynomial time. ", "summary_of_the_review": "To the best of the my knowledge, this work is the first to present a scalable verification framework for NODEs. The paper is well written, and the theoretical contribution seems sound. The authors included an extensive empirical evaluation of the performance of the framework. The authors should explain in more detail the restrictiveness of the proposed controlled adaptive ODE solver. ", "strength_and_weaknesses": "One of the main contributions of this paper is the reduction of the computational complexity of verification of NODES by GAINS enabled by controlled adaptive ODE solvers. The theoretical impact of the use of a CAS over an AS solver has been briefly and clearly described in 'Comparison to Adaptive Solvers' on page 5. However, the included empirical comparison is difficult to grasp. Moreover, from Figure 4, it appears that for a small error threshold, the difference in performance between CAS and AS is relatively large. It would be good if the authors could include for some of the experiments on the (F)MNIST and PHYSIO-Net datasets the difference in performance and (standard) adversarial robustness of the AS and CAS solvers. Furthermore, the authors should clarify the impact of the update factor on the computational complexity. \n\nThe authors perform an extensive empirical evaluation of the performance of the framework. These experiments clearly show the strength of the proposed framework to assess and improve adversarial robustness. It would be interesting to compare the performance of the networks trained by GAINS and TisODE or other approaches as cited in the related work that improve empirical robustness. \n\nFurthermore, it should be emphasised in the related works that for an ODE solver with fixed time step, the problem considered in this work is similar to that of verifying neural networks dynamic models, which are  discrete time dynamical models driven by a neural network for which formal robustness verification and control against have been recently studied [1,2]. \n\n[1] : Adams, Steven, et al \"Formal control synthesis for stochastic neural network dynamic models.\" IEEE Control Systems Letters (2022). \n\n[2] :  Wei, Tianhao, and Changliu Liu. \"Safe Control with Neural Network Dynamic Models.\" Learning for Dynamics and Control Conference. PMLR, 2022.\n\n", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}]

Author rebuttal:

Decision: Accept: poster