Verified Safe Reinforcement Learning  for Neural Network Dynamic Models

Authors: junlin  wu
huan  zhang
yevgeniy  vorobeychik
Venue: NeurIPS_cc_2024_Conference
Published: 2024-05-12 00:36:01

Abstract: Learning reliably safe autonomous control is one of the core problems in trustworthy autonomy. However, training a controller that can be formally verified to be safe remains a major challenge. We introduce a novel approach for learning verified safe control policies in nonlinear neural dynamical systems while maximizing overall performance. Our approach aims to achieve safety in the sense of finite-horizon reachability proofs, and is comprised of three key parts. The first is a novel curriculum learning scheme that iteratively increases the verified safe horizon. The second leverages the iterative nature of gradient-based learning to leverage incremental verification, reusing information from prior verification runs. Finally, we learn multiple verified initial-state-dependent controllers, an idea that is especially valuable for more complex domains where learning a single universal verified safe controller is extremely challenging. Our experiments on five safe control problems demonstrate that our trained controllers can achieve verified safety over horizons that are as much as an order of magnitude longer than state-of-the-art baselines, while maintaining high reward, as well as a perfect safety record over entire episodes.

Main paper: 
 introduction: 
 The ability to synthesize safe control policies is one of the core challenges in autonomous systems. This problem has been explored from numerous directions across multiple disciplines, including control theory and AI [Achiam et al., 2017 , Dawson et al., 2022] . While considerable progress has been made, particularly when dynamics are linear [Wabersich and Zeilinger, 2018] , the ability to synthesize controllers that can be successfully verified to be safe while maintaining high performance in nonlinear dynamical systems remains a major open problem. Indeed, even the subproblem of safety verification in nonlinear systems is viewed in itself as a major challenge and is an active area of research, particularly for neural network controllers [Bastani et al., 2018 , Ivanov et al., 2019 , Wei and Liu, 2022] . State-of-the-art approaches for safe control synthesis, including most that leverage reinforcement learning [Gu et al., 2022] , typically only offer empirical evaluation of safety, and rely on safety proofs that hold either asymptotically (rather than for concrete problems) [Xiong et al., 2024] or under idealized assumptions which do not hold in practice [Berkenkamp et al., 2017] .Two common properties are typically leveraged in safety verification: forward invariance and reachability. The former aims to identify a set of starting subsets of safe states under which one-step (forward) dynamics remain in this (forward invariant) set. The latter computes the set of states that can possibly be reached after K steps of the dynamics for a given control policy, and checks whether it intersects with the unsafe set. Approaches for synthesizing (including those that do so using learning) safe policies almost exclusively aim to achieve verified safety through forward invariance. However, this has proved extremely challenging to employ beyond the simplest dynamics.We propose the first (to our knowledge) approach for learning K-step verified safe neural network controllers that also aim to maximize efficiency in systems with neural dynamics. While neural dynamics are clearly not universal, they can capture or effectively approximate a broad range of practical dynamical systems [Nagabandi et al., 2018] , and have consequently been the focus of much prior work in safe control and verification [Dai et al., 2021] . For example, consider the scenario of a drone navigating through a series of obstacles to reach a designated goal, requiring K = 50 steps to safely maneuver through the obstacles. We aim to train a controller that can reach the goal as fast as possible, while guaranteeing safety for the initial 50 steps, ensuring 1) the drone does not collide with any obstacles and 2) its angle remains within a predefined safe range.Our approach combines deep reinforcement learning with state-of-the-art differentiable tools for efficient reachability bound computation, and contains two key novel ingredients. The first is a novel curriculum learning scheme for learning a verified safe controller. This scheme takes advantage of the structure of the K-reachability problem at the root of our safety verification by creating a curriculum sequence with respect to increasing K. An important insight that is specific to the verification setting is that verification must work not merely for a fixed K, but for all steps prior, an issue we address by memorizing subsets of states who either violate, or nearly violate, safety throughout the entire K-step curriculum learning process. Additionally, to maintain both strong empirical and verified performance, we propose a novel loss function that integrates overall reward, as well as both traditional (empirical) safety loss along with the K-reachability bound. Our second innovation is to learn a collection of controllers that depend on the initial state, in contrast to typical approaches that focus on learning a single "universal" controller. The ability to allow for learning multiple controllers makes the verified learning problem considerably easier, as we can "save" controllers that work on a subset of initial states, and simply try learning a new controller for the rest, guaranteeing incremental improvement through the learning process. We further improve performance through incremental verification, which leverages information obtained in previous learning iterations.We evaluate the proposed approach in five control settings. The first two are lane following and obstacle avoidance, both pertaining to autonomous driving. The last three involve drone control with obstacle avoidance. Two of these consider fixed obstacles, while the third aims to avoid even moving obstacles (with known dynamics). We show that the proposed approach outperforms five state-of-the-art safe control baselines in the ability to achieve verified safety without significantly compromising overall reward (efficiency). In particular, our approach learns controllers that can verify K-step safety for K up to an order of magnitude larger than the prior art and maintains a perfect safety record for K far above what we verify, something no baseline can achieve.In summary, we make the following contributions:1. A framework for safe optimal control that combines both finite-horizon verified (worst-case) and empirical (average-case) safety constraints. 2. A novel curriculum learning approach that leverages memorization, forward reachability analysis, and differentiable reachability overapproximation for efficiently learning verified safe policies. 3. An approach for learning a collection of control policies that depend on the initial state which enables significant improvements in verified safety horizon over large initial state sets S 0 . 4. An incremental verification approach that leverages small changes in gradient-based learning to improve verification efficiency during learning. 5. An extensive experimental evaluation that demonstrates the efficacy of the proposed approach in comparison with five state-of-the-art safe RL baselines.Related Work: Safe reinforcement learning has been extensively studied through the lens of constrained Markov decision process (CMDP)-based approaches, which represent cost functions as constraints and aim to maximize reward while bounding cost, using approaches such as Lagrangian and penalty methods, and constrained policy optimization [Achiam et al., 2017 , Stooke et al., 2020 , Ma et al., 2022 , Jayant and Bhatnagar, 2022 , Yu et al., 2022 , So and Fan, 2023 , Ganai et al., 2024 ].An alternative control-theoretic perspective aims to ensure stability or safety using Lyapunov and control barrier functions. For example, Dawson et al. [2022] used a learning-based approach to find robust control Lyapunov barrier functions; Chow et al. [2018] constructed Lyapunov functions to solve CMDPs; [Wang et al., 2023a] proposed soft barrier functions for unknown and stochastic environments; and Alshiekh et al. [2018] created safety shielding for safe RL agents. These approaches, however, provide no practical formal safety guarantee for neural network controllers. In addition, some work on provably safe RL focuses on the probabilistic setting [Berkenkamp et al., 2017 , Jansen et al., 2020 , Xiong et al., 2024] and required statistical assumptions, whereas our work aims for strict deterministic safety guarantees over a finite horizon.Among existing works focusing on safe RL with formal guarantees, Fulton and Platzer [2018] apply a theorem prover for differential dynamic logic to guarantee safety during runtime. Noren et al. [2021] and Wei et al. [2022] consider forward safety invariance for systems with uncertainty. Kochdumper et al. [2023] propose to project actions to safe subspace using zonotope abstraction and mixed-integer programming (MIP). However, these approaches do not readily apply to neural network controllers.For systems involving neural networks, Wei and Liu [2022] applied integer programming formulation for neural networks to solve an MIP problem to find safe control actions satisfying forward invariance; Bastani et al. [2018] extracted decision-tree-based policies for RL to reduce verification complexity; and Ivanov et al. [2019] used hybrid system verification tools to model deep neural networks. Our work differs from these and similar approaches because we consider forward reachability guarantees for neural network controllers in neural nonlinear systems.We make extensive use of neural network verification tools. Early work in this vein used SMT [Katz et al., 2017 , Huang et al., 2017] or MIP-based [Tjeng et al., 2019] approaches to solve this problem, but their scalability is extremely limited. Significant progress has been made in developing techniques to formally verify the properties of large neural networks through overapproximation, such as bound propagation [Zhang et al., 2018 , Gowal et al., 2018 , Xu et al., 2021] , optimization [Qin et al., 2019 , Dvijotham et al., 2018 , 2020] , and abstract interpretation [Gehr et al., 2018 , Singh et al., 2019 , Katz et al., 2019 , Lopez et al., 2023] . Recently, most verifiers have adopted branch-and-bound based approaches to further enhance their performance [Wang et al., 2021 , Kouvaros and Lomuscio, 2021 , Ferrari et al., 2022 , Zhang et al., 2022] . Our approach makes use of differentiable overapproximation methods known collectively as α,β-CROWN [Wang et al., 2021 , Zhang et al., 2022] (implemented with the auto_LiRPA package), and takes advantage of the particular structure of these verification approaches in applying incremental verification to significantly speed up safe controller learning.Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?Answer: [Yes] Justification: Abstract and Introduction Section Guidelines:• The answer NA means that the abstract and introduction do not include the claims made in the paper. • The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or NA answer to this question will not be perceived well by the reviewers. • The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings. • It is fine to include aspirational goals as motivation as long as it is clear that these goals are not attained by the paper. 
