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: The paper introduces a safety-guaranteeing controller distillation method for neural network dynamic models (NNDM). The approach is based on the stochastic barrier functions. The introduced algorithm works in two phases. In the first phase, a convex approximation results are applied to obtain piecewise linear bounds for the NNDM on the domain discretized into square regions. In the second step, a synthesis of a minimally invasive (according to the provided definition) controller is carried out using the linear programming approach.
strengths_and_weaknesses: The paper introduces a novel approach for a problem of large importance in safe machine learning, i.e. synthesis of safe controllers for NNDM's. For instance, NNDM's are widely encountered in model-based reinforcement learning approaches, and a synthesis of a safe controller given NNDM has a large potential for practical applications. 

The paper aims at bringing the tool of barrier functions previously widely studied in control theory approaches for closed-form models (restricting practical applications in ML) into the world of NN-based models. I have not verified the claim that this is in fact the first paper demonstrating such an approach, but if yes then the paper would constitute a major result. 

The approach is reasonable and is clearly presented. The formal presentation is supported by theoretical results, i.e. lemmas and theorems. The layout makes it easy to follow and understand the algorithm construction. The overall approach seems to be sound. The formal presentation is supported by experimental case studies (Sec. 6). 

I am happy with the formal presentation but have some objections to the experimental evaluation. My main critique, see also questions below, is lack of proper presentation of the setup in the main paper. I would rethink if all of the plots in Fig. 1 are crucial for presentation, and perhaps replace some of them with more illuminating text. The examples, confirm that the approach works in a desirable way (large safety certificate probability/ small $\varepsilon$ of the minimally invasive controller) , however, those results are not compared to a single baseline, which makes them harder to appreciate. The third is the scalability issue, it is actually noted by the authors that the bottleneck is the discretization step. In fact, it is hard to think how such an approach would scale up to larger systems, given that the phase space needs to be discretized into square-like subregions, resulting in an exponential explosion of the number of subregions. Without overcoming this issue the approach may not have a significant impact in reliable ML community, and I would like the authors to at least provide a convincing argument for that there exists a path towards relaxing the restrictive discretization step.

Weighting positives and negatives, I think the paper is a valuable contribution to the reliable machine learning field of research, and I am leaning toward accepting it. 
 I am voting for weak accept at present, but I am open to increasing my score in case the authors satisfactorily address my remarks for the experimental section of the work, i.e., will provide some baseline method evaluation, will improve the presentation of the experimental results in the main part and will discuss how the restrictive discretization step could be circumvented..
questions: * There is no baseline presented for the experimental section, which makes the presented results incomparable, and  hard to evaluate the impact of the algorithm being introduced;
* It would be very nice if authors use at least one example, in which an analytical model is not available or is more complicated than a nonlinear ODE/hybrid system, appearing in the classical applications of barrier function certificates to closed-form models, maybe one of the  MuJoCo standard environments should do a good job here;
* the experimental setting is not clearly introduced in the main part, e.g. the safety certification sets used for the barrier function computation are not provided;
* l. 309, the Husky models used for the experimental evaluation are not standard, haven't seen them being used in RL literature, please explain and provide an appropriate reference;
* regarding the implementation, what is the rationale in having part of the code (i.e. NeuralNetControlBarrier) written in Julia, as opposed to having the code fully written in Python ?

## Minor remarks
* l. 261, elaborate and provide a reference for 'called Jensen’s gap, is a non-negative polynomial of x, u, and moments E[vd]';
* l. 217 the difference between $L_q(x)$ and $L_{q,x}(x) $ is not explained;
limitations: The limitations related especially to the scalability issue have been appropriately addressed in the paper.
review_title: null

final_score: rating: 3: Reject: For instance, a paper with technical flaws, weak evaluation, inadequate reproducibility and incompletely addressed ethical considerations.
review_content: summary: This paper considers the safety guarantees of the neural network dynamic models (NNDMs). Specifically, the authors use stochastic barrier certificate to verify if a given NNDM satisfy the safety in a probabilistic way, which provides a lower bound on the system's safety probability. If the safety probability is below the desired threshold, then the authors propose to directly modify the output of the NNDM that robustly minimize the unsafety probability in a minimally-invasive manner. The authors applied the proposed method on three different control problems.
strengths_and_weaknesses: Strengths:

This paper combines stochastic barrier certificate and convex relaxation of a neural network in a good way.

Weaknesses:

