Verified Safe Reinforcement Learning for Neural Network Dynamic Models

We appreciate the reviewer's thoughtful comments and feedback. Our responses are below.

Question 1: What is the experimental setup in terms of timeout (if any) used to compare tools.

Response 1: We did not use any timeouts in our experiments, as all algorithms completed within reasonable time. Table 2 (in the Appendix) provides some timing details as an ablation study for our approach. We will add complete details in the revision.

Question 2: What is the limiting factor in terms of the techniques' ability to synthesise safe policies?

Response 2: The primary limiting factor is the scailablity of the verification tool for more complex domains, particularly when we include moving obstacles. This is of two types: 1) actual verification (e.g., after training is completed), and 2) differentiable verification that training requires. The latter is a more significant limiting factor than the former, and our approach would directly benefit from further advances in this area.

We thank the reviewer for the thoughtful comments and suggestions. Our responses are below.

Question 1: Can the author explain the soundness of the approach proposed in the manuscript?

Response 1: Soundness is a direct consequence of our use of a sound verification tool $(\alpha,\beta)$-CROWN, before declaring any of our initial-state-dependent controllers safe in the sense of $K$-step reachability (Lines 4-5 and 10-11 in Algorithm 2). We will clarify in the revision.

Question 2: The rationality of the experimental comparison baseline, why is it more interesting to compare with these methods?

Response 2: We chose recent baselines that cover the classical and SOTA approaches for a wide range of methods commonly used in Safe RL, including Lagrangian penalty, reward penalty, constrained PPO, and safe RL with reachability estimation. We also added a control-theoretic baseline using CBF in response to Reviewer kLbx (see Response 2 there); the performance of this baseline is comparable to our other baselines.

Question 3: What are the maximum dimensions of the system security verification problem that can be solved by this method?

Response 3: This depends greatly on the horizon $K$ that we wish to verify. For example, for small reachability horizon $K$, we can scale to thousands of dimensions. However, as meaningful reachability horizon entails larger $K$, this limits scalability, with verification tools the primary bottleneck. In general, there will be a tradeoff between state space dimension, verifiable horizon $K$, and fraction of state space that we can prove safety for.

We thank the reviewer for the thoughtful comments and suggestions. Our responses are below.

Question 1: The authors may have to discuss their incremental verification vs. NNCS verification tools; POLAR-Express[1], CORA[2], etc.

Response 1: Indeed, incremental verification is a well-explored idea in the verification literature, and we took inspiration from this literature. To our knowledge, we are the first to use this idea in training provably safe controllers. This entails several innovations:

1. We incrementally verify (and backpropagate the results) several steps ahead in a single training iteration (i.e., not merely from $k$ to $k+1$, but more generally from $k_i$ to $k_{i+1}$, where $k_{i+1} - k_i > 1$). Doing this more generalized version of incremental verification is crucial for training, significantly speeding it up, and reducing the likelihood of being stuck in "local optima" where inertia resulting from policy obtained for $k$ prevents verification from succeeding for $k+1$ (e.g., because we are too close to the unsafe region with velocity directed towards it).
2. Incremental verification is also an important component of our "Curriculum Learning with Memorization" training piece, where a significant challenge is backpropagation of $\mathcal{L}_{\text{bound}}$, which becomes GPU-intensive as the number of forward reachability steps, and consequently the neural network depth, increases. (GPU requirements for $K$-step backpropagation significantly exceed those for $K$-step verification.) Using incremental verifiation also allow us to efficiently extract useful gradient information for training. Furthermore, as shown in the ablation study in Table 2, the use of incremental verification during training significantly increases computational efficiency.

We will add the discussion regarding how our approach to incremental verification compares to, and differs from NNCS verification (e.g., POLAR-Express[1], CORA[2], etc.) in the revision.

Question 2: It is unclear how the proposed approach compares to other control-theoretical methods, for instance, the CBF-based approaches.

