Verified Safe Reinforcement Learning for Neural Network Dynamic Models

Summary

The paper proposes methods to learn formally verified neural network control policies for (continuous-space, discrete-time) non-linear dynamical systems, whose dynamics are also represented by a neural network. It builds on existing methods for NN verification, and their application to a k-step composition of NNs for the policy and dynamics. The key novel ideas of the paper are a variant of curriculum learning, built into an incremental policy synthesis approach over increasing time horizons, and a parameterized approach to representing state-dependent policies. Experimental results show improved performance on four benchmarks compared to five comparable techniques.

Strengths

- Clear and very well written paper. - Clearly presented and motivated novel ideas to improve performance on a challenging problem. - Comprehensive empirical evaluation with a good number of meaningful benchmarks and baselines, and a further ablation study in the appendix. - Impressive gains over baseline implementations.

Weaknesses

- The empirical results focus on the degree of safety achieved by different policies, but there seems to be no discussion of performance, e.g. runtime, or more directly the scalability of the various methods.

Questions

1. Relating to the stated weakness above, what is the experimental setup in terms of timeout (if any) used to compare tools, and what is the limiting factor in terms of the techniques' ability to synthesise safe policies?

Rating

7

Confidence

4

Soundness

3

Presentation

4

Contribution

3

Limitations

Yes

Summary

The authors primarily propose a novel method to learn verified safe control policies for nonlinear neural dynamical systems, aiming to achieve safety in the sense of bounded reachability. By leveraging memorization, forward reachability analysis, and differentiable reachability over-approximation, the authors effectively learn verified safe policies, and further introduce an incremental verification approach to enhance the efficiency of the learning process, enabling the acquisition of multiple verified initial state-dependent controllers.

Strengths

The manuscript proposes a method for learning a k-step verified safe neural network controller, aimed at maximizing the efficiency of systems with neural dynamics. In contrast to traditional approaches relying on forward-invariance proofs for safe control synthesis, the manuscript opts for the more practical bounded reachability verification, enabling the leveraging of state-of-the-art differentiable neural network approximation tools. The experimental results demonstrate that, across several dynamic system environments considering both static and moving obstacles, the proposed approach significantly outperforms the state-of-the-art safe reinforcement learning baselines. This highlights the advantages of the bounded reachability verification framework over the traditional forward-invariance guarantees, in terms of practical viability and performance when applied to systems with neural dynamics.

Weaknesses

The algorithm proposed in this manuscript lacks rationality analysis (1) Page 3.: “and required statistical assumptions“->”and requires statistical assumptions” (2) Page 4.: “which enable learning verified safe controllers over longer horizons K”->”which enables learning verified safe controllers over longer horizons K” (3) Page 4.: “In this work, we primarily utilize the α,β-CROWN toolbox”-> The α,β-CROWN toolbox should give a brief introduction here

Questions

(1) Can the author explain the soundness of the approach proposed in the manuscript? (2) The rationality of the experimental comparison baseline, why is it more interesting to compare with these methods? What are the maximum dimensions of the system security verification problem that can be solved by this method?

Rating

6

Confidence

4

Soundness

2

Presentation

3

Contribution

2

Limitations

The manuscript thoroughly discusses the limitations of the proposed methods, and the security guarantees provided are weaker compared to forward-invariance. However, bounded reachability offers a more practical approach to achieving verified safety, effectively realizing the safety of the entire event horizon in practice, and provides an alternative for the development of verified safe reinforcement learning.

Summary

This paper tackles the problem of synthesizing verified control policies for dynamical systems with the use of neural networks. The authors focus on nonlinear discrete-time system dynamics for which the use of neural networks is motivated by the challenge of reaching the goal without colliding with obstacles. To guarantee non-collision and maintain reasonable performance, the authors propose an approach of iteratively using an existing verification toolbox with curriculum-based lookahead. The approach is evaluated on the benchmarks from previous work.

Strengths

The approach of building a curriculum of horizons and re-using verification results from the previous steps is relatively novel and provides an interesting future direction. It is a significant improvement over the baselines that the proposed algorithm achieves 100% empirical safety. The decrease in performance is evident for several benchmarks and may exacerbate for a longer horizon. The paper is overall well-structured. However, a motivating example to guide the reader through the algorithm would be helpful.

Weaknesses

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. The authors motivate the choice of verification toolbox (a,b-CROWN) with its suitability for incremental verification. 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. 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.

Questions

1. Could the authors explain the choice of these particular benchmark problems to evaluate the approach on? 2. Is the state-space continuous or discrete for these benchmarks? (it appears it is continuous but only action-space is explicitly mentioned) 3. Which of the chosen benchmark problems particularly showcases the benefit of a longer-than-five step lookahead reachability? 4. How is the average reward computed (with verification over what horizon size)? Is it dependent on the verification horizon? 5. 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?

Rating

6

Confidence

4

Soundness

3

Presentation

3

Contribution

3

Limitations

The approach seems to have been specifically designed for verification tools that are suitable for incorporating into gradient-based learning. This can be a significant limitation to generalizability of the approach, since the authors do not discuss or evaluate what requirements the verification tools need to satisfy to be adopt the proposed approach. Based on the current presentation, the approach can only work with a,b-CROWN toolbox. If this is the case, it must be explicitly discussed as a limitation, it is, however, still an improvement over this particular domain. 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".

Summary

This paper studies safe reinforcement/control learning by optimization of long-horizon safety verification and learning multiple initial-state-dependent controllers. The authors propose several novel ideas, including a curriculum learning to increase the verification horizon, incremental verification, and split the initial region for multi-controllers training. A set of control tasks show the effectiveness of the approach, compared to other CMDP-based safe RL methods.

Strengths

1. The paper is well-written and easy to follow. 2. As far as I can tell, the idea of optimizing the verification horizon (curriculum learning) is novel and the experimental result is quite significant. 3. The approach is sound.

Weaknesses

1. the reviewer feels that incremental verification in this paper is quite common in the reachable set computation of neural network-controlled systems (NNCS), where the computed reachable set at $k$-th step will become the initial set for $k+1$ set computation. The authors may have to discuss their incremental verification vs. NNCS verification tools. To name a few tools, please refer to POLAR-Express[1], CORA[2], etc. 2. Splitting the state/initial space set into small grids for verification and controller synthesis/training is also common in the NNCS verification community. However, I have to admit that the design of multi-initial-state-dependent controllers is new to me. 3. The experiments only compare to the CMDP-based approach, it is unclear how the proposed approach compares to other control-theoretical methods, for instance, the CBF-based approaches. [1] Wang, Y., Zhou, W., Fan, J., Wang, Z., Li, J., Chen, X., ... & Zhu, Q. (2023). Polar-express: Efficient and precise formal reachability analysis of neural-network controlled systems. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. https://github.com/ChaoHuang2018/POLAR_Tool [2] https://github.com/TUMcps/CORA?tab=readme-ov-file

Questions

1. How to ensure that Algorithm 2 can terminate?

Rating

7

Confidence

4

Soundness

3

Presentation

3

Contribution

3

Limitations

The authors have addressed the limitations in the final part.