Verified Safe Reinforcement Learning  for Neural Network Dynamic Models
Authors: Junlin Wu
Huan Zhang
Yevgeniy Vorobeychik
Venue: NeurIPS 2024 poster (2024)
Keywords: neural network
formal verification
safe reinforcement learning
Primary area: safety_in_machine_learning

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. Our code is available at https://github.com/jlwu002/VSRL.

Verified Safe Reinforcement Learning for Neural Network Dynamic Models
Junlin Wu
Huan Zhang
Computer Science & Engineering Washington University in St. Louis junlin in. wu@wustl.edu
Electrical & Computer Engineering
University of Illinois Urbana- -hhaaa-hh
huan@huan-zhan -zhang- com
Yevgeniy Vorobeychik
Computer Science & Engineering
Washington University in St. Louis
yvorobeychikOmustt..
Abstract
Learning reliably safe autonomous control one of the core problems in trust- worthy autonomy. However, training controller that can be formally verified to be safe remains major challenge. We introduce novel approach for learning verified safe control policies in nonlinear neural dynamical systems while maxi- mizing 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 leverage incremental verification, reusing information from prior verification runs. Finally, learn multiple verified settial-statedeppendee is especially valuable for more complex domains where learning a single universal verified safe controller is extremely challenging. Our experiments on five safe trol problems demonstrate that our trained controllers can achieve verified safety over horizons that much baselines, while maintaining high reward, as well as a perfect safety record over entire episodes. Our code is available fethhtp::/// htt.bttg..t.tt/gg///g thub. com wwmmmj/0002//VSR
controllers, idea that
order of magnitude longer than state-of-the -hettt-rrt
Introduction
The ability synthesize safe control policies is one of the challenges in autonomous systems. This problem has been explored from numerous directions across multiple disciplines, including control theory and AI [Achiam al. 2017 Dawson et al. 2022]. While considerable progress has been made, particularly when dynamics are linear Waabersich 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 major open problem. Indeed, even the subproblem of safety verification in nonlinear systems is viewed in itself major challenge and is active of research, particularly for neural network controllers [Bastani et al., 2018 Ivanov et al. 2019 Weil and Liu 2022]. State-of-the-art 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 al. 2024 or under idealized assumptions which do not hold in practice [Berkenkamp et al. 2017].
Two common properties 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
38th Conference on Neural Information Processing Systems (NcurIPS 2024).

---

