Venue: ICLR 2021 Conference

Reviews:

final_score: rating: 5: Marginally below acceptance threshold
review_content: ## Summary

The authors propose a safety verification algorithm based on reachability analysis and formal methods that is applicable to dynamics models and policies that are parameterized as neural networks. 

I find the problem(s) clear and well-motivated in general. There are many prior works in this area from outside the machine learning community, and I'm not totally convinced that this paper provides a substantial contribution over those works. 

## Strengths

 - The problem setup is clear and well-motivated
 - The methodology seems solid

## Weaknesses

 - The work is framed in the context of model-based RL, but since the model (including the estimate of the modeling error bound $d$) is assumed known, it would seem like this should be framed more squarely within the optimal control literature. Within this literature, there are many methods related to Safe MPC (e.g. [1], [2])  that it would seem are attempting to achieve the same objective as what is stated here. 

 - The central issue with all of the host of works on formal methods and reachability analysis for dynamical systems is that they don't scale to complex environments or dynamics. As a result, assumptions need to made such as monotonicity (work of Del Vecchio e.g. [3] [4]). The experiments that you show are very simplistic also (low dimensional and very simple/convex geometry). Is there something about this approach which allows us to make progress in terms of scaling these methods to real world problems.  

 - You argue that "Estimating modeling errors is an active area of research and is required for several existing works on safe RL (Akametalu et al., 2014; Gillula & Tomlin, 2012), and is complementary to our goal. Since the primary contribution of this work is the development of a reachable tube formulation for model-based controllers that use NNs, we rely on existing techniques (Moldovan et al., 2015) to estimate a conservative modeling error bound." but I find this assumption that you are given the modeling error bound diminishes the contribution of the work since everything downstream in your algorithm will be impacted by this value, which is hard to get in practice. 

## Minor Comments/Questions

 - Similar to comment above, what is a "model-based policy"? If you mean that it is derived from model-based RL method, why is this important?

- It would seem that taking the worst case modeling error, while able to provide guarantees (subject to the accuracy of the modeling error), also results in conservatism. A comment on this in the manuscript would be nice. 

- Part of the novelty that is claimed here is that the dynamics and policy are parametrized by neural networks, but what is the limitation of previous works on reachability analysis that would not permit a NN model to be used?

[1] Learning-based Model Predictive Control for Safe Exploration
T Koller, F Berkenkamp, M Turchetta, A Krause
Decision and Control (CDC), 2018 IEEE 57th Conference on

[2] Safe nonlinear trajectory generation for parallel autonomy with a dynamic vehicle model
W Schwarting, J Alonso-Mora, L Paull, S Karaman, D Rus
IEEE Transactions on Intelligent Transportation Systems 19 (9), 2994-3008

[3] M. R. Hafner and D. Del Vecchio, “Computational tools for the safety control of a class of piecewise continuous systems with imperfect information on a partial order,” SIAM J. Control Optim., vol. 49, pp. 2463–2493, 2011.

[4] R. Ghaemi and D. D. Vecchio, “Control for safety specifications of systems
with imperfect information on a partial order,
review_title: ICLR 2021

final_score: rating: 7: Good paper, accept
review_content: update after rebuttal: the answers were convincing, and the paper improved. 

Summary and Contribution

This work presents a novel approach for the safety verification of model based RL controllers. It uses a so-called reachability tube analysis to check whether unsafe states may be reached from the initial states of a (learned) model. In case unsafe states may be reached, a backward analysis determines the initial states that are safe (if they exist). Existing methods to measure potential modeling errors are taken into account. The efficacy of the method is demonstrated on two small examples.



Reasons for Score

With more details on the correctness, better literature study, and more experiments, the paper would be a clear accept. As of now, I see it as marginally above the acceptance threshold.

Strengths

- A novel method for verifying the safety of NN-based controllers
- A framework to incorporate inherent modeling errors

Weaknesses

- A better comparison to related work is in order
- The experiments are not very extensive, and it is not clear how to reproduce them.
- The correctness and completeness of the method, as well as the concrete assumptions on the NN architecture is unclear to me. 