preliminaries: 
 Constrained Markov Decision Process (CMDP): We consider a deterministic Constrained Markov Decision Process (CMDP) defined by the tuple (S, A,F, R, γ, C 1 , C 2 , . . . , C m , d 1 , d 2 , . . . , d m ),where: S is a set of states, A is a set of actions, F : S × A → S is the deterministic state transition function, R : S × A → R is the reward function, C i : S × A → R is the cost function for the i-th constraint, d i is the cost limit for the i-th constraint, and γ ∈ [0, 1) is the discount factor. A policy π : S → A is a mapping from states to actions. A trajectory is a sequence of states and actions generated by following a policy π from some initial state s 0 ∈ S 0 ⊆ S, which can be represented as a sequence τ = (s 0 , a 0 , s 1 , a 1 , s 2 , a 2 , . . . ) where s t ∈ S, a t = π(s t ) for all t, s t+1 = F (s t , a t ), a reward r t = R(s t , a t ) and a cost c t = i∈[m] C i (s t , a t ) are received after each action.We denote π θ as the policy that is parameterized by the parameter θ. A common goal for CMDP is to learn a policy π θ that maximizes a discounted sum of rewards J (π θ ) while ensuring that expected discounted costs J Ci (π θ ) do not exceed the cost limit d i , ∀i ∈ [m]. Formally, CMDP is to solve the below optimization problem:EQUATIONwhereJ (π θ ) = E τ ∼π [ ∞ t=0 γ t R(s t , a t )] and J Ci (π θ ) = E τ ∼π [ ∞ t=0 γ t C i (s t , a t )]. Verified Safe CMDP: We define the state space as the union of predefined safe and unsafe states, denoted as S = S safe ∪ S unsafe . We assume that the transition function F is represented by a ReLU neural network, and is known for verification purposes. This assumption is very general, as many known dynamical systems can be represented exactly or approximately using ReLU neural networks [Gillespie et al., 2018 , Pfrommer et al., 2021 , Dai et al., 2021 , Liu et al., 2024] . Our objective is to train a controller that not only satisfies safety constraints empirically at decision time, but also ensures verified safety for the first K steps.Formally, we aim to solve the following optimization problem:max θ J (π θ ) (2a) s.t. J Ci (π θ ) ≤ d i , ∀i ∈ [m] (empirically satisfied) (2b) s t ∈ S safe , ∀t ∈ [K] (mathematically verified) (2c) s t+1 = F (s t , a t ), a t = π θ (s t ), s 0 ∈ S 0 ⊆ S safe (2d)In particular, we aim to solve (2) for high values of K and large sets of verified safe initial states S 0 , while preserving a high objective value. Note that for a given controller, (2c) can also be interpreted as a set of forward reachability verification problems. However, our interest here extends beyond mere verification; we aim to train (synthesize) a controller that can be efficiently verified for safety.For simplicity, we restrict attention to d i = 0 for all i; however, our approach can be directly applied to arbitrary values of d i .In this work, we primarily utilize the α,β-CROWN toolbox [Xu et al., 2021 , Wang et al., 2021] for neural network (NN) verification; however, our training framework is general and, in principle, can work with any differentiable verification technique. Let F k,π θ denote the k-step forward function (iterative composition of F ) under policy π θ . For example,s 1 = F 1,π θ (s) = F (s, π θ (s)), F 2,π θ (s) = F (s 1 , π θ (s 1)), and so on. Correspondingly, we represent the k-step forward reachable regions returned by the NN verifier for an initial state set S as F k,π θ Bound (S), which is typically represented as a box.Question: Does the paper discuss the limitations of the work performed by the authors?Answer: [Yes] Justification: we discuss the primary limitation of the work in the conclusion.Guidelines:• The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper. • The authors are encouraged to create a separate "Limitations" section in their paper.• The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be. • The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on a few datasets or with a few runs. In general, empirical results often depend on implicit assumptions, which should be articulated. • The authors should reflect on the factors that influence the performance of the approach.For example, a facial recognition algorithm may perform poorly when image resolution is low or images are taken in low lighting. Or a speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon. • The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size. • If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness. • While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an important role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations. 