(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 Ksttep 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 [Nagaaandi 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 series of obstacles to reach a designated goal, requiring K = 50 steps to safely maneuver through the obstacles. We aim to train 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-ar 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 K-rrechabilityy 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 novel loss function that integrates overall reward, as well as both traditional (empirical) safety loss along with the K K-reachability bound. Our second innovation is to learn 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, we can "save" controllers that work 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-arr 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 K-step safety for K up to order of magnitude larger than the prior art and maintains 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. 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 So.
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-ant safe RL baselines.
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. a [017 [Sookk et al. 2020
Related Work:
Ma et al. 2022 Jayant and Bhatnagar 2022
Yu ct al. 2022 So and Fan 2023 Ganai et al. 2024

---

An alternative control-theoretes perspective aims to ensure stability or safety using Lyapunov and control barrier functions. For example, [Dwsso al. [2022] used learning- -ased approach to find robust control Lyapunov barrier functions; [Cho et al. [2018) constructed Lyapunov functions to solve CMDPs; WWnng et al., 2023a] proposed soft barrier functions for unknown and stochastic envi-
ronments; 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 al. [017 Jansen ctt al. 2020 Xiong et al. 2024] and required statistical assumptions, whereas our work aims for strict deterministic safety guarantees over finite horizon.
Among existing works focusing on safe RL with formal cetrrattes,,uullooe and Platzer 2018 apply a
theorem prover for differential dynamic logic to guarantee safety during runtime. Noren et al. [202]]
and Wei et al. [202]] consider forward safety invariance for systems with uncertainty. Kochdumper
et al. [2233] 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 [0222] 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 bree- policies for RL to reduce verification complexity; 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 al. [217 Huang et al. [017] or MIP-based (Tjeng et al.) [209)] 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. [021] Kouvaros and Lomuscio 2021
Ferrari et al. [202]] Zhang al.) [202]]. Our approach makes
of differentiable overapproximation
methods known collectively as a. a,B-CROWN [Wang et al., [22 Zhang et al. [022] (implemented with the auto LiRRPA package), and takes advantage of the particular structure of these verification
approaches in applying incremental verification to significantly speed up safe controller learning.
2 Preliminaries
Constrained Markov Decision Process (CMDP): We consider deterministic Constrained Markov Decision Process (CMDP) defined by the tuple (S, F, R, 7, Cr...,,..... d1, dmn), where: S is a set of states, A is a set of actions, F: 8 A S is the deterministic state transition function, R: : S x A + IR is the reward function, C; : S x A + IR is the cost function for the i-th constraint, d; is the cost limit for the i-th constraint, and 7 [0, 1) is the discount factor. A policy : S + AA 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 sy E Sg S S, which can be represented as sequence = (So, ag. $1, 01, $2, a2..... where st E S, = (ss) for all f, S1+1 = F(s,, oz), reward r, = R(s,, a.) and a cost C = Σie(m) Ci(se, 0t) are received after each action.
We denote Te as the policy that is parameterized by the parameter 0. A common goal for CMDP is to learn policy that maximizes a discounted sum of rewards I (TT) while ensuring that expected discounted costs Jc, (TT) do not exceed the cost limit d,, Vi E [m]. Formally, CMDP is to solve the below optimization problem:
max I (TTE) 0
s.t. Jc, (Te) S di, Vi [m].
where J(TO) = ETA EE 7 R(s,, a:) and Jc. (TO) = Eya E (CC,
Verified Safe CMDP: We define the state space as the union of predefined safe and unsafe states,
denoted as S Safee U Sunsafe- 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 ReL. neural
networks Giilesppi et al. 2018 Pfrommer et al. 2021 Dai et al. 2021 Liu et al. 2024 Our
3

---

objective is to train 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 [
(2a)
s.t. Jc. (TO) S di,
Vi E [m] (empirically satisfied) Vt E [K] (mathematically verified)
(2b)
8t Safer
(2c)
86-1 = F(st: ar), 0r = Te(s)), 8u E Su S Saate
(2d)
In particular, aim to solve (2) for high values of K and large sets of verified safe initial states So. while preserving a high objective value. Note that for a given controller, (2c) can also be interpreted as 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, restrict attention to d, = 0 for all i; however, our approach can be directly applied to arbitrary values of d;.
In this work, we primarily utilize the a,,-CROWN toolbox Xu et al. for neural network (NN) verification; however, our training framework is general and, in princi- ple, can work with any differentiable verification technique. Let FM denote the k-step forward function (iterative composition of F) under policy Ty. For example, $1 = (s) = F(s. (s)). (s) = F(1 To (1))), and so on. Correspondingly, we represent the s-step forward reachable re- gions returned by the NN verifier for an initial state set S as FBound (S), which is typically represented as box.
202 Wang et al. 202
3 Approach
The problem of learning verified safe control over a target horizon K entails three key technical chal- lenges. 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
state, it is difficult to find single universal controller that can achieve verified safety for each starting state in Sg. 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 eustomized for subsets of Su, 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 Vorobey. chik 2022]. At a high level, for a problem targeting K -stepp 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 Fk becoming deeper. For a deeper NN and a fixed branching budget, the output bounds become looser (Wang et al. [02T]. increasing the likelihood of intersections with unsafe regions. However, the ability to verify safety in prior steps enables us to tailor 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 K-step horizon. Our curriculum training framework is detailed in Algorithm [
The process begins by initializing the policy To with a pre-trained policy using safe RL algorithms (Line We then split the initial region So into grid Go (Line 4. We assume Sn is m-ddimensional box centered 8, E Rm with radius r E R.m i.e., S. = [sc -r., rr & + r). We prioritize splitting the dimensions that are directly implicated in safety constraints, thereby taking advantage of the

---

Algorithm Curriculum Learning with Memorization
1: Input: target safety horizon K, initial region So. unsafe region Sunsate, max attempt Tlmax
2: Output: controller Tæ
3: Initialize Ty with pre-trained policy, buffer B {}
4: Split initial region Sn into grid Go
5: for k 1.2....: K do
6: Thmain f-
7: Suc + Bound (9o) n Sunsae // optionally use Branch-and-Boume to refine Go
8: while Perain Renax and Suc + 0 do
9:
Safe RL training with loss function L(x) = (2) + BC (S (Swc U B)
Temin t -erain +
11: Suc - (9o) O Sunsafe
12: end while
13: Filter regions Sg C Go such that dist( Proma (Sk); Sunsafe) < store (Sk, 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 cost function CR for regions where (R(S) = if S S Sunsafe 0, and CR(S) > otherwise. positive CR means region intersects with Sunsafe, while CR = indicates S is safe. For example, if the task is to avoid the region (a, b). and the output bounds are given by JB = Iit; Zub]. we can define CR(EB) = max(Tab a, 0) max(b - Tíb. 0). We then calculate the gradient (CR(F Bound (Sr))/Or for chosen value and proceed to split along the dimensions with the largest gradient values, We continue this process, keeping the total number of grid splits within a predetermined p budget, and stop splitting once the budget is reached.
larger gradient indicates higher likelihood of reducing the cost Cn-
For each training phase k, we monitor the training rounds (Nuriin) as well as the k-step forward reachable regions returned by the verifier that are identified unsafe (Suc). Each phase is conducted for a maximum 7mmax rounds or until verified k-step safety achieved, that is, when Sue
(Line 8). At the end of each training phase, we also filter out regions Sg C Go where pd (Sx) are within distance to the unsafe regions. These regions
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 Maunchandd-ounde algorithm [Everett et al. 2020 Wang et al. 2021 to refine Go 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 l- k-phase loss for bounds (Line 9), where
(xx) = (xr) + XB (BoundaSuuc U B)
(3a)
Lnound ( Suc U UB) = Cn(FRimm (Suc)) +
Σ Cn(Fi. Bound (e(P)rnaasS)))
(3b)
(8,
Here, LSSEERL the standard safety RL loss, and LBound denotes the loss that incentivizes ensuring the output bounds returned by the verifier remain within the safe region. If both Sue is k-step safe and v(S., i) E B, S; is i-step safe, then LBouna U B) = O. otherwise, L (Suc U B) > In practice, we clip Lnauna U B) to ensure it remains within a reasonable range for training stability. The regularization parameter À is calculated based on the magnitude of LSatRL and LBound. with À min (Amax. a, L LBound), where Amax and a,, are hyperparamters. This approach helps maintain the effectiveness of bound training, especially when LBound is small. Furthermore, we cluster elements in B into categories that we do not need to construct computational graph for all i < k. Specifically, we merge all 5; for i S i < d2 into the iz category, meaning the elements in B are now (Us, i1, 12) instead of i).
is important to note that while our training scheme targets K -teep verified safety, the policy returned by Algorithm does not necessarily guarantee it. We address this issue by learning initial-state- dependent controllers as described below. Furthermore, the computation of Loound is computationally intensive. Its backpropagation requires constructing computational graphs for the k-th step forward
5

---

NN FBoggdd as well as for all i-th step forward NNs corresponding to each (S;, i) E B. These NNs become increasingly deep as grows, causing the computational graphs to consume memory beyond the typical GPU memory limits. We will address this next.
Above we discussed the challenge presented by the backpropagation of Lbound. 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 well- explored in the verification literature Wang et al. (0236], Althoff 2015]. to our knowledge, we are the first to apply it in training provably safe controllers.
Incremental Verification:
At a high level, to calculate the reachable region for a Aurget step, we decompose the verification into multiple phases. We begin by splitting the kaargt horizon into intervals defined by 0 < k1 < l-2 < < kip Kaarget- We first calculate the reachability region for the k; step and then use its output bounds as input to calculate the reachable region for the k4+1 step. This approach ensures that the computational graph is only built for the (kt+1 - ky) step horizon when using a.B-CROWN.
Unlike traditional incremental verification, which typically calculates the reachable region from k to k ++1, 1, we incrementally verify and backpropagate several steps ahead in single training iteration (i.e., from k; to 1; where ki+1 - k; > 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 lo prevents successful verification for k + (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 (kn, -1) steps' reachability, which is independent of karges This significantly reduces GPU memory usage. Since Fk is an iterative composition of F under the same policy Te, the bound for k steps tends to be tight. Moreover, when training Te to tighten these bounds, the overall bound for the entire ksarget horizon becomes increasingly tight.
Initial-State- Seatee-ttate- Controller: While curriculum learning above includes verification steps, it does not guarantee verified safety for the controller over the entire K K-step horizon. In this section, we propose using an statee--tttte-deeedeeett 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 So + O, which maps each initial state so E S a specific policy Th(so). The underlying idea is that training a verifiable safe policy To over the entire set of initial states Su 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 high level, the mapping and parameter set @ are obtained by first performing comprehensive verification for the controller output from Algorithm over the entire K K-step horizon. We then filter unverified regions, cluster them, and fine-tune the controller parameters 0 for each cluster. We store these fine-tuned parameters in the parameter set O This iterative refinement process continues until for every so E Sp. there exists a 0 θ such that To is verified safe for the entire K K-step horizon. The detailed algorithm is presented in Algorithm 2
The algorithm starts with verifying the policy Ty obtained from Algorithm The function VERIFY "ERIFYSAFF(TTe, So, K) (Line 4 performs verification of policy ne for initial states Sy for the entire horizon K. This verification process identifies and categorizes regions into verified safe areas, Sy and areas identified as unsafe, SY Notably, the union of these regions covers all initial states, meaning SV U S = Sy- After verifying that any state su E SY is guaranteed to be safe under policy TT. we record (SV ( Te) in the mapping dictionary H (Line
Next, we address the unsafe regions SY that lack a corresponding verified safe controller. We first cluster them based on the type of safety violation (Line The reason for clustering is that regions with similar safety violations are more likely 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-Srate-Deeenden Controller
1: Input: target safety horizon K, policy wo
2: Output: mapping dictionary H, which includes the mapping and parameter set θ
3: Initialize H
4: (S SV unsafe + VERIFYSAFETY So, K)
5: Store (S
safo 8) in mapping dictionary
6: while S
unsate * 0 do
7:
S , Sr} 6- CLUSTERREGION (S // cluster based on safety violation
8:
for = 1,2,.....
do
9:
TA. - TRAINPOLICY((TT Si, K) i Store (S (aate, 8') in mapping dictionary
10:
S Sinsate.)) & VERIFYSAFETY (Tgr, St, K)
12:
end for
13:
SY Lumsafe + U; Sy
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 simultaneouslly We then fine-tune the controller for the initial states in each cluster using Algorithm [ This fine-tuning process is typically fast, as the initial policy 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 80 E So.
At decision time, given initial state so, first identify the pair (8 TT) in the mapping dictionary H where E safe- then use the corresponding verified safe controller πT. Note that the soundness of the algorithm directly follows from our use of the sound verification tool a,8-CROWN.
4 Experiments
4.1 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 continuous action space for those discrete-time systems. In each experiment, we specify the initial region Sn 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 So that can be verified for safety over K steps; 2) Verified-Mar the maximum number of steps for which all states in Sy can be verified as safe; 3) Emp-k: the percentage of regions in So that initial state Sg. This is evaluated for both & = 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, in conventional reinforcement learning-
empirically safe for is steps. obtained by sampling 10" datapoints from the
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. [022]; 4) MBPPO, which applies model-basee safe RL with constrained PPO [Jayant and Bhatnagar] 2022 ; 5) CBF-RL, which is 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 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
7

---

Table Results for verified safety, empirical safety and average reward. The percentage results are truncated instead of rounded, to prevent missing unsafe violations.
Lane Following
Verified-80(1)
Verified-Man Mfx
Emp-80(t)
Emp-500(t)
Avg Reward (t)
PPO-Lag
98.6
99.9
99.9
326 + 6
PPO-PID
88.5
8
99.9
99.9
327 + 6
CAP 99.5
99.9
99.9
357 + 4
MBPPO
99.7
8
99.9
99.9
382 + 5
CBF-RL
98.7
7
99.9
99.9
331 +
RESPO
99.8
99.9
99.9
383 +
VSRL
100.0
80
100.0
100.0
214 +
Vehicle Avoidance (Moving Obstacles) Verified-Max(t)
Verified-50(1)
Emp-50(t)
Emp-500(t)
Avg Reward (t)
PPO-Lag
72.8
87.8
87.8
303 = 12
PPO-PID
72.0
6
89.4
89.4
287 + 22
CAP
73.3
89.5
89.5
393 +
MBPPО
82.6
6
94.2
94.2
375 + 10
CBF-RL
73.0
89.3
89.3
301 + 15
RESPO
74.5
9
89.6
89.6
391 + 20
VSRL
100.0
50
100.0
100.0
401 +
2D Quadrotor (Fixed Obstacles) Perified-Max(1" Emp-50(1)
Verified-50(1)
Emp-500(t)
Avg Reward
PPO-Lag
0.0
5
83.4
83.4
405 + 30
PPO-PID
0.0
99.3
97.5
411 + 25
CAP
0.0
3
99.5
99.5
393 + 12
MBPPO
58.9
99.9
84.5
399 +
CBE-RL
0.0
89.9
89.7
408 + 17
RESPO
60.4
99.9
99.9
339 + 19
VSRL
100.0
50
100.0
100.0
401 + 20
2D Quadrotor (Moving Obstacles) (erified-Max(t))
Verified-50(t)
Emp-50(t)
Emp-500(t)
Avg Reward (t)
PPO-Lag
0.0
3
99.7
99.7
371 + 7
PPO-PID
0.0
99.7
99.7
371 +
CAP
57.1
8
99.2
99.2
362 +
MBPPO
0.0
99.3
99.3
374 +
CBF-RL
0.0
4
99.3
99.3
369 + 6
RESPO
99.1
99.1
373 + 6
VSRL
100.0
50
100.0
100.0
364 +
3D Quadrotor (Fixed Obstacles) Verified-Max(t)
Verified-1 15t()
Emp-15(t)
Emp-500(t)
Avg Reward(1)
PPO-Lag
0.0
85.2
81.2
132 + 11
PPO-PID
0.0
89.4
88.3
145 + 12
CAP
0.0
63.6
59.2
141 + 11
MBPPO
41.1
75.4
73.1
132 9
CBF-RL
0.0
2
82.3
79.2
140 + 10
RESPO
0.0
65.7
21.3
79 8
VSRL
100.0
15
100.0
100.0
122 + 14

---

Lane Following: Our lane following environment follows the discrete-time bicycle model [Kong al. 2015]. The model imputs are 3-dimensional (z, 8, v), where x is the lateral distance to the center of the lane, 0 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 (ar, 0 v) = (0, O, Otarget) The safety constraints are 1) stays within a maximum distance from the lane center (||=]] S dmax), 2) remains within a predefined range (1 S 0mxx), and 3) v does not exceed the maximum threshold (v S Umax).
Vehicle Avoidance: Our vehicle avoidance environment features a vehicle moving on an z-y plane, with 4-dimensional inputs (z. y, 8, u). Here, (ar y) represents the location of the vehicle on the plane, 0 is the angle relative 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 (u S Umax) and angle [100 < mmax). The task to navigate the vehicle to 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, 0, ø, 2, 0). where (y, represents the position of the quadrotor on the y-= plane, and 0 represents the angle. The action space is 2-dimensional and continuous; the actions are clipped within a range reflect motor constraints. Our safety criteria include an angle constraint [[0]] S. mmax) and minimum height constraint to prevent collision with the ground (y 2 Bunn). We consider two scenarios for obstacles: fixed and moving. For fixed obstacles. there are five rectangular obstacles positioned in the y- 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- 12-dimensional input space, represented as (xc, M,, 2, o, 0, vh, - ú, 2, wa, Wy: Wy).)). The action space 4-dimensional and continuous; the actions are clipped within a range to reflect motor constraints. Here, (1r, y, z) denotes the location of the quadrotor in space, @ is the roll angle, 0 is the pitch angle, and &/ is the yaw angle, Was Wyy 4ig represent the angular velocity around the x, y. and z axes, respectively. The task is to navigating towards the goal while adhering safety constraints. which include avoiding five obstacles represented as 3D rectangles. The details for the environment settings are deferred to the Appendix.
4.2 Results
As shown in Table 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 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., |O| = 1). This 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.c., |6| = 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 haseline 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- dependdet controllers as part of VSRL. As shown in the Appendix (Section A.I) the