Questions for Authors

- Please compare your work to the literature listed below. What is novel, how does it relate?
- What assumptions are being made on the neural network architecture? How can you obtain an exact and efficient method (soundness, completeness, global optima) for an potentially undecidable problem? 
- How would your method perform on state-of-the-art benchmark sets like from OpenAI or Deepmind?
- If you assume model-based RL, and the model is already there, why can't you construct a simpler model like a Markov decision process and reason directly about safety using sound and efficient methods like value iteration or linear programming? I understand you have a continuous state space (as given by the neural network), but do the experiments/examples require such a complicated model?

Detailed Comments

- related work

There is large body of related work on safety of (model-based) RL which has not been cited, for instance:


[1] Prashanth L, A., and Michael Fu. "Risk-sensitive reinforcement learning: A constrained optimization viewpoint." arXiv preprint arXiv:1810.09126 (2018)

[2] Zheng, Liyuan, and Lillian J. Ratliff. "Constrained upper confidence reinforcement learning." arXiv preprint arXiv:2001.09377 (2020).

[3] Eriksson, Hannes, and Christos Dimitrakakis. "Epistemic Risk-Sensitive Reinforcement Learning." arXiv preprint arXiv:1906.06273 (2019).

[4] Sebastian Junges, Nils Jansen, Christian Dehnert, Ufuk Topcu, Joost-Pieter Katoen:
Safety-Constrained Reinforcement Learning for MDPs. TACAS 2016: 130-146

[5] Nils Jansen, Bettina Könighofer, Sebastian Junges, Alex Serban, Roderick Bloem:
Safe Reinforcement Learning Using Probabilistic Shields. CONCUR 2020: 3:1-3:16

[6] Guy Avni, Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, Bettina Könighofer, Stefan Pranger:
Run-Time Optimization for Learned Controllers Through Quantitative Games. CAV (1) 2019: 630-649

[7] Mohammadhosein Hasanbeig, Alessandro Abate, Daniel Kroening:
Cautious Reinforcement Learning with Logical Constraints. AAMAS 2020: 483-491


[8] Mohammadhosein Hasanbeig, Alessandro Abate, Daniel Kroening:
Logically-Correct Reinforcement Learning. CoRR abs/1801.08099 (2018)


- correctness and efficiency

I don't really understand how you can incorporate nonconvex boundaries of the reachable tube. In any case, it should be an overapproximation. How is the efficiency of the method? How will it perform in practice? 

- experiments

It would be very nice to see how the method performs on well-known environments like the OpenAI safety gymn or the Deepmind safety gridworlds.


review_title: Interesting paper, questions about correctness, efficiency, related work, and experiments

final_score: rating: 7: Good paper, accept
review_content: # Summary

The paper presents a method for safety verification of trained model-based RL agents using reachable set analysis.
The method allows to both analyse whether any of the start states might end in an unsafe state, via the forward reachable tube, and to determine which start states do or do not end in an unsafe state, via the backward reachable tube.
Another claimed contribution is the first method to calculate the backward reachable tube on NNs.
An experimental evaluation is performed on to navigation environments.

# Comments to the Authors

Safety verification is a crucial topic for the acceptance and deployment of learned methods in control systems.
This paper contributes a method to verify a model-based RL controller in forwards and backwards direction, given the trained controller, a set of start and goal states and the constraints, i.e. a description of the unsafe states.

The method appears sound and is presented as straightforward, which will allow adoption in future works and potentially pratical application.
It includes the transfer of the backward reachable tube computation to NNs, which is central to the method.
Since it is outside my expertise, I do not verify the theoretical contributions of the paper.

Coming from the experimental evaluation, there are a few questions regarding the applicability of the method:
a) How would it handle dynamic environments, e.g. moving obstacles? As it is, only the deterministic trajectory of the agent appears to be evaluated.
b) How complex is the method computationally? What are the runtimes for the given examples?
c) In Figure 3 (right) it appears as if some green starting states are in an unsafe area. Is this a visual artifact or does the method not guarantee that all unsafe starting states are discovered (which was my impression before)?