Response 2: We thank the reviewer for the suggestion. We ran an experiment with a CBF-based safe RL baseline from [3]. The results are below (where (M) stands for moving obstacles and (F) stands for fixed obstacles), which we will add to the revision, and are qualitatively similar to other baselines we consider.

[3] Emam, Yousef, Gennaro Notomista, Paul Glotfelter, Zsolt Kira, and Magnus Egerstedt. "Safe reinforcement learning using robust control barrier functions." IEEE Robotics and Automation Letters, 2022.

Question 3: How to ensure that Algorithm 2 can terminate?

Response 3: Ensuring termination entails simply setting a limit on the number of training iterations or setting a timeout, as is typically done in RL, or imposing an upper bound on the number of controllers the Algorithm can return. In our experiments, however, this proved unnecessary, as all cases terminated in reasonable time and with few initial-state-dependent controllers.

We thank the reviewer for the detailed comments and feedback. Our responses are below.

Question 1: A motivating example to guide the reader through the algorithm would be helpful.

Response 1: We appreciate the suggestion and will use vehicle avoidance as such an example in the revision.

Question 2: As can be seen from the ablation study, the runtime improvement is achieved with the proposed approach when the lookahead is longer than 5 steps. It is not clear if a long lookahead is required for the considered benchmarks.

Response 2: Below is the result where we only train for 5 steps lookahead.

This ablation (in comparison with the results in Table 1 in the paper) shows why considering lookahead with $K>5$ is critical for our benchmarks (especially 2D and 3D Quadrotor).

Question 3: It is not clear how much the proposed technique is constrained by the chosen toolbox or general enough to be adopted for other verification tools under certain assumptions.

Response 3: Our training framework is general and can in principle work with any differentiable verification technique; to our knowledge $(\alpha,\beta)$-CROWN is simply the best differentiable neural network verifier [5]. We will clarify in the revision.

Question 4: The choice of benchmark problems is not motivated in the evaluation section. The description of the benchmarks is not complete and requires looking into original papers. It would be appreciated to have complete system models stated formally in the appendix.

Response 4: Our benchmark problems are common benchmarks in the literature. For example, [3,4] use Quad2D, and [4] additionally uses Quad3D. The vehicle avoidance benchmark is a variant of CarGoal in the Safety Gym, used by PPO-PID, MBPPO, and RESPO baselines. We will add the description of the complete system models in the final version of the paper.

Question 5: Is the state-space continuous or discrete for these benchmarks?

Response 5: Both action and state space are continuous for all.

Question 6: How is the average reward computed? Is it dependent on the verification horizon?

Response 6: Average reward is computed over the entire episode horizon for each environnment, independently of the verification horizon (just as it is done in conventional RL). We will clarify in the revision.

Question 7: Is it possible to incorporate the proposed forward K-step reachability into the related reachability-based verification tools which do not yet consider it? What features or assumptions need to be satisfied?

Response 7: Yes. For training, the reachability-based verification toolbox needs to be differentiable. For verification, any reachability tool that supports NN-based dynamics and controllers would work.

Question 8: Open-access to data and code: the answer is "yes" when the data and code are anonymously open-source. If they are not yet open-sourced the answer should be "no yet".

Response 8: This is a good point; we do intend to make all code and data available on github.

[3] Emam, Yousef, Gennaro Notomista, Paul Glotfelter, Zsolt Kira, and Magnus Egerstedt. "Safe reinforcement learning using robust control barrier functions." IEEE Robotics and Automation Letters, 2022.

[4] Dawson, Charles, Zengyi Qin, Sicun Gao, and Chuchu Fan. "Safe nonlinear control using robust neural lyapunov-barrier functions." In Conference on Robot Learning, 2022.

[5] Brix, Christopher, Stanley Bak, Changliu Liu, and Taylor T. Johnson. "The fourth international verification of neural networks competition (VNN-COMP 2023): Summary and results.", 2023.