approach: 
 The problem of learning verified safe control over a target horizon K entails three key technical challenges. The first is that as K grows, the differentiable overapproximation techniques for reachability verification become looser, making it difficult to verify K beyond very small horizons. Second, while control policies π depend on state, it is difficult to find a single universal controller that can achieve verified safety for each starting state in S 0 . Our approach addresses these challenges through three technical advances: 1) curriculum learning with memorization and 2) incremental verification, which enable learning verified safe controllers over longer horizons K, and 3) iterative learning a collection of controllers customized for subsets of S 0 , which addresses the third challenge above.Curriculum Learning with Memorization: Curriculum learning is an iterative training strategy where the difficulty of the task increases as training progresses [Bengio et al., 2009, Wu and Vorobeychik, 2022] . At a high level, for a problem targeting K-step verified safety, training can be divided into K phases, with each phase k aiming to achieve verified safety at the corresponding k-th forward step. In the k-th phase, we conduct formal verification against the k-th step safety, filter out regions that cannot be verified, and use them for further training. As k increases, the task difficulty also increases, mainly due to the forward NN F k,π θ becoming deeper. For a deeper NN and a fixed branching budget, the output bounds become looser [Wang et al., 2021] , increasing the likelihood of intersections with unsafe regions. However, the ability to verify safety in prior steps enables us to tailor a controller that closely aligns with the fixed NN dynamics, thereby achieving tighter bounds. This process captures the essence of curriculum learning.Nevertheless, our approach deviates from traditional curriculum learning in a way that is quite consequential for our setting: we aim to ensure that a controller is verified as safe not only for the k-th step but also maintains safety for all prior steps. Consequently, during our curriculum learning process, we store states that are close to being unsafe in each phase in a buffer, effectively memorizing information about regions that potentially violate safety. These states, along with the unverified states at the current phase, are then incorporated into the training process, helping to ensure safety across the entire K-step horizon. Our curriculum training framework is detailed in Algorithm 1.The process begins by initializing the policy π θ with a pre-trained policy using safe RL algorithms (Line 3). We then split the initial region S 0 into a grid G 0 (Line 4). We assume S 0 is a m-dimensional box centered at s c ∈ R m with a radius r ∈ R m , i.e., S 0 = [s c -r, s c + r]. We prioritize splitting the dimensions that are directly implicated in safety constraints, thereby taking advantage of the Algorithm 1 Curriculum Learning with Memorization 1: Input: target safety horizon K, initial region S 0 , unsafe region S unsafe , max attempt n max 2: Output: controller π θ 3: Initialize π θ with pre-trained policy, buffer B = {} 4: Split initial region S 0 into grid G 0 5: for k = 1, 2, . . . , K do 6: n train ← 0 7: S uc ← F k,π θ Bound (G 0 ) ∩ Sn train ← n train + 1 11: S uc ← F k,π θ Bound (G 0 ) ∩ S unsafe 12:end while13: Filter regions S k ⊆ G 0 such that dist(F k,π θ Bound (S k ), S unsafe ) < ϵ, store (S k , k) in buffer B 14: end for typical structure of safety constraints that only pertain to a small subset of state variables. For instance, in drone control for obstacle avoidance, we prioritize splitting the location and angle axes. Next, we design a cost function C R for regions where C R (S) = 0 if S ∩ S unsafe = ∅, and C R (S) > 0 otherwise. A positive C R means region S intersects with S unsafe , while C R = 0 indicates S is safe. For example, if the task is to avoid the region [a, b], and the output bounds are given byx B = [x lb , x ub ], we can define C R (x B ) = max(x ub -a, 0) • max(b -x lb , 0). We then calculate the gradient ∂C R (F t,π θBound (S 0 ))/∂r for a chosen value of t and proceed to split along the dimensions with the largest gradient values, as a larger gradient indicates a higher likelihood of reducing the cost C R . We continue this process, keeping the total number of grid splits within a predetermined budget, and stop splitting once the budget is reached.For each training phase k, we monitor the training rounds (n train ) as well as the k-step forward reachable regions returned by the verifier that are identified as unsafe (S uc ). Each phase is conducted for a maximum of n max rounds or until verified k-step safety is achieved, that is, when S uc = ∅ (Line 8). At the end of each training phase, we also filter out regions S k ⊆ G 0 where F k,π θ Bound (S k ) are within ϵ distance to the unsafe regions. These regions are then stored in the buffer B (Line 13). We include these critical regions in the training set for each reinforcement learning update to enhance verified safety across the entire horizon. During this process, we optionally use the Branch-and-Bound algorithm [Everett et al., 2020 , Wang et al., 2021] to refine G 0 up to a predetermined branching limit, which helps achieve tighter bounds.For each RL update, we use a loss function that integrates the standard safe RL loss with a k-phase loss for bounds (Line 9), whereEQUATIONHere, L SafeRL is the standard safety RL loss, and L Bound denotes the loss that incentivizes ensuring the output bounds returned by the verifier remain within the safe region. If both S uc is k-step safe and∀(S i , i) ∈ B, S i is i-step safe, then L Bound (S uc ∪ B) = 0, otherwise, L Bound (S uc ∪ B) > 0.In practice, we clip L Bound (S uc ∪ B) to ensure it remains within a reasonable range for training stability. The regularization parameter λ is calculated based on the magnitude of L SafeRL and L Bound , with λ = min(λ max , a r • L SafeRL /L Bound ), where λ max and a r are hyperparamters. This approach helps maintain the effectiveness of bound training, especially when L Bound is small. Furthermore, we cluster elements in B into categories so that we do not need to construct a computational graph for all i < k. Specifically, we merge all S i for i 1 ≤ i ≤ i 2 into the i 2 category, meaning the elements inB are now (∪ i1≤i≤i2 S i , i 1 , i 2 ) instead of (S i , i).It is important to note that while our training scheme targets K-step verified safety, the policy returned by Algorithm 1 does not necessarily guarantee it. We address this issue by learning initial-statedependent controllers as described below. Furthermore, the computation of L Bound is computationally intensive. Its backpropagation requires constructing computational graphs for the k-th step forward NN F k,π θ Bound , as well as for all i-th step forward NNs corresponding to each (S i , i) ∈ B. These NNs become increasingly deep as k grows, causing the computational graphs to consume memory beyond the typical GPU memory limits. We will address this next.Incremental Verification: Above we discussed the challenge presented by the backpropagation of L bound , which is GPU-memory intensive and does not scale efficiently as the target K-step horizon increases. To mitigate these issues, we propose the use of incremental verification to enhance computational efficiency and reduce memory consumption. While incremental verification is wellexplored in the verification literature Wang et al. [2023b] , Althoff [2015] , to our knowledge, we are the first to apply it in training provably safe controllers.At a high level, to calculate the reachable region for a k target step, we decompose the verification into multiple phases. We begin by splitting the k target horizon into intervals defined by 0< k 1 < k 2 < • • • < k n = k target .We first calculate the reachability region for the k i step and then use its output bounds as input to calculate the reachable region for the k i+1 step. This approach ensures that the computational graph is only built for the (k i+1 -k i ) step horizon when using α,β-CROWN.Unlike traditional incremental verification, which typically calculates the reachable region from k to k + 1, we incrementally verify and backpropagate several steps ahead in a single training iteration (i.e., from k i to k i+1 , where k i+1 -k i > 1). This generalized version of incremental verification is essential for training, as it significantly accelerates the process and reduces the likelihood of becoming trapped in "local optima," where inertia from the policy obtained for k prevents successful verification for k + 1 (e.g., due to proximity to the unsafe region with velocity directed toward it).For the bounds used in neural network training, we effectively build the computational graph and perform backpropagation using a neural network sized for (k n -k n-1 ) steps' reachability, which is independent of k target . This significantly reduces GPU memory usage. Since F k,π θ is an iterative composition of F under the same policy π θ , the bound for k n-1 steps tends to be tight. Moreover, when training π θ to tighten these bounds, the overall bound for the entire k target horizon becomes increasingly tight.Initial-State-Dependent Controller: While curriculum learning above includes verification steps, it does not guarantee verified safety for the controller over the entire K-step horizon. In this section, we propose using an initial-state-dependent controller to address this issue. For example, in a vehicle avoidance scenario, different initial conditions, such as varying speeds and positions, may correspond to different control strategies. We introduce a mapping function h : S 0 → Θ, which maps each initial state s 0 ∈ S to a specific policy π h(s0) . The underlying idea is that training a verifiable safe policy π θ over the entire set of initial states S 0 is inherently challenging. However, by mapping each initial state to a specific set of parameters, we can significantly enhance the expressivity of the policy. This approach is particularly effective in addressing and eliminating corner cases in unverifiable regions.At a high level, the mapping and parameter set Θ are obtained by first performing comprehensive verification for the controller output from Algorithm 1 over the entire K-step horizon. We then filter unverified regions, cluster them, and fine-tune the controller parameters θ for each cluster. We store these fine-tuned parameters in the parameter set Θ. This iterative refinement process continues until for every s 0 ∈ S 0 , there exists a θ ∈ Θ such that π θ is verified safe for the entire K-step horizon. The detailed algorithm is presented in Algorithm 2.The algorithm starts with verifying the policy π θ obtained from Algorithm 1. The function VERIFYSAFE(π θ , S 0 , K) (Line 4) performs verification of policy π θ for initial states S 0 for the entire horizon K. This verification process identifies and categorizes regions into verified safe areas, S V safe , and areas identified as unsafe, S V unsafe . Notably, the union of these regions covers all initial states, meaning S V safe ∪ S V unsafe = S 0 . After verifying that any state s 0 ∈ S V safe is guaranteed to be safe under policy π θ , we record (S V unsafe , π θ ) in the mapping dictionary H (Line 5). Next, we address the unsafe regions S V unsafe that lack a corresponding verified safe controller. We first cluster them based on the type of safety violation (Line 7). The reason for clustering is that regions with similar safety violations are more likely to be effectively verified safe by the same controller. For instance, in a scenario involving navigation around two obstacles, we could potentially identify up to three clusters: the first corresponding to grids that can lead to collisions with obstacle 1, the second includes grids associated with collisions with obstacle 2, and the third is the set of grids that may lead to collisions with both. Given the finite number of safety constraints, the number of possible clusters is also finite. Although the theoretical maximum number of clusters grows exponentially Algorithm 2 Initial-State-Dependent Controller 1: Input: target safety horizon K, policy π θ 2: Output: mapping dictionary H, which includes the mapping h and parameter set Θ 3: Initialize H = {} 4: (S V safe , S V unsafe ) ← VERIFYSAFETY(π θ , S 0 , K) 5: Store (S V safe , θ) in mapping dictionary H 6: while S V unsafe ̸ = ∅ do 7:{S 1 , S 2 , . . . , S I } ← CLUSTERREGION(S V unsafe ) // cluster based on safety violation 8:for i = 1, 2, . . . , I do 9:π θ ′ ← TRAINPOLICY(π θ , S i , K) 10: (S V safe,i , S V unsafe,i ) ← VERIFYSAFETY(π θ ′ , S i , K) 11:Store (S V safe,i , θ ′ ) in mapping dictionary H 12:end for 13:S V unsafe ← i S Vunsafe,i 14: end while with the number of safety constraints, in practice, this number is significantly smaller. This is due to the fact that the controller, being pretrained, is less likely to violate multiple or all constraints simultaneously. We then fine-tune the controller for the initial states in each cluster using Algorithm 1. This fine-tuning process is typically fast, as the initial policy is already well-trained. We store each initial state region and its corresponding verified safe policy in the mapping dictionary H. This clustering and fine-tuning process continues until a verified safe policy exists for every s 0 ∈ S 0 .At decision time, given an initial state s 0 , we first identify the pair (S V safe , π θ ) in the mapping dictionary H where s 0 ∈ S V safe , then use the corresponding verified safe controller π θ . Note that the soundness of the algorithm directly follows from our use of the sound verification tool α,β-CROWN.Question: For each theoretical result, does the paper provide the full set of assumptions and a complete (and correct) proof?Answer: [NA]Answer: [Yes] Justification: We will provide all code and data on github, along with documentation, to facilitate reproduction of the experiments if the paper is accepted for publication. Guidelines:• The answer NA means that paper does not include experiments requiring code. • The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster. • The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology. • If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML). 