---

former significantly reduces average verification time during training, whereas the latter enables us to greatly boost the size of the initial state region Sg 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 mnitia-staaeedeeendee controllers. The third is to leverage small changes iterative gradient-basee 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 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
learning to enable incremental
based synthesis.
Acknowledgments
This research was partially supported by the NSF (grants NIS-5995558, 118-221414,, CCF-2403758, and IIS-2331960 22331963)) and NVIDIA. Huan Zhang is supported in part by the AI2050 program at Schmidt Sciences (AI 2050 Early Career Fellowship).
References
Joshua Achiam, David Held, Aviv Tamar, and Pieter Abbeel. Constrained policy optimization. In International conference on machine learning, pages 22-31. PMLR, 2017.
Mohammed Alshiekh, Roderick Bloem, Rüdiger Ehlers, Bettina Könighofer, Scott Niekum, and Ufuk Topcu. Safe reinforcement learning via shielding. In Proceedings of the AAAI conference on artificial intelligence, volume 32, 2018.
Matthias Althoff. An introduction to CORA 2015. In Proc. of the 1st and 2nd Workshop on Applied Verification for Continuous and Hybrid Systems, pages 120-151, EasyChair, December 2015. doi: 10.29007/zbkv.
Osbert Bastani, Yewen Pu, and Armando Solar-L Lezama. Verifiable reinforcement learning via policy extraction. Advances in neural information processing systems, 31, 2018.
Yoshua Bengio. Jérôme Louradour, Ronan Collobert, and Jason Weston. Curriculum learning. In Proceedings of the 26th annual international conference on machine learning, pages 41-48, 2009.
Felix Berkenkamp, Matteo Turchetta, Angela P. Schoellig, and Andreas Krause. Safe model- based reinforcement learning with stability guarantees. Proceedings of the 31st International Conference Neural Information Processing Systems, page 908-919, 2017.
Yinlam Chow, Ofir Nachum, Edgar Brenez-Guzman, and Mohammad Ghavamzadeh, A lyapunov- based approach to safe reinforcement learning. Advances in neural information processing systems, 31, 2018.
Hongkai Dai, Benoit Landry, Lujie Yang, Marco Pavone, and Russ Tedrake. Lyapunov-stable neural- network control. In Dylan A. Shell, Mare Toussaint, and M. Ani Hsich, editors, Robotics: Science and Systems XVII, Virtual Event, July 12-16, 2021, 2021.
Charles Dawson, Zengyi Qin, Sieun Gao, and Chuchu Fan. Safe nonlinear control using robust neural lyapunov-barrier functions. In Conference Robot Learning, pages 1724-1735. PMLR, 2022.
10

