Venue: ICLR 2023 Conference

Reviews:

final_score: rating: 6: marginally above the acceptance threshold
review_content: 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. 
strength_and_weaknesses: Strength:
1. The combination of ODE solvers with variable steps and the graph representation of solver trajectories seem to be interesting. 

2. The improvement of running time is significant.

Weaknesses:

1. MNIST is a very simple task. Is it possible to run the proposed method for CIFAR10?

2. The theoretical novelty of this paper is unclear. 
clarity,_quality,_novelty_and_reproducibility: The paper is well written and includes some solid results on certified robustness of the neural ODEs. Codes have been provided to reproduce the results. I think the idea of combining ODE solvers with variable steps and the graph representation of solver trajectories is interesting. I am a little bit concerned with the scalability of the proposed approach, since MNIST is really considered as a very simple task. 
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.
review_title: null

final_score: rating: 8: accept, good paper
review_content: summary_of_the_paper: ### Problem
The paper tackled robustness certification and certified training of Neural ODEs.

### Proposed Method
Authors 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.

The authors then propose a novel verification method for this solver, which is built on top of propagation-based verification methods like DeepPoly or CROWN.

Authors also show how this method can be used for certified training.

### Experiments
Authors conduct two sets of experiments, on classification on MNIST and FMNIST, and time-series on Physio-net. 
strength_and_weaknesses: ### STRENGTHS
1. Novel Problem:
The verification of neural ODEs is an under-explored area.
2. Novel solution:
I 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 
3. Good writing:
The paper is very well written. The figures are also very helpful for understanding the method.

### WEAKNESSES
1. Validate CAS vs AS on more problems
- 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.
2. Certified accuracy of even adversarial trained methods is 0 everywhere
- 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
- 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.
- Can you reduce the epsilon further to see if we can verify adv trained networks at all? 
3. Medium scale experiments missing
- 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.
- Baseline: Would it be possible to add a baseline into the tables? Maybe an inferior version of your own method by removing some component? 


clarity,_quality,_novelty_and_reproducibility: The presentation and clarity are very good.

The novelty and quality of technical contribution is also good.

The code is provided for reproducibility.
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.
review_title: null

final_score: rating: 8: accept, good paper
review_content: 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. 
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. 

The 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. 

Furthermore, 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]. 

[1] : Adams, Steven, et al "Formal control synthesis for stochastic neural network dynamic models." IEEE Control Systems Letters (2022). 

[2] :  Wei, Tianhao, and Changliu Liu. "Safe Control with Neural Network Dynamic Models." Learning for Dynamics and Control Conference. PMLR, 2022.


clarity,_quality,_novelty_and_reproducibility: The authors are the first to propose an analysis framework for verification of high dimensional NODEs. The paper is well written, the context and problem formulation are introduced clearly and the most important aspect of contribution are explained well. The theoretical results given seem to be theoretically sound. The theoretical and experimental details are clearly documented, and the code for implementation of the work is shared.
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.
review_title: null

final_score: rating: 6: marginally above the acceptance threshold
review_content: 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.
Evaluating 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.

This work propose: 
- 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)
- 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.

Evaluation is performed on image classification, using MNIST and FashionMNIST, as well as on time series regression. 
strength_and_weaknesses: # Strengths
The 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. 
Relevant context (explanation about adversarial robustness and neural ODE) is given to make the paper accessible.

The 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.

The 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.


# Weakness
The 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.
As a consequence, even if the results are technically interesting, I wonder if they are actually important. 

I 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? 

## Question about training.
In 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?


clarity,_quality,_novelty_and_reproducibility: See above.

Some minor notes / typos:
- The plots of Step size vs. Time (in Figure 1. or Figure 3.) allow the step size to go negative, is that possible / normal?
- The caption of Figure 7 is kind of overlapping with the legend of the figures.
- At the end of section 5, the authors discuss the fact that "eps-annealing alone is insufficient to stabilize the training". I did not see any discussion of annealing prior to that in the paper, but it is discussed in the appendix. Either some more of the discussion on training should be moved to the main paper, or this bit should be added to the appendix, because as it is, the context for it is not present.
- Second line of section 6.2 -> "We rescaling most features"
- Caption of Figure 9 -> "Comparison of th "


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.


[Note]
I trust myself to review the elements of the paper that relate to verification but don't have significant expertise in Neural ODE.
review_title: null

Meta-review: metareview:_summary,_strengths_and_weaknesses: The authors develop a novel certified robustness training and verification method for neural ODEs. By restricting the step-sizes taken in a neural ODE solver, they are able to reduce the problem of certifying robustness of neural ODEs to that of standard computation graphs, enabling them to take advantage of efficient certification methods like CROWN and DeepPoly.

Strenghts:
1. The paper achieves SOTA certified robustness results for Neural ODEs.
2. The authors obtain an exponential speedup relative to prior work on Neural ODE certification.

Weaknesses:
1. The paper only presents experiments on smaller datasets and tasks, calling into question the scalability of the method to larger datasets and complex prediction tasks where Neural ODEs are likely to be used.

In summary, the reviewers were satisfied with the contributions of the paper and have consensus on acceptance of the paper.  
justification_for_why_not_higher_score: The authors do not show scalability of the method to complex tasks where Neural ODEs would have a significant advantage.
justification_for_why_not_lower_score: The authors develop efficient and novel certification and certified training algorithms for a challenging class of neural models, i.e., neural ODEs.
Decision: Accept: poster