experiment setup: 
 We evaluate our proposed approach in five control settings: Lane Following, Vehicle Avoidance, 2D Quadrotor (with both fixed and moving obstacles), and 3D Quadrotor [Kong et al., 2015 , Dai et al., 2021] . The dynamics of these environments are approximated using NN with ReLU activations. We use a continuous action space for those discrete-time systems. In each experiment, we specify the initial region S 0 for which we wish to achieve verified safety. We then aim to achieve the maximum K for which safety can be verified. We evaluate the approaches using four metrics: 1) Verified-K : the percentage of regions in S 0 that can be verified for safety over K steps; 2) Verified-Max: the maximum number of steps for which all states in S 0 can be verified as safe; 3) Emp-k : the percentage of regions in S 0 that are empirically safe for k steps, obtained by sampling 10 7 datapoints from the initial state S 0 . This is evaluated for both k = K (the number of steps we are able to verify safety for) and k = T (total episode length); 4) Avg Reward: the average reward over 10 episodes, with both mean and standard deviations reported. Note that the average reward is computed over the entire episode horizon for each environment, independently of the verification horizon, as in conventional reinforcement learning.We compare the proposed verified safe RL (VSRL) approach to six baselines: 1) PPO-Lag, which utilizes constrained PPO with the standard Lagrangian penalty [Achiam et al., 2017] ; 2) PPO-PID, which employs constrained PPO with PID Lagrangian methods [Stooke et al., 2020] ; 3) CAP, which adopts model-based safe RL with an adaptive penalty [Ma et al., 2022] ; 4) MBPPO, which applies model-based safe RL with constrained PPO [Jayant and Bhatnagar, 2022]; 5) CBF-RL, which is a Control Barrier Function (CBF)-based safe reinforcement learning approach [Emam et al., 2022] ; and 6) RESPO, which implements safe RL using iterative reachability estimation [Ganai et al., 2024] .Next, we describe the four autonomous system environments in which we run our experiments. Further experimental setup details are provided in Appendix A.2. Lane Following: Our lane following environment follows the discrete-time bicycle model [Kong et al., 2015] . The model inputs are 3-dimensional (x, θ, v), where x is the lateral distance to the center of the lane, θ is the angle relative to the center of the lane, and v represents the speed. The objective is to maintain a constant speed while following the lane, meaning the system equilibrium point is (x, θ, v) = (0, 0, v target ). The safety constraints are 1) x stays within a maximum distance from the lane center (∥x∥ ≤ d max ), 2) θ remains within a predefined range (∥θ∥ ≤ θ max ), and 3) v does not exceed the maximum threshold (v ≤ v max ).Vehicle Avoidance: Our vehicle avoidance environment features a vehicle moving on an x-y plane, with 4-dimensional inputs (x, y, θ, v). Here, (x, y) represents the location of the vehicle on the plane, θ is the angle relative to the y-axis, and v is the speed. In this setting, we have five moving obstacles, each moving from one point to another at constant speed. Each obstacle is represented as a square.Additionally, safety constraints are set for the speed (v ≤ v max ) and angle (∥θ∥ ≤ θ max ). The task is to navigate the vehicle to a designated location while following safety constraints.2D Quadrotor: For the 2D quadrotor environment, we follow the settings in Dai et al. [2021] . The input is 6-dimensional (y, z, θ, ẏ, ż, θ), where (y, z) represents the position of the quadrotor on the y-z plane, and θ represents the angle. The action space is 2-dimensional and continuous; the actions are clipped within a range to reflect motor constraints. Our safety criteria include an angle constraint (∥θ∥ ≤ θ max ) and a minimum height constraint to prevent collision with the ground (y ≥ y min ). We consider two scenarios for obstacles: fixed and moving. For fixed obstacles, there are five rectangular obstacles positioned in the y-z plane. For moving obstacles, there are five obstacles that moves from one point to another at constant speed, each represented as a square.3D Quadrotor: Our 3D quadrotor environment features a 12-dimensional input space, represented as (x, y, z, ϕ, θ, ψ, ẋ, ẏ, ż, ω x , ω y , ω z ). The action space is 4-dimensional and continuous; the actions are clipped within a range to reflect motor constraints. Here, (x, y, z) denotes the location of the quadrotor in space, ϕ is the roll angle, θ is the pitch angle, and ψ is the yaw angle, ω x , ω y , ω z represent the angular velocity around the x, y, and z axes, respectively. The task is to navigating towards the goal while adhering to safety constraints, which include avoiding five obstacles represented as 3D rectangles. The details for the environment settings are deferred to the Appendix.As shown in Table 1 , our approach significantly outperforms all baselines in terms of verified safety, as well as empirical safety over the entire episode horizon. Furthermore, the only environment in which VSRL exhibits a significant decrease in reward compared to baselines is lane following; for the rest, it achieves reward comparable to, or better than the baselines.Specifically, in the lane following environment, the proposed VSRL approach achieves verified 80-step safety using a single controller (i.e., |Θ| = 1). This is an order of magnitude higher K than all baselines (which only achieve K ≤ 8). While all baselines obtain a safety record of over 99.9% over the entire episode (K = 500), our approach empirically achieves perfect safety.For vehicle avoidance, we achieve verified 50-step safety using two controllers (i.e., |Θ| = 2); in contrast, the best baseline yields only K = 13. We also observe considerable improvements in both verified and empirical safety over the baseline approaches: for example, the best verified baseline (CAP) violates safety over 10% of the time over the full episode length, whereas VSRL maintains a perfect safety record. In this case, VSRL also achieves the highest reward.For the 2D Quadrotor environment with fixed and moving obstacles, we are able to achieve verified 50-step safety using four and two controllers, respectively. The best baseline achieves only K = 14 in the case of fixed and K = 8 in the case of moving obstacles (notably, different baselines are best in these cases).Finally, in the most complex 3D Quadrotor environment, we achieve verified safety for K = 15, but empirically maintain a perfect safety record for the entire episode durection. The best baseline achieves verified safety for only K = 4, but is empirically unsafe over 40% of the time during an episode. Even the best safety record of any baseline is unsafe nearly 12% of the time, and we can only verify its safety over a horizon K = 3.Ablation Study: We evaluate the importance of both incremental verification and using multiple initial-state-dependent controllers as part of VSRL. As shown in the Appendix (Section A.1), the former significantly reduces average verification time during training, whereas the latter enables us to greatly boost the size of the initial state region S 0 for which we are able to achieve verify safety. 
