Venue: NeurIPS 2022 Conference

Reviews:

final_score: rating: 6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.
review_content: summary: This paper builds the connection between white-box, non-linear dynamic models to black-box, neural dynamic models. Furthermore, this paper expresses the potential usage of neural abstraction of safety verification tasks, especially for dynamics without local Lipschitz continuity. How to build neural abstractions and verify over the abstractions might be a potentially exciting direction if the scalability issues and details in the paper could be further elaborated on and explored.


—— Updated the score. Thanks for the explanation for the scalability issues. I assume that the authors included the experiment details in the response to me and 93rE in the updated version of the paper.
strengths_and_weaknesses: *Strengths*

- The idea of replacing non-linear dynamics with neural networks is interesting and potentially useful in the verification community.
- This paper presents better verification results compared to a well-known verification tool.

*Weaknesses*

This paper’s contribution is a bit vague (I think the main contribution is on the verification side, but the author also states the training part as one of the critical contributions. Please correct if my understanding is wrong.) The theorem in the paper comes with the assumption that the neural abstraction exists (The paper leverages a particular category of neural networks: feed-forward neural network with ReLU activations) and lacks existence and convergence guarantee.
-  The main differences between the training method in the paper and the classic regression training process are not well-stated. Using the counterexamples and generating more training samples would guide the search, but how those newly added samples can help with the performance at convergence is not exhibited.
   - One potential experiment: checking if using a large dataset can give a similar performance to using counterexample-based guidance. (The dataset details are not provided in the paper, which is expected.) 
- Theorem 1 in the paper assumes a neural abstraction for a dynamical system F exists, which is a key and strong assumption for the following analysis in the paper. What is the reasonable explanation for this assumption? Can the authors provide theoretical analysis for the existence of the neural abstraction given a dynamic F?
- The benchmarks with better performance in neural abstractions are small-scale and not commonly used. The results from these benchmarks are not convincing enough without further details. (e.g., potentially using cases of these benchmarks, further details of the design choices and reasons for these benchmarks, etc.)




questions: - “Corollary 1 ensures that concluding that a neural abstraction is safe suffices to assert that the original dynamical model is also safe.” Does the neural abstraction come with over approximations? If yes, what is the best over-approximation error this neural abstraction can give? 
- Similar to Weaknesses 2, what is the justification for the existence assumption of the neural abstraction?
This paper uses $\epsilon$ and $\delta$ to measure the disturbance and the abstraction error. Is there a boundary for these two values? Are they arbitrary customized? What is the minimum $\epsilon$ or $\delta$ one can get?
- The benefits of the synthesis part are not clear. Does the classic regression training method fail to train a neural network for verification? What are the differences in the results from the final verification process between these two training methods? (That said, if the training method does not matter, the verification heavily depends on the setting of $\epsilon$ and $\delta$, which also raises questions in the previous point.)

limitations: This paper presents an interesting idea without detailed theoretical analysis and experimental evaluation. The approximation and error-bound analysis are expected. Also, more experimental results about the scalability and justification of the current benchmark setting are expected.
review_title: null

final_score: rating: 7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.
review_content: summary: This work trains a NN (relu) to model a system dynamic of an ODE, then transform this NN into a hybrid automata with affine dynamics. This automata is then verified using dReal, with 2 outcomes. If it is certified, the hybrid automata is a safe abstraction, and is used to prove the safety of the system. If it is not certified, dReal produces a counter example which can be used to refine the NN modeling of the system.
strengths_and_weaknesses: ## str

this paper is clean to read, and presents a very straight forward algorithm that simultaneously provides safety guarantees (automatically) while achieving this with as few computation cycles as possible using CEGIS. I'm not too familiar with this field, but if the claims of novelty is substantiated (maybe other reviewers can help me), then I'm in favor of this paper both in soundness and novelty.

## weakness

This paper suffers the classical problem of scalability, which is ubiquitous in thm proving. while we cannot expect this paper to solve the fundamental problem that's the curse of dimensionality, this work should at least discuss _how_ such a problem can be alleviated. As it stands now this work is bit of a "dead end" where it is difficult to see if the proposed algorithm can be extended to become even more efficient.
questions: I have a feeling that, the CEGIS algorithm, when applied to generating examples for numerical optimization (such as training a NN) can have some wild responses. For instance, it is a known problem in polynomial fitting that one should provide sample points in a particular way (https://en.wikipedia.org/wiki/Chebyshev_nodes). 

I'm unsure if similar phenonium exists in this domain, but nonetheless it should be reported, as I think it provides insights on the nature of the problem. I propose the following experiment, let me know if it sounds reasonable:

- instead of returning 1 sample point from cegis using dReal, try to get 2 distinct points from dReal (this itself can be done in a fairly hacky way, doesn't matter how). 
- randomly choose one of these two points as your counter example
- run until termination, note down properties such as total time spent until a solution is found

repeat the above procedure 100 times. is there a wide distribution difference between solution time? Is there some property of the series of CE points that cause your algorithm to find a safe abstraction sooner?
limitations: this is done well.
review_title: null

final_score: rating: 6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.
review_content: summary: The paper proposes a novel method of using neural-network-based abstractions to verify non-linear dynamical systems. The proposed method can generalize to systems that do not exhibit local Lipschitz continuity.
strengths_and_weaknesses: The paper proposes a method for learning neural abstractions of non-linear dynamical systems. The work is generally sound and interesting.

## Strengths
- The problem of safety verification on non-linear dynamical systems is a problem of great interest to the community of control. The authors clearly describe the limitations of previous methods and provide a thorough comparison in the experiments.
- The technical parts of this paper are quite strong. It is novel to leverage neural networks to approximate dynamics in safety verification.

However, I have some concerns about the proposed method. I summarize all of my major concerns below:
## Weakness
- Some analysis on the size of hybrid automatons cast from neural abstractions is missing. The size of the hybrid automatons is critical for safety verification since it is directly related to approximation precisions.
- It is not very clear why SpaceEx is used for analyzing the generated hybrid automatons. To the best of my knowledge, Flow* can also handle hybrid automatons.
- Though the authors discussed scalability issues of the proposed method, more detailed experimental results on scalability analysis might be a good add-on. In addition, profiling time costs for different steps in the proposed method is important to support the claims in the paper.
questions: - Why not use Flow* or other hybrid automatons analysis methods to analyze the cast hybrid automatons?
- How expensive it is to use dReal in the loop of training?
limitations: The author provides a detailed discussion of limitations.
review_title: null

Meta-review: metareview: This was a borderline paper. The overall idea of using neural networks as abstractions is sound and novel. However, the evaluation is not thorough, there is no theoretical analysis, and concerns about scalability remain. After calibrating across my pile, I am recommending acceptance. Please make sure to incorporate the reviewers' feedback in the final version of the paper. 
confidence: Less certain
Decision: Accept