---

Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy A. Mann, and Pushmeet Kohli. A dual upproach scalable verification of deep networks. In Proceedings of the Thirty-Fourth Conference on Uncertainty in Artificial Intelligence, UAI 2018, Monterey, California, USA, August 6-10, 2018, pages 550-559, 2018.
Krishnamurthy Dj Dvijotham, Robert Stamforth, Sven Gowal, Chongli Qin, Soham De, and Pushmeet Kohli. Efficient neural network verification with exactness characterization. In Uncertainty in artificial intelligence, pages 497-507. PMLR, 2020.
Yousef Emam, Gennaro Notomista, Paul Glotfelter, Zsolt Kira, and Magnus Egerstedt. Safe rein- forcement learning using robust control barrier functions. IEEE Robotics and Automation Letters, 2022.
Michael Everett, Golnaz Habibi, and Jonathan P How. Robustness analysis of neural networks via efficient partitioning with applications in control systems. IEEE Control Systems Letters, 5(6): 2114-2119, 2020.
Claudio Ferrari, Mark Niklas Mueller, Nikola Jovanović, and Martin Vechev. Complete verification via multi-neuron relaxation guided Representations, 2022.
In International Conference on Learning
Nathan Fulton and André Platzer. Safe reinforcement learning via formal methods: Toward safe con- trol through proof and learning. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 32, 2018.
Milan Ganai, Zheng Gong, Chenning Yu, Sylvia Herbert, and Sicun Gao. Iterative reachability estimation for safe reinforcement learning. Advances in Neural Information Processing Systems, 36, 2024.
Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. Ai2: Safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE Symposium on Security and Privacy (SP), pages 3-18, 2018.
Morgan T Gillespie, Charles M Best, Eric C Townsend, David Wingate, and Mare D Killpack. Learning nonlinear dynamic models of soft robots for model predictive control with neural networks. In 2018 IEEE International Conference on Soft Robotics (RoboSoft), pages 39-45. IEEE, 2018.
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Timothy Mann, and Pushmeet Kohli. On the effectiveness of interval bound propagation for training verifiably robust models. arXiv preprint 1810.1811..121111 2018.
Shangding Gu, Long Yang, Yali Du, Guang Chen, Florian Walter, Jun Wang. Yaodong Yang. and Alois Knoll. A review of safe reinforcement learning: Methods, theory and applications. arXiv preprint arXiv:2205. 10330, 2022.
Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. Safety verification of deep neural networks. In Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28. 2017, Proceedings, Part I 30, pages 3-29. Springer, 2017.
Radoslav Ivanov, James Weimer, Rajeev Alur, George Pappas, and Insup Lee. Verisig: verifying safety properties of hybrid systems with neural network controllers. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pages 179-178, 2019.
Nils Jansen, Bettina Könighofer, Sebastian Junges, Alex Serban, and Roderick Bloem. Safe rein- forcement learning using probabilistic shields. In 31 International Conference on Concurrency Theory (CONCUR 2020). Schloss- Dagstuul--Liibbizz Zentrum für Informatik, 2020.
Ashish K Jayant and Shalabh Bhatnagar. Model-based safe deep reinforcement learning via constrained proximal policy optimization algorithm. Advances Neural Information Processing Systems, 2224432-24445 2022.