conclusion: 
 We present an approach for learning neural network control policies for nonlinear neural dynamical systems. In contrast to conventional methods for safe control synthesis which rely on forward invariance-based proofs, we opt instead for the more pragmatic finite-step reachability verification. This enables us to make use of state-of-the-art differentiable neural network overapproximation tools that we combine with three key innovations. The first is a novel curriculum learning approach for maximizing safety horizon. The second is to learn multiple initial-state-dependent controllers.The third is to leverage small changes in iterative gradient-based learning to enable incremental verification. We show that the proposed approach significantly outperforms state of the art safe RL baselines on several dynamical system environments, accounting for both fixed and moving obstacles.A key limitation of our approach is the clearly weaker safety guarantees it provides compared to forward invariance. Nevertheless, our results demonstrate that finite-step reachability provides a more pragmatic way of achieving verified safety that effectively achieves safety over the entire episode horizon in practice, providing an alternative direction for advances in verified safe RL to the more typical forward-invariance-based synthesis. 
safeguards: 
 Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?Answer: [NA] Justification: The paper is about safe reinforcement learning, and poses no such risk.Guidelines:• The answer NA means that the paper poses no such risks.• Released models that have a high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters. • Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images. • We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make a best faith effort.12. Licenses for existing assets Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?Answer: [Yes] Justification: The paper references the Auto_Lirpa codebase and associated research papers describing it.Guidelines:• The answer NA means that the paper does not use existing assets.• The authors should cite the original paper that produced the code package or dataset.• The authors should state which version of the asset is used and, if possible, include a URL. • The name of the license (e.g., CC-BY 4.0) should be included for each asset.• For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided. • If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswithcode.com/datasets has curated licenses for some datasets. Their licensing guide can help determine the license of a dataset. • For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided. 
 
 Appendix: In this section, we conduct an ablation study to evaluate the importance of both incremental verification and the use of multiple initial-state-dependent controllers as part of the VSRL approach. Table 2 presents the ablation study results for incremental verification. To ensure a fair comparison, we record the runtime for 20 training epochs with only one region from the grid split for all environments.In practice, this process can be run on GPUs in parallel for multiple regions. Given that the neural network structures for the 2D Quadrotor environment with both moving and fixed obstacles are the same, the runtime results are similar; therefore, we report these collectively as 2D Quadrotor. The results indicate that incremental verification significantly reduces the average verification time during training. Without incremental verification, the verification time increases rapidly as the number of steps increases.Table 3 : Percentage of regions in S 0 that can be verified for safety for K steps (Verified-K).Veh. Avoid. (↑) 2D-Quad (F) (↑) 2D-Quad (M) (↑) 3D-Quad (F) (↑)Single Ctrl. 99.0 97.6 96.9 74.7 Multi Ctrl.100.0 100.0 100.0 100.0Table 3 shows the ablation study results for using multiple initial-state-dependent controllers. We report results for the Vehicle Avoidance environment (Veh. Avoid.), 2D Quadrotor with fixed obstacles (2D-Quad (F)), moving obstacles (2D-Quad (M)), and 3D Quadrotor (3D-Quad (F)). We exclude the Lane Following environment from this comparison, as only one controller was used there to achieve 100% verified safety. The results demonstrate that using multiple controllers significantly enhances the ability to achieve verified safety across a larger initial state region S 0 .Lane Following Our lane following environment follows the discrete-time bicycle model [Kong et al., 2015 ]ẋ = v cos(θ + β) ẏ = v sin(θ + β) θ = v l r sin(β) v = a β = tan -1 l r l f + l r tan(δ f )where we set the wheel base of the vehicle to 2.9m. The model inputs are 3-dimensional (x, θ, v), where x is the lateral distance to the center of the lane, θ is the angle relative to the center of the lane, and v represents the speed. The objective is to maintain a constant speed while following the lane, meaning the system equilibrium point is (x, θ, v) = (0, 0, v target ). The safety constraints are 1.x stays within a maximum distance from the lane center (∥x∥ ≤ d max ), 2. θ remains within a predefined range (∥θ∥ ≤ θ max ), 3. v does not exceed the maximum threshold (v ≤ v max ).The parameters are set as d max = 0.7, θ max = π/4, and v max = 5.0. The initial regionsS 0 is x ∈ [-0.5, 0.5], θ ∈ [-0.2, 0.2], v ∈ [0.0, 0.5].The reward received at each step is measured as the distance to the equilibrium point. More specifically, for a state that is of distance d to the target equilibrium point, the reward is e -d . For VSRL training, our controller is initialized using a controller pretrained with a safe RL algorithm. When training with the bound loss, we add a large penalty on unsafe states to incentivize maintaining safety throughout the entire trajectory. For branch and bound during verification, we set the precision limit as 0.025, which means as soon as the precision of the grid region reaches this precision, we stop branching. For the dynamics approximation, we use an NN with two layers of ReLU each of size 8.Vehicle Avoidance Our vehicle avoidance environment features a vehicle moving on an x-y plane, with 4-dimensional inputs (x, y, θ, v). Here, (x, y) represents the location of the vehicle on the plane, θ is the angle relative to the y-axis, and v is the speed. In this setting, we have five moving obstacles, each moving from one point to another at a constant speed for the duration of 500 steps. The five obstacles are: 1) moving from (x, y) = (-0.6, 1.0) to (x, y) = (-0.35, 2.0); 2) moving from (x, y) = (0.6, 0.0) to (x, y) = (0.75, 1.0); 3) moving from (x, y) = (0.0, 1.0) to (x, y) = (0.0, 2.0); 4) moving from (x, y) = (-0.85, 1.0) to (x, y) = (-1.6, 1.5); 5) moving from (x, y) = (0.75, 0.0) to (x, y) = (0.85, 0.0). Each obstacle is represented as a square with a diameter of 0.1. Additionally, safety constraints are set for the speed (v ≤ v max ) and angle (∥θ∥ ≤ θ max ), where v max = 5.0 and θ max = π/2. The task is to navigate the vehicle to a designated location while following safety constraints. The agent starts near the origin within an area defined by x, y ∈ [-0.5, 0.5], θ ∈ [-0.2, 0.2], and v ∈ [0, 0.1], and the goal is (x target , y target ) = (1.0, 2.0). The branching precision limit is 0.025 and for dynamics approximation, we use a NN with two layers of ReLU each of size 10.2D Quadrotor For the 2D quadrotor environment, we follow the settings in Dai et al. [2021] .ẋ = - sin(θ) m • (u 0 + u 1 ) ẏ = cos(θ) m • (u 0 + u 1 ) -g θ = length I • (u 0 -u 1 )We use a timestep dt = 0.02, the mass of the quadrotor is set to m = 0.486, the length to l = 0.25, the inertia to I = 0.00383, and gravity to g = 9.81. The input is 6-dimensional (y, z, θ, ẏ, ż, θ), where (y, z) represents the position of the quadrotor on the y-z plane, and θ represents the angle. The action space is 2-dimensional and continuous; the actions are clipped within a range to reflect motor constraints. Our safety criteria are 1. angle θ remains within a predefined range (∥θ∥ ≤ θ max ), 2. a minimum height constraint to prevent collision with the ground (y ≥ y min ), 3. avoid obstacles.Here we set θ max = π/3 and y min = -0.2. The task is for the quadrotor to navigate towards the goal while following safety constraints. We consider two scenarios for obstacles: fixed and moving. For fixed obstacles, there are five rectangular obstacles positioned in the y-z plane. We use (x l , x u , y l , y u ) to represent the two dimensional box, and the obstacles are: (x l , x u , y l , y u ) = (-0.3, -0.1, 0.4, 0.6), (x l , x u , y l , y u ) = (-1.2, -0.8, 0.2, 0.4), (x l , x u , y l , y u ) = (0.0, 0.1, 0.5, 1.0), (x l , x u , y l , y u ) = (0.6, 0.7, 0.0, 0.2), (x l , x u , y l , y u ) = (-0.8, -0.7, 0.7, 0.9). For moving obstacles, there are five obstacles that moves from one point to another at constant speed for the duration of 500 steps, each represented as a square of diameter 0.1. The obstacles are: 1) moving from (x, y) = (0.6, 0.0) to (x, y) = (0.6, 0.1); 2) moving from (x, y) = (-0.5, 0.2) to (x, y) = (-0.4, 0.3); 3) moving from (x, y) = (-0.3, 0.4) to (x, y) = (-0.4, 0.5); 4) moving from (x, y) = (-0.1, 0.3) to (x, y) = (0.0, 0.4); 5) moving from (x, y) = (-0.7, 0.5) to (x, y) = (-0.4, 0.6). The initial region for the quadrotor is defined with x ∈ [-0.5, 0.5] and the remaining state variables within [-0.1, 0.1]. The target goal is set to (x, y) = (0.6, 0.6). We set the branching limit to 0.0125 and for dynamics approximation we use a NN with two layers of ReLU each of size 6.3D Quadrotor Our 3D quadrotor environment features a 12-dimensional input space, represented as (x, y, z, ϕ, θ, ψ, ẋ, ẏ, ż, ω x , ω y , ω z ). The action space is 4-dimensional and continuous; the actions are clipped within a range to reflect motor constraints. Here, (x, y, z) denotes the location of the quadrotor in space, ϕ is the roll angle, θ is the pitch angle, and ψ is the yaw angle, ω x , ω y , ω z represent the angular velocity around the x, y, and z axes, respectively. The environment setting and neural network dynamics approximation follows the setup in Dai et al. [2021] , with the modification of using ReLU activations instead of LeakyReLU. The system dynamics is:plant_input =    1 1 1 1 0 L 0 -L -L 0 L 0 κ z -κ z κ z -κ z    • u R = rpy2rotmat(ϕ, θ, ψ) p = 0 0 -g + R • 0 0 plant_input[0]/m ω = -ω × (I • ω) + plant_input[1 :] I   φ θ ψ  =   1 sin(ϕ) • tan(θ) cos(ϕ) • tan(θ) 0 cos(ϕ) -sin(ϕ) 0 sin(ϕ) cos(θ) cos(ϕ) cos(θ)   • ωThe dynamics neural network has two ReLU layers, each with a size of 16 and dt = 0.02. We set the branching precision limit to 0.00625. The task is to navigating towards the goal while avoiding five obstacles represented as 3D rectangles. The locations of the obstacles are (-0.5, 0.5, -0.2, 0.2, -0.65, -0.55), (-0.7, -0.6, -0.1, 0.1, -0.5, -0.4), (0.5, 0.6, -0.2, 0.2, -0.4, -0.3), (-0.8, -0.6, 0.2, 0.4, -0.3, -0.2), (-0.8, -0.6, -0.4, -0.2, -0.2, -0.1), where the first obstacle is to avoid controller collide with the ground. We set the goal at (x, y, z) = (0.0, 0.0, 0.0), and the initial region is defined with x ∈ [-0.5, 0.5], y ∈ [-0.1, 0.1], and z ∈ [-0.5, -0.3], with the remaining variables confined to the range [-0.05, 0.05]. The reward is calculated based on the distance to the goal, where the agent receives a higher reward for being closer to the goal. The environment episodes end if either the magnitude of ϕ or θ exceeds π/3.Our code runs on an AMD Ryzen 9 5900X CPU with a 12-core processor and an NVIDIA GeForce RTX 3090 GPU. 