Regarding the presentation of the paper, I understand that the authors are restricted by the conference format, but I would encourage to revise the selection of material for the main paper and the appendices.
The related work part of the paper might be benefit from some of the extended work in the appendix and the experiments could also be described more in detail.
At the same time, maybe the size of the flowchart could be improved or non-crucial parts of Sec. 3.2 extracted to the appendix.
Also, I think it is okay to put the paper + appendix as the main PDF on openreview, which makes the appendices more accessible for the readers on this platform.
review_title: Verification of model-based RL using reachable set analysis

final_score: rating: 3: Clear rejection
review_content: Summary: The paper studies the problem of safety verification of model-based RL controllers in continuous action&state spaces. The paper proposes a verification method based on reachable set analysis. The proposed method either verifies the controller to be safe or identifies the subset of initial states that are safe.

Strengths:

i) The motivation, organization and the overall writing of the paper are clear.

Weakness:

i) The problem of verifying properties of NN based controllers is studied in the literature [1,2,3,4,5,6,7,8,9,10,11,12,…], which is not discussed in detail in the paper (i.e., there is a paragraph present in the supplementary material). Moreover, there are no experimental comparisons made to any of these previous works.

ii) The tested experimental domains are not the best representatives of the control problems motivated in the paper. They are extremely small in size and do not really require NN approximation. As such, the resulting NN architectures are very small (as seen in the supplementary materials).

References:

[1] Verisig: verifying safety properties of hybrid systems with neural network controllers, Ivanov et al. HSCC-19.

[2] Learning and Verification of Feedback Control Systems using Feedforward Neural Networks, Dutta et al., 2018.

[3] Reachability Analysis and Safety Verification for Neural Network Control Systems, Xiang and Johnson, arvix 2018.

[4] Efficient Verification of Control Systems with Neural Network Controllers, Yang et al., ICVISP-19.

[5] Verifying Deep-RL-Driven Systems, Kazak et al. NetAI-19.

[6] Guarded Deep Learning using Scenario-based Modeling, Katz MODELSWARD 2020.

[7] Reachability Analysis for Neural Agent-Environment Systems, Akintunde et al, KR-18.

[8] Verification of RNN-Based Neural Agent-Environment Systems, Akintunde et al, AAAI-19.

[9] Reachability Analysis for Neural Feedback Systems using Regressive Polynomial Rule Inference, Dutta et al., HSCC-19.

[10] ReachNN: Reachability Analysis of Neural-Network Controlled Systems, Huang et al., TECS-19.

[11] Reachable Set Estimation and Safety Verification for Piecewise Linear Systems with Neural Network Controllers, Xiang et al., ACC-18.

[12] A Reachability Method for Verifying Dynamical Systems with Deep Neural Network Controllers, Julian et al., arvix, 2019.
review_title: Review of Safety Verification of Model-based RL Controllers

Meta-review: # Quality: 
The paper makes a good job of presenting the proposed algorithm, which seems interesting and solid.
However, the paper fails to place the proposed approach in the larger context of the existing literature.
In addition, only qualitative results are presented, without any comparison. 
As such, it is impossible to really understand the goodness of the proposed approach.

# Clarity: 
The paper is generally well-written and clear.

# Originality:
The proposed approach is novel to the best of the reviewers and my knowledge.

# Significance of this work: 
The paper deal with a very relevant and timely topic. However, as stated by the authors themself the paper is not concerned with high-dimensional systems, which is what would really differentiate this work compared to existing literature. In addition, the paper has no quantitative results nor comparisons against previous literature, and does not evaluate any of the standard benchmarks.

# Overall:
There is disagreement from the reviewers regarding the acceptance of this paper, and the overall score is very borderline. After thoroughly reading the paper, I agree with the evaluation of Reviewer 2 and 3 regarding the lack of comparisons and thus lean towards rejection.


Decision: Reject