The contibutions of this paper are not clear. There are some related works, and the authors have not compared their method with other approaches, especially in the experiments.  There is one important notation that is misleading. When the safety probability is below the desired threshold, the authors just modify the output of the NNDM, instead of generating controls for the system as claimed by the authors. The ``control'' of a system should not be considered in the form of equation (3). The equation (3) just directly modify the output of the NNDM. For example, if the state x denotes the system's position that is controlled by the system's acceleration, the authors just modify the position to satisfy the safety probability instead of changing the acceleration. In order to model the real control of a system, the authors should consider the control in the $f^w$. In other words, the control is an input to the NNDM.  
questions: 1. In line 15, the authors claim they introduce a method of generating controls for the system. What is the control of the system? The authors just directly modify the system state in the form of equation (3). This is not the real control of the system.

2. It is hard to justify the contribution of this paper since the authors just modify the output of a NNDM (equation (3)) to satisfy the safety probability.

3. In line 112, the authors claim that ``Computation of this probability is particularly challenging because system (1) is stochastic and NN is generally non-convex'' ? I do not think this is a reasonable motivation.

4. In line 118, I do not think u_k is the ``real'' control action of the system. It is just a variable to change the output of a NNDM.

5. In equation (4b), what is $\eta$? Could it be negative?

6. The right hand side of (5) is very likely to be negative. The authors should justify this.

7. In Proposation 1, what is $\lambda_0(x)$? Moreover, in Corollary 1, the conclusion is equivalent to state that $\lambda_0(x)$ is a SOS polynomial following the last equation of Proposation 1. This is really confusing.

8. In line 181, can we always partition $X_s$ to a finite set of regions, in which each region is a basic semi-algebraic set?

9. In theorem 1, what are the domains of $\beta$ and $\eta$? Moreover, in theorem 2, is this optimization always feasible? For example, what if $\theta$ is negative? The authors should clearly define the domain of a variable before using it.

10. In experiments, there are no comparisons with other approaches that consider safety guarantees. Therefore, it is hard to justify the contribution of this work. Moreover, the authors did not explain why there is an exception in Husky, in which case the safety probability is 0.800 (cannot meet the 0.95 threshold).

limitations: The authors just modify the output of a NNDM to satisfy a given safety probability. This approach does not generate a ``real'' control for the system. Therefore, it does not apply to dynamical systems.
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 provides probabilistic safety guarantees for dynamical systems. Noticing the safety issues in neural network based dynamical systems, this paper utilizes stochastic barrier function generated by SOS optimization and propose a safety probabilistic certificate for discrete step system. In the control synthesis problem, the paper also provides a lower bound of safety probability by local convex relaxation.
strengths_and_weaknesses: 1. Introducing the stochastic function into dynamical system learning is novel.

2. The narrative structure is clear.

3. It’s interesting to see many tricks in this paper to reformulate the problems.
questions: 1. I’m a bit concerned on the comparison metrics in the experiment, see my detailed question 1,2.

2. The computational time could be an issue for high dimensional system and finer partitions, but this is not a deal-breaker since the target is certification.
limitations: 1. Algorithm 1 has safe set as input, how to determine unsafe/safe region for each application? If that requires additional prior knowledge, then it might be unfair to compare the safety probability to safe region between synthesis controller and baseline model from imitation learning, since the former one already “knows” where the boundary is.

2. As for the verification comparison itself, I’m concerned why use the model from imitation learning as baseline instead of the expert controller. If the imitation learned model only saw the trajectory generated from an expert controller during training, then it’s reasonable it cannot handle corner cases. In line 311, it seems like your synthesis controller has been exposed to new data, then this is again not fair comparison. Feel free to correct me if I misunderstood your approach.  

3. In the verification results, I’m curious why larger architecture leads to worse Ps?
review_title: null

Meta-review: metareview: This paper introduces a new approach to synthesizing barrier certificates for the verification of systems whose dynamics are defined by a neural network. There was some confusion on the exact contribution, but it was clarified in the rebuttal that while there are many prior works that aim to verify systems with neural controllers, this is the first paper that aims to provide guarantees for systems where the dynamics themselves are modeled with a neural network. This is also connected to another concern expressed in the reviews, which is the absence of a proper baseline. As the authors pointed out, the lack of any competing systems that can handle NN dynamic models makes such a baseline comparison difficult, but nevertheless, the authors added an additional baseline as part of the rebuttal process. Overall, I agree with reviewers D3ig and JTrX that this is a technically solid paper acceptable for publication at NeurIPS. 
confidence: Less certain
Decision: Accept