Decision: The paper introduces a novel technique for safe RL leveraging differentiable 
NN verification tools, currently, the algorithm is built using the $\alpha,\beta$-crown
verification method. 

The reviewers agreed that the approach is sound and novel and the authors addressed 
the main concerns of the reviewers during the rebuttal phase. In the final version of the paper, please include 
the discussion on the neural network-controlled systems, the additional benchmark, ablation and
clarifications provided in the response to the reviewers.

Reviews: review: paper_summary: paper_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.
strength_weakness: strength_weakness: 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: questions: 1. How to ensure that Algorithm 2 can terminate?
limitations: limitations: The authors have addressed the limitations in the final part.
paper_summary: paper_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.
strength_weakness: strength_weakness: 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: 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?
limitations: 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".
paper_summary: paper_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.
strength_weakness: strength_weakness: 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: 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?
limitations: 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.
paper_summary: paper_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.
strength_weakness: strength_weakness: - 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: 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?
limitations: limitations: Yes

Comments: comment: Thank you for these clarifications.
I greatly appreciate the feedback from the authors, which has sufficiently addressed my concerns and problems. I am willing to increase my score.
Thank you for your response. The authors have addressed my main concern with the paper. As such, I've increased the score to Weak Accept.
Thank you for your detailed response and promise to clarify the points in the revision. I have no further questions.