---

Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International Conference on Computer Aided Verification, pages 97-117, 2017.
Guy Katz, Derek Huang. Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar 7eljić, et al. The marabou framework for verification and analysis of deep neural networks. In Computer Aided Verification: 31 International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part 1 31, pages 443-452. Springer, 2019.
Niklas Kochdumper, Hanna Krasowski, Xiao Wang, Stanley Bak, and Matthias Althoff. Provably safe reinforcement learning via action projection using reachability analysis and polynomial zonotopes. IEEE Open Journal of Control Systems, 2:79-92, 2023.
Jason Kong, Mark Pfeiffer, Georg Schildbach, and Francesco Borrelli. Kinematic and dynamic vehicle models for autonomous driving control design. In 2015 IEEE intelligent vehicles symposium (IV), pages 1094-1099. IEEE, 2015.
Panagiotis Kouvaros and Alessio Lomuscio. Towards scalable complete verification of relu neural networks via dependency- -based branching. In IJCAI, pages 2643-2650, 2021.
Ziang Liu, Genggeng Zhou, Jeff He, Tobia Marcueci, Fei-Fei Li, Jiajun Wu, and Yunzhu Li. Model- based control with sparse neural dynamics. Advances in Neural Information Processing Systems, 36, 2024.
Diego Manzanas Lopez, Sung Woo Choi, Hoang- Tran, and Taylor T Johnson. Nnv 2.0: the neural network verification tool. In International Conference Computer Aided Verification, pages 397-412. Springer, 2023.
Yecheng Jason Ma, Andrew Shen, Osbert Bastani, and Jayaraman Dinesh. Conservative and adaptive penalty for model-based safe reinforcement learning. In Proceedings of the AAAI conference on artificial intelligence, volume 36, pages 5404-5412, 2022.
Anusha Nagabandi, Gregory Kahn, Ronald Fearing, and Sergey Levine. Neural network dynam- ies for model-based deep reinforcement learning with model-free fine-tuning. In 2018 IEEE international conference on robotics and automation (ICRA), pages 7559-7566. IEEE, 2018
Charles Noren, Weiye Zhao, and Changliu Liu, Safe adaptation with multiplicative uncertainties using robust safe set algorithm. PPAC-PupersOnLiie, 54(20):360-365, 2021.
Samuel Pfrommer, Mathew Halm, and Michael Posa. Contactnets: Learning discontinuous contact dynamics with smooth, implicit representations. Conference on Robot Learning, pages 2279- 2291. PMLR, 2021.
Chongli Qin, Krishnamurthy (Dj) Dvijotham, Brendan O'Donoghue, Rudy Bunel, Robert Stanforth, Sven Gowal, Jonathan Uesato, Grzegorz Swirszez, and Pushmeet Kohli. Verification of non-linear specifications for neural networks. In International Conference on Learning Representations, 2019.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages, 3(PO1L):41, 2019.
Oswin So and Chuchu Fan. Solving stabilize-avoid optimal control via epigraph form and deep reinforcement learning. In Proceedings of Robotics: Science and Systems, 2023.
Adam Stooke, Joshua Achiam, and Pieter Abbeel. Responsive safety in reinforcement learning by pid lagrangian methods. In International Conference on Machine Learning, pages 9133-9143. PMLR, 2020.
Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In International Conference on Learning Representations, 2019.
12

---

Kim P Wabersich and Melanie N Zeilinger. Linear model predictive safety certification for learning- based control. In 2018 IEEE Conference on Decision and Control (CDC), pages 7130-7135. IEEE, 2018.
Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. Advances in Neural Information Processing Systems, 34, 2021.
Yixuan Wang, Simon Sinong Zhan, Ruochen Jiao, Zhilu Wang, Wanxin Jin, Zhuoran Yang, Zhaoran Wang, Chao Huang, and Qi Zhu. Enforcing hard constraints with soft barriers: safe reinforcement learning in unknown stochastic environments. In Proceedings of the 40th International Conference on Machine Learning, (CML'23. JMLR, 2023a.
Yixuan Wang, Weichao Zhou, Jiameng Fan, Zhilu Wang, Jiajun Li, Xin Chen, Chao Huang, Wenchao Li, and Qi Zhu. Polar-express: Efficient and precise formal reachability analysis of neural-network controlled systems. IEEE Transuctions on Computer-Aided Design of Integrated Circuits and Systems, 2023b.
Tianhao Wei and Changliu Liu. Safe control with neural network dynamic models. In Learning for Dynamics and Control Conference, pages 739-750. PMLR, 2022.
Tianhao Wei, Shucheng Kang, Weiye Zhao, and Changliu Liu. Persistently feasible robust safe control by safety index synthesis and convex semi-infinite programming. IEEE Control Systems Letters, 7:1213-1218, 2022.
Junlin Wu and Yevgeniy Vorobeychik. Robust deep reinforcement learning through bootstrapped opportunistic curriculum. International Conference on Machine Learning, pages 24177-24211. PMLR, 2022.
Nuoya Xiong, Yihan Du, and Longbo Huang. Provably safe reinforcement learning with step-wise violation constraints. Advances in Neural Information Processing Systems, 36, 2024.
Kaidi Xu, Huan Zhang. Shiqi Wang, Yihan Wang. Suman Jana, Xue Lin, and Cho-Jui Hsich. Fast and Complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In International Conference on Learning Representations, 2021.
Dongjie Yu, Haitong Ma, Shengbo Li, and Jianyu Chen. Reachability constrained reinforcement learning. In International Conference on Machine Learning, pages 25636-25655. PMLR, 2022.
Huan Zhang, Tsui-Wei Weng, Pin-Ye Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In Advances in Neural Information Processing Systems, pages 4944 4953, 2018.
Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsich, and J. Zico Kolter. neural network verification. In Proceedings
General cutting planes for couudd-popagation of the 36th International Conference on Neural Information Processing Systems, 2022.
13

---

A
Appendix
A.1 Ablation Study
In this section, we conduct an ablation study to evaluate the importance of both incremental verifica- tion and the use of multiple nntial-state-ddeeedeett controllers as part of the VSRL approach.
Table Runtime (in seconds) for 20 training epochs with and without incremental verification.
Lane Following
5-step (4)
10-step (4)
15-step (4)
20-step (4)
w/ Incr. Veri.
9.4
9.4
17.4
24.8
w/o Iner. Veri.
9.6
38.1
105.9
185.5
Vehicle Avoidance
5-step (4)
10-step (4)
15-step (4)
20-step (4)
w/ Incr. Veri.
14.0
16.1
19.8
25.5
w/o Incr. Veri. 14.1
47.6
110.5
187.1
2D Quadrotor 10-step (4)
5-step (4)
15-step (4)
20-step (4)
w/ Incr. Veri.
8.4
13.7
15.9
19.6
w/o Iner. Veri.
8.8
35.8
86.8
152.1
3D Quadrotor 6-step (V)
5-step (4)
7-step (L)
8-step (U)
w/ Incr. Veri.
31.0
31.9
36.7
49.9
w/o Incr. Veri.
30.9
61.6
149.9
403.6
Table presents the ablation study results for incremental verification. 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 Sp that can be verified for safety for K steps (Verified-K).
Veh. Avoid. (t)
2D-Quad (F) (t)
2D-Quad (M) (f)
3D-Quad (F) (t)
Single Ctrl. 99.0
97.6
96.9
74.7
Multi Ctrl.
100.0
100.0
100.0
100.0
Table 3hows the ablation study results for using multiple mnital--ttteedeeeedeett 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, 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 larger initial state region Sp-
A.2 Experiment Setup
Lane Following Our lane following environment follows the discrete-time bicycle model [Kong
al.
2015
f
cos + 3)
14

---

sin + 5)
v sin(B)
I.
B tan -1 (
4 +4 tan(ōr)
where we set the wheel base of the vehicle to 2.9m. The model inputs are 3-dimensional (x, 0, v), where x: the lateral distance to the center of the lane, 0 is the angle relative 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 (a:, A v) = (0, O, Urarget). The safety constraints are
1. x stays within a maximum distance from the lane center ([|=]l S dmax),
2. 0 remains within predefined range (||0) S mmxx),
3. V does not exceed the maximum threshold (11 S Umma))
The parameters are set dmaax 0.7, 0max 7/4, and Umax = 5.0. The initial regions So is x E [-0.5, 0.5]. 0 E [-0.2, 0.2]. v E [0.0, 0.5]. The reward received at each step is measured as the distance the equilibrium point. More specifically, for state that is of distance d to the target equilibrium point, the reward is e-d For VSRL training, our controller initialized using a controller pretrained with 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 the precision limit 0.025, which means as soon 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 (zx, y, 0, v). Here, (I, 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 for the duration of 500 steps. The five obstacles are: 1) moving from (z. y) = (-0.6, 1.0) to (x. y) = (-0.35, 2.0); ; 2) moving from (0.75, 1.0); 3) moving from (z.z) (0.0, 1.0) to (z. y) (0.0, 2.0);
(z. y) (0.6, 0.0) to (z. 4) moving from (z. 8) = (-0.85, 1.0) to (z. y) = (-1.6, 1.5); 5) moving from (x,y) y) = (0.75, 0.0) to (z, y) (0.85, 0.0). Each obstacle is represented as square with diameter of 0.1. Additionally,
safety constraints are set for the speed (u I Umax) and angle [11@) I 0max). where Umax = 5.0 and 6mux 2/2. The task is to navigate the vehiele to designated location while following safety constraints. The agent starts near the origin within an area defined by I. y E [-0.5, 0.5].
0 E [-02, 0.2), and [0, 0.1J, and the goal is (Irarget Murget) (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
t sin(f)
(wo + u1)
ý cos(
(up + u1) -
length
(uo - u1)
We use timestep di 0.02, the mass of the quadrotor is set m 0.486, the length to = 0.25, the inertia to 0.00383, and gravity to g = 9.81. The input 6-dimensional (y. 2, 0 ú, é, 6). where (y, 2) represents the position of the quadrotor on the y-z plane, and 0 represents the angle. The action space is 2-dimensional and continuous; the actions are clipped within range to reflect motor constraints. Our safety criteria are
1. angle A remains within a predefined range (1101 S mmax)
2. a minimum height constraint to prevent collision with the ground (y 2 Umin),
3. avoid obstacles.
Here we set 0max = π 3 and Ymin = 0.2. The task is for the quadrotor to navigate towards the goal while following safcty constraints. We consider two scenarios for obstacles: fixed and moving, For
15

---

fixed obstacles, there are five rectangular obstacles positioned in the 2- plane. We use (2), Fu. 3t V/u) to represent the two dimensional box, and the obstacles are: (I), 9t yv (-0.3, 0.1, 0,,, 0.6). (1z, w.. Vu) = (-1.2, 0.88, 0.2, 0.4), (aT, Tu, y1, yu) = (0.0, 0.1, 0.5, 1.0), (x1, Tu. Ut. Un) (0.6, 0.7, 0.0, 0.2), (2i, Tu, Vt, Vu) = (-0.8, -077, 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 (z. y) = (0.6, 0.0) to (z. (0.6, 0.1); 2) moving from (I, y) (-0.5, 0.2) to (I, y)
(-0.4, 0.3); 3) moving from (x. = (-0.3, 0.4) to (x. - -0.4, 0.5): 4) moving from (x, 3) = (-0.1, 0.3) to (x,y) =
(0.0, 0.4); 5) moving from (z. = (-0.7, 0.5) to (z. (-0.4, The initial region for the quadrotor is defined with x E [00.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 NN with two layers of ReI.U each of size 6.
3D Quadrotor Our 3D quadrotor environment features 12- 12-dimensional input space, represented as (z. y, 2, o, 0, th, è. U, 2, Wz, Wy, Wz). The action space is 4-dimensional and continuous; the actions clipped within a range to reflect motor constraints. Here, (z. y, 2) denotes the location of the quadrotor in space, & is the roll angle, 0 is the pitch angle, and wi is the yaw angle, Way wy: wa represent the angular velocity around the x, y, and axes, respectively. The environment setting and neural network dynamics approximation follows the setup in Dai et al. [202T], with the modification of using ReLU activations instead of LeakyReLU. The system dynamics is:
1
1
0
L
LL
plant input
-L
0
L
0
K2
K2
Kz
-
Rij
R rpy2
(p, 0, +b)
p
+ R
9]
Dllnt_inppu((0)
w x (I w) + plant_input[] :]
I
sin(Ø) tan(O)
cos(Ø) (0) sin ())
0
(o) sin(e) (os(
w
cos( (os(O)
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.2, -0.65, -0.55,, -0.6, 00.1, -0.5, -0.4), (0.5, 0.65, -0.20 0.2, -0.4, -0.3), (-0.8, 0066, 0.2,0.4, -0.3, 0..3 -0.2), (-0.8, (0-.088-000 -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 (1r, y,, (0.0. 0.0, 0.0), and the initial region is defined with E [-0.5,
and E 1-0.5 0.33), 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 & exceeds 7 n/3.
y E [-001100.1
A.3 Compute Resources
Our code runs on an AMD Ryzen 9 5900X CPU with a 1 12-core processor and an NVIDIA GeForce RTX 3090 GPU.
16

---

NeurIPS Paper Checklist
1. Claims
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 perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how be expected to generalize other settings.
much the results
is fine to include aspirational goals as motivation as long is clear that these goals are not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Justification: we discuss the primary limitation 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 not discussed in the paper.
The authors are encouraged to create 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 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 few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution low images are taken in low lighting. Or speech-to-text system might 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 address problems of privacy and faimess.
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 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory Assumptions and Proofs
Question:
For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [NA]
17

---

Justification:
The paper does not include theoretical results.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced the statement of any theorems.
The proofs can either appear the main paper or the supplemental material, but they appear in the supplemental material, the authors are encouraged to provide short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental Result Reproducibility
Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Question:
Answer: [Yes]
Justification: We provide details of the experimental setup both in Section A.2 and in the Appendix.
Guidelines:
The answer NA means that the paper does include experiments. If the paper includes experiments, No answer this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is novel architecture, describing the architecture fully might suffice, or if the contribution is a specific model and empirical evaluation, it may be necessary to either make possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g.. in the case of large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily a new algorithm, the paper should make it clear how reproduce that algorithm. (b) If the contribution is primarily
model architecture, the paper should describe the architecture clearly and fully.
(c) If the contribution is a new model (e.g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome deseribe the particular way they provide for reproducibility, In the case of closed-source models, it may be that access to the model is limited in some way (e.g., registered users), but it should be possible for other researchers to have some path to reproducing or verifying the results.
5. Open access to data and code
Question: Does the paper provide open access to the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, as described in supplemental material?
18

---

Answer: [Yes]
Justification: We will provide all code and data on github, along with documentation, to facilitate reproduction of the experiments if the paper accepted for publication.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurlPS code and data submission guidelines (https://nips. cc/
for more details.
While we encourage the release of code and data, we understand that this might not be possible, so "No" is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to to reproduce the results. See the NeurIPS code and data submission guidelines (https
ssicnpolicy) for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information as possible in supplemental material (appended to the paper) recommended, but including URLs to data and code permitted.
6. Experimental Setting/Details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification:
We provide this information in Section 4 and the Appendix.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, or as supplemental material.
7. Experiment Statistical Significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer: [Yes]
Justification: We report confidence intervals in the results table in the experiments (see Section
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by emror bars, confi- dence intervals, or statistical significance tests, at least for the experiments that support the main claims of the paper.
The factors of variability that the error bars capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
19

---

It should be clear whether the error bar is the standard deviation or the standard error of the mean.
is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that out of range (e.g. negative error rates).
If error bars are reported in tables or plots, The authors should explain the text how they were calculated and reference the corresponding figures tables in the text.
8. Experiments Compute Resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed reproduce the experiments?
Question:
Answer: [Yes]
Justification: Justification: We provide this information in the Appendix.
Guidelines:
The answer NA means that the paper does include experiments.
The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well as estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary failed experiments that didn't make into the paper).
9. Code Of Ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics https://neurips..co
Answer: [Yes]
Justification: All aspects of the paper and research conform in all respects to the NeurlPS Code of Ethics.
Guidelines:
The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.
If the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g., there a special consid- eration due to laws or regulations in their jurisdiction).
10. Broader Impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [Yes]
Justification: As mentioned the introduction, ability to synthesize safe controllers is core challenge in autonomous systems (such as autonomous cars). As such, our work is expected have positive broader impacts.
Guidelines:
The answer NA means that there is no societal impact of the work performed.
If the authors answer NA or No. they should explain why their work has no societal impact or why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
20

---

The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is 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 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 attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility ML).
11. Safeguards
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, scraped datasets)?
Question:
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 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 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 dataset.
The authors should state which version of the asset is used and, if possible, include URL.
The name of the license (c.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 Datasets.papersstt paperswi thcode. cww/ datasets package should be provided. For popular datasets,
has curated licenses for some datasets. Their licensing guide can help determine the license of 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.
21

---

If this information is not available online, the authors are encouraged to reach out to the asset's 's creators.
13. New Assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [NA]
Justification: The paper does not release new assets.
Guidelines:
The answer NA means that the paper does not release new assets,
Researchers should communicate the details of the dataset/code/moodl as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset is used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing and Research with Human Subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification:
The paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsoureing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included in the main paper.
According the NeurIPS Code of Ethies, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional Review Board (IRB) Approvals or Equivalent for Research with Human Subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification: The paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing research with human subjects.
Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurlPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.
22


Reviews:
[{"review_id": "49qFuICNck", "reviewer": "Reviewer_kLbx", "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.", "questions": "1. How to ensure that Algorithm 2 can terminate?", "limitations": "The authors have addressed the limitations in the final part.", "rating": 7, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The paper is well-written and easy to follow.\n2. As far as I can tell, the idea of optimizing the verification horizon (curriculum learning) is novel and the experimental result is quite significant. \n3. 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.\n2. 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.  \n3. 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. \n\n[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\n[2] https://github.com/TUMcps/CORA?tab=readme-ov-file", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for the thoughtful comments and suggestions. Our responses are below.\n \n > **Question 1:** The authors may have to discuss their incremental verification vs. NNCS verification tools; POLAR-Express[1], CORA[2], etc.\n\n**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: \n1) 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).\n2) 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.\n\nWe 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.\n\n>**Question 2:** It is unclear how the proposed approach compares to other control-theoretical methods, for instance, the CBF-based approaches.\n\n**Response 2:**\nWe 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.\n \n\n|  |  |  Verified-K  |  Verified-Max  |  Emp-K |  Emp-500  |  Avg   Reward  |\n|---|---|---|---|---|---|---|\n| Lane Following, K = 80 | CBF-based | 98.7 | 7 | 99.9 | 99.9 | $\\mathbf{331 \\pm 7}$ |\n|  | VSRL (ours) | $\\mathbf{100.0}$  |      $\\mathbf{80}$        |       $\\mathbf{100.0}$      |   $\\mathbf{100.0}$        |         $214 \\pm 5$  |\n|  |  |  |  |  |  |  |\n| Vehicle Avoidance (M), K = 50 | CBF-based | 73.0 | 6 | 89.3 | 89.3 | $301 \\pm 15$ |\n|  | VSRL (ours) | $\\mathbf{100.0}$  |      $\\mathbf{50}$       |     $\\mathbf{100.0}$      |    $\\mathbf{100.0}$       |      $\\mathbf{401 \\pm 4}$    |\n|  |  |  |  |  |  |  |\n| 2D Quadrotor (F), K = 50 | CBF-based | 0.0 | 5 | 89.9 | 89.7 | $\\mathbf{408 \\pm 17}$ |\n|  | VSRL (ours) |  $\\mathbf{100.0}$  |  $\\mathbf{50}$  |  $\\mathbf{100.0}$  |  $\\mathbf{100.0}$ |  ${401 \\pm 20}$ |\n|  |  |  |  |  |  |  |\n| 2D Quadrotor (M), K = 50 | CBF-based | 0.0 | 4 | 99.3 | 99.3 | $\\mathbf{369 \\pm 6}$ |\n|  | VSRL (ours) | $\\mathbf{100.0}$  |      $\\mathbf{50}$        |     $\\mathbf{100.0}$      |    $\\mathbf{100.0}$        |    $364\\pm 4$   |\n|  |  |  |  |  |  |  |\n| 3D Quadrotor (F), K = 15 | CBF-based | 0.0 | 2 | 82.3 | 79.2 | $\\mathbf{140 \\pm 10}$ |\n|  | VSRL (ours) | $\\mathbf{100.0}$  |     $\\mathbf{15}$         |     $\\mathbf{100.0}$      |     $\\mathbf{100.0}$      |     $122 \\pm 14$  |\n|  |  |  |  |  |  |  |\n\n[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.\n\n> **Question 3: How to ensure that Algorithm 2 can terminate?**\n\n**Response 3:**\nEnsuring 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.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "5kvH38INwn", "reviewer": "Reviewer_11TB", "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.", "questions": "1. Could the authors explain the choice of these particular benchmark problems to evaluate the approach on?\n2. Is the state-space continuous or discrete for these benchmarks? (it appears it is continuous but only action-space is explicitly mentioned)\n3. Which of the chosen benchmark problems particularly showcases the benefit of a longer-than-five step lookahead reachability?\n4. How is the average reward computed (with verification over what horizon size)? Is it dependent on the verification horizon?\n5. 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": "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.\n\nOpen-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\".", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "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. \n\nIt 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. \n\nThe 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.\nThe 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. \n\nThe 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.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for the detailed comments and feedback. Our responses are below.\n\n> **Question 1:** A motivating example to guide the reader through the algorithm would be helpful.\n\n**Response 1:**\nWe appreciate the suggestion and will use vehicle avoidance as such an example in the revision.\n\n> **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.\n\n**Response 2:**\nBelow is the result where we only train for 5 steps lookahead.\n|                               |  Verified-K  |  Verified-Max  |  Emp-K |  Emp-500  |  Avg   Reward   |\n|-------------------------------|--------------|----------------|--------|-----------|-----------------|\n| Lane Following, K = 80        | 98.7         | 7              | 99.9   | 99.9      |  328 $\\pm$ 5    |\n| Vehicle Avoidance (M), K = 50 | 73.1         | 6              | 88.7   | 88.7      |  304 $\\pm$ 10   |\n| 2D Quadrotor (F), K = 50      | 0.0            | 5              | 87.5   | 87.5      |  401 $\\pm$ 23   |\n| 2D Quadrotor (M), K = 50      | 0.0            | 5              | 99.7   | 99.7      |  373 $\\pm$ 5    |\n| 3D Quadrotor (F), K = 15      | 0.0            | 5              | 90.5   | 89.3      |  129 $\\pm$ 10   |\n\nThis 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).\n\n> **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.\n\n**Response 3:** \nOur 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.\n\n> **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.\n\n**Response 4:**\nOur 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.\n\n> **Question 5:** Is the state-space continuous or discrete for these benchmarks?\n\n**Response 5:** \nBoth action and state space are continuous for all.\n\n>**Question 6:** How is the average reward computed? Is it dependent on the verification horizon?\n\n**Response 6:**\nAverage 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.\n\n> **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?\n\n**Response 7:**\nYes. 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.\n\n> **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\".\n\n**Response 8:**\nThis is a good point; we do intend to make all code and data available on github.\n\n[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.\n\n[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.\n\n[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.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "ReWxaCUi5O", "reviewer": "Reviewer_gxvV", "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.", "questions": "(1) Can the author explain the soundness of the approach proposed in the manuscript?\n\n(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": "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.", "rating": 6, "confidence": 4, "soundness": 2, "presentation": 3, "contribution": 2, "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. \n\nThe 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\n\n(1) Page 3.: “and required statistical assumptions“->”and requires statistical assumptions”\n\n(2) Page 4.: “which enable learning verified safe controllers over longer horizons K”->”which enables learning verified safe controllers over longer horizons K”\n\n(3) Page 4.: “In this work, we primarily utilize the α,β-CROWN toolbox”-> The α,β-CROWN toolbox should give a brief introduction here", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for the thoughtful comments and suggestions. Our responses are below.\n\n> **Question 1:** Can the author explain the soundness of the approach proposed in the manuscript?\n\n**Response 1:**\nSoundness 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.\n\n> **Question 2:** The rationality of the experimental comparison baseline, why is it more interesting to compare with these methods?\n\n**Response 2:**\nWe 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.\n\n> **Question 3:** What are the maximum dimensions of the system security verification problem that can be solved by this method?\n\n**Response 3:**\nThis 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.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "Sel6YoAKqw", "reviewer": "Reviewer_8TUT", "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.", "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": "Yes", "rating": 7, "confidence": 4, "soundness": 3, "presentation": 4, "contribution": 3, "strengths": "- Clear and very well written paper.\n\n- Clearly presented and motivated novel ideas to improve performance on a challenging problem.\n\n- Comprehensive empirical evaluation with a good number of meaningful benchmarks and baselines, and a further ablation study in the appendix.\n\n- 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.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We appreciate the reviewer's thoughtful comments and feedback. Our responses are below.\n\n> **Question 1:** What is the experimental setup in terms of timeout (if any) used to compare tools.\n\n**Response 1:**\nWe 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.\n\n> **Question 2:** What is the limiting factor in terms of the techniques' ability to synthesise safe policies?\n\n**Response 2:**\nThe 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.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: 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.
Decision: Accept (poster)