Learning Control Policies for Region Stabilization in Stochastic Systems
Authors: Matin Ansaripour
Mathias Lechner
Đorđe Žikelić
Krishnendu Chatterjee
Thomas A Henzinger
Venue: Submitted to ICLR 2023 (2023)
Keywords: Stability
learning for control
martingale
verification

Abstract: We consider the problem of learning control policies in stochastic systems which guarantee that the system stabilizes within some specified stabilization region with probability 1. Our approach is based on the novel notion of stabilizing ranking supermartingales (sRSMs) that we introduce in this work. Our sRSMs overcome the limitation of methods proposed in previous works whose applicability is restricted to systems in which the stabilizing region cannot be left once entered under any control policy. We present a learning procedure that learns a control policy together with an sRSM that formally certifies probability 1 stability, both learned as neural networks. Our experimental evaluation shows that our learning procedure can successfully learn provably stabilizing policies in practice.

Under review as a conference paper at ICLR 2023
LEARNING CONTROL POLICIES FOR REGION STABI- LIZATION IN STOCHASTIC SYSTEMS
Anonymous authors Paper under double-blind review
ABSTRACT
We consider the problem of learning control policies in stochastic systems which guarantee that the system stabilizes within some specified stabilization region with probability 1. Our approach based on the novel notion of stabilizing ranking su- permartingales (sRSMs) that we introduce in this work. Our sRSMs overcome the limitation of methods proposed in previous works whose applicability is restricted to systems in which the stabilizing region cannot be left once entered under any control policy. We present a learning procedure that learns a control policy to- gether with an sRSM that formally certifies probability-1 stability, both learned as neural networks. Our experimental evaluation shows that our learning procedure can successfully learn provably stabilizing policies in practice.
INTRODUCTION
Machine learning methods present a promising approach to solving non-linear control problems. However, the key challenge for their deployment in real-world scenarios is that they do not con- sider hard safety constraints. For instance, the main objective of reinforcement learning (RL) is to maximize expected reward (Sutton & Barto 2018). but doing this provides no guarantees of the system's 's safety. This is particularly concerning for safety-critical applications such as autonomous driving or healthcare, in which unsafe behavior of the system might have fatal consequences. Thus, a fundamental challenge for deploying learning- based methods in safety-critical applications such as robotics problems formally certifying safety of learned control policies (Amodei et al., 2016 García & Fernández) 2015).
Stability is a fundamental safety constraint control theory, which requires the system to converge to and eventually stay within some specified stabilizing region with probability 1, a.k.a. almost-sure (a.s.) asymptotic stability (Khalil 2002 Kushner 1965). Most existing research on learning policies for control system system with formal guarantees on stability considers deterministic systems and employs Lyapunov functions (Khalil) 2002) for certifying the system's 's stability. In particular, a Lyapunov function is learned jointly with the control policy (Berkenkamp et al. 2017: Richards et al. 2018 Chang et al.] 2019 Abate et al. 2021a). Informally, a Lyapunov function is a function that maps system states nonnegative real numbers whose value decreases after every one-step evolution of the system until the stabilizing region is reached. Recent work Lechner et al. (2022) has extended the notion of Lyapunov functions stochastic systems and proposed ranking supermartingales (RSMs) for certifying a.s. asymptotic stability in stochastic systems. RSMs generalize Lyapunov functions to supermartingale processes in probability theory (Williams) 1991) and decrease in value in expectation upon every one-step evolution of the system.
While these works present significant advances in learning control policies with formal stability guarantees, they are either only applicable to deterministic systems or assume that the stabilizing set is closed under system dynamics, i.e., the agent cannot leave it once entered. In particular, the work of Lechnerr et al. (2022) reduces stability in stochastic systems to a.s. reachability condition by assuming that the agent cannot leave the stabilization set. However, this assumption may not hold in real-world settings because the agent may be able to leave the stabilizing set with some positive probability due to the existence of stochastic disturbances. We illustrate this on an example in Fi
Contributions In this work, we introduce stabilizing ranking supermartingales (sRSMs) and prove that they certify a.s. asymptotic stability even when the stabilizing set is not assumed to be closed

---

Under review as a conference paper at ICLR 2023
under system dynamics. The key novelty of our sRSMs compared to RSMs is that they also impose an expected decrease condition within a part of the stabilizing region. The additional condition ensures that, once entered, the agent leaves the stabilizing region with probability most p < 1. Thus, the probability of the agent entering and leaving the stabilizing region N times is at most p., which by letting N - implies that the agent eventually stabilizes within the region with probability 1. The key conceptual novelty is that we combine the convergence results of RSMs Lechner al. (2022) with a concentration bound on the supremum value of supermartingale process. This combined reasoning allows us to formally guarantee a.s. asymptotic stability even for systems in which the stabilizing region is not closed under system dynamics.
We also present a method for learning a control policy jointly with an sRSM that certifies a.s. asymp- totic stability. The method parametrizes both the policy and the sRSM as neural networks and draws insight from established procedures for learning neural network Lyapunov functions Chang et al. (2019) and RSMs Lechner et al. (2022). loops between a learner module that jointly trains a pol- icy and an sRSM candidate and a verifier module that certifies a.s. asymptotic stability of the learned sRSM candidate by formally checking whether all sRSM conditions are satisfied. the sRSM can- didate violates some sRSM conditions, the verifier module produces counterexamples that are added to the learner module's 's training set to guide the learner in the next loop iteration.
We experimentally evaluate our learning procedure on 2 stochastic RL tasks in which the stabilizing region is not closed under system dynamics and show that our learning procedure successfully learns control policies with a.s. asymptotic stability guarantees for both tasks.
RELATED WORK
Stability for deterministic systems Most early works on control with stability constraints rely either on hand-designed certificates or their computation via sum-of ofuuqus (SOS) programming (Henrion & Garulli 2005) Parrilo| 2000). Automation via SOS programming is restricted problems with
polynomial dynamics and does not scale well with dimension. Learning-based methods present promising approach to overcome these limitations (Richards et al., 2018 Jin et al.] 2020 Chang & Gao. 2021). In particular, the methods of (Chang et al. 2019; Abate et al.) [202 la) also learn control policy and a Lyapunov function as neural networks by using a vearfer-errffeer framework that our method builds on and extends stochastic systems.
Stability for stochastic systems While the theory behind stochastic system stability is well stud- ied (Kushner [9655] 2014), there only few works that consider control with formal stability guarantees. The methods of (Crespo & Sun 2003) Vaidya| 2015) are numerical and certify weaker notions of stability. Recently, (Lechner et al. 2022 Zikelić et al. 2022) used RSMs and a learning procedure for learning stabilizing policy together with an RSM that certifies a.s. asymptotic sta- bility. However, as discussed in Section [T] this method is applicable only to systems in which the stabilizing region is assumed to be closed under system dynamics. In contrast, we propose the first method that does not require this assumption.
Learning stable dynamics Learning dynamics from observation data is the first step in model-based RL. Recent works considered learning deterministic Kolter & Manek (2019) and stochastic Umlaufi & Hirche (0017); Lawrence et al. (2020) system dynamics with specified stabilizing region.
Safe exploration RL Safe exploration RL restricts exploration of model-free RL algorithms in a way that ensures that given safety constraints are satisfied. This is typically ensured by learning the system dynamics' uncertainty and limiting exploratory actions within a high probability safe region via Gaussian Processes (Koller et al., 2018 Turchetta et al.) (019)) linearized models Dalal et al. (2018), deep robust regression (Liu et al. 2020), and Bayesian neural networks (Lechner et al. 2021.
Probabilistic program analysis Ranking supermartingales were originally proposed for proving
a.s. termination in probabilistic programs (PPs) [Chakarov & Sankaranarayanan 2013). Since then, they have been used for termination (Chatterjee et al. 2016 Abate et al. (02 and safety (Chat-) terjee et al., 2017: Takisaka et al. 2021) analysis in PPs. and the work of (Chakarov et al., 2016) considers recurrence and persistence with the latter being equivalent to stability. However, the per- sistence certificate of (Chakarov et al. (0166) is numerically challenging for learning and it differs substantially from our notion of sRSMs.
2

---

Under review as a conference paper at ICLR 2023
3 PRELIMINARIES
We consider a discrete- time stochastic dynamical system of the form
X fx,, π (xx), wi),
where f x u x X X' is dynamics function, π X - U is control policy and wi Min is a stochastic disturbance vector. Here, we use X C RR" to denote the state space, U C R. the action space and A S Rº the stochastic disturbance space of the system. In each time step, wi is sampled according to a probability distribution d over N. independently from the previous samples.
A sequence (x,, Ur (ee, of state-action dittiionn-dsuubbneee triples is trajectory of the system, if u I (xx). Wa E (upport(d) and X++1 = fx, ur:wr) hold for each t E Ny. For each state X, E X, the system induces Markov process and defines a probability space over the set of all trajectories that start in Xo Puterman 1994), with the probability measure and the expectation operators Px and Ex-.
Assumptions The state space X' C IR",, the action space 2 C Rmm and the stochastic disturbance space N C I2 are all assumed to be morel-measurable. Furthermore, we assume that the system has bounded maximal step size under any policy æ, i.c. that there exists A > 0 such that for every x E X. w E N and policy π we have ||x - f(x, π (x), w) S A. Note that this is a realistic assumption that is satisfied in many real-world scenarios, e.g. self-driving car can only traverse certain maximal distance within each time step whose bounds depend on the maximal speed that the develop. For our learning procedure in Section 5 we also assume that X' C R is compact and that f is Lipschitz continuous, which are common assumptions in control theory and RL.
Almost-sure asymptotic stability There several notions of stability in stochastic systems. In this work, we consider the notion of almost-sure asymptotic stability (Kushner] 1965). which requires the system to eventually converge and stay within the stabilizing set. In order to define this formally, for each x E X' let d(x, X,) = in,x, ||x x, I11. where || |/1 is the I fn-orrm on R".
set X, S X is said to be -urely (a.s.) asymp- totically stable, if for each initial state X E X we have Fx, [lim,-ro d(x;, X.)
Definition 1. A non-empty
1.
The above definition slightly differs from that of (Kushner 1965) which considers the special case of X, being a singleton set consisting only of the origin. i.c. X. = [0). The reason for this difference that, analogously to (Lechner et al. 2022) and to the existing works on learning stabilizing poli- cies in deterministic systems (Berkenkamp et al., 2017] Richards et al. 2018 Chang et al. 2019), we need to consider stability with respect to an open neighhorhood of the origin for our learning method to be stable. Note that we do not assume that the stabilizing set X, is closed under system dynamics so that the system cannot leave X, once it is reached, which contrasts the previous works on stability in deterministic (Berkenkamp et al. 2017: Richards et al. 2018 Chang et al. 2019) and stochastic (Lechner et al. 2022) systems.
4 THEORETICAL RESULTS
In this section, we introduce our novel notion of stabilizing ranking supermartingales (sRSMs). We then show that sRSMs can be used to formally certify a.s. asymptotic stability with respect to a fixed policy without requiring that the stabilizing set is closed under system dynamics. Note, in this section only, we assume that the policy π is fixed. In the next section, we will present our algorithm for learning policies that guarantee a.s. asymptotic stability together with an sRSM as a formal certificate of a.s. asymptotic stability.
Overview of ranking supermartingales In order to motivate our sRSMs and to explain their nov- elty, we first recall ranking supermartingales (RSMs) of (Lechner et al., 2022). RSMs were in- troduced for certifying a.s. asymptotic stability under a given policy x, when the stabilizing set is assumed to be closed under system dynamics. Note that, if the stabilizing set is assumed to be closed under system dynamics, then a.s. asymptotic stability of X, is equivalent to a.s. reachability since the agent cannot leave X, once entered. In what follows, we define RSMs and explain why they insufficient for certifying a.s. asymptotic stability when the stabilizing set is not closed under system dynamics.
3

---

Under review as a conference paper at ICLR 2023
a) f(x, =x++++
b)
C) V
w a~0((1111)
x(x)= =
X(+1 X1
X, (-0o,) 0l
Wy U
V(x) softplus(a 3)
M=1, =y=1, A-1.5 0.5
0
30
V M + -
Example of a 1-dimensional stochastic dynamical system for which the stabilizing set X, not closed under system dynamics since from every system state any other state is reachable with positive probability. a) System definition and an sRSM that it admits. b) Illustration of a single time step evolution of the system. e) Visualization of the sRSM and the corresponding level set used to bound the probability of leaving the stabilizing region.
Figure| 1:
Intuitively, an RSM is a non-negative continuous function V X - R that maps system states to non-negative real numbers and whose value at each state in X,, strictly decreases in expected value by some > 0 upon every one-step evolution of the system under the policy x.
Definition 2 (Ranking supermartingales (Lechner et al. 2022) ). A continuous function V
said to be a ranking supermartingale (RSM) for X₂ if V
(x)
Z O holds for each x X and if there
exists e >> 0 such that (V (xx) w))l < V(x)
e holds for each x E Xxx
It was shown that, if system under policy æ admits an RSM and the stabilizing set X, is assumed to be closed under system dynamics, then X, is a.s. asymptotically stable. The intuition behind this result is that V needs to strictly decrease in expected value until X, reached while remaining bounded from below by O. Results from martingale theory can then be used to prove that the agent must eventually converge and reach X₂ with probability 1, due to a decrease in expected value by <> 0 outside of X, being striet which prevents convergence any other state. However, apart from nonnegativity, the defining conditions on RSMs do not impose any conditions on the RSM once the agent reaches X,. In particular, if the stabilizing set X, not closed under system dynamics, then the defining conditions of RSMs do not prevent the agent from leaving and reentering X, infinitely many times and thus never stabilizing. In order formally ensure stability, the defining conditions of RSMs need to be strengthened and in the rest of this section we solve this problem.
Stabilizing ranking supermartingales We now define our sRSMs, which may be used to certify a.s. asymptotic stability even when the stabilizing set is not assumed to be closed under system dynamics and thus overcome the limitation of RSMs of (Lechner al., 2022) that was discussed above. Recall we use A to denote the maximal step size of the system.
Definition 3 (Stabilizing ranking supermartingales). Let e, M, 6 > 0. A Lipsehitz continuous func- tion V X + IR is said to be an M, 6) -tabbilizing ranking supermartingale M,8)-sRMM) for X, if the following three conditions hold:
1. Nonnegativity. V(x) > 0 holds for each X.
2. Strict expected decrease if V 2 M. For each x E X, Vx) 2 M then
B [V (x)x [V(x) -
3. Lower bound outside X.. V(x) 2 M + Lv A + 8 holds for each x E X' No, where Lv is a Lipschitz constant of
An example of an sRSM for a 1-dimensional stochastic dynamical system is shown in Fig. [ The intuition behind our new conditions as follows. Condition in Definition B requires that, at each state in which V 2 M, the value of V decreases in expectation by evolution of the system. As we show below, this ensures probability convergence to the set of states S = (x E X' Vxx) S M) from any other state of the system. On the other hand, condition in Definition 3 requires that V Z M + Ly A + å outside of the stabilizing set X', thus S C X, Moreover, if the agent is in state where V < M. the value of V in the next state has to be < M + Ly A due to Lipschitz continuity of V and A being the maximal step size of the system. Therefore, even if the agent leaves S, for the agent to actually leave X, the value of V has to increase from a value < M + Lv to a value 2 M + Ly + 8 while satisfying the strict expected decrease condition imposed by condition 2 in Definition 3 at every intermediate state
0 upon one-step
4

---

Under review as a conference paper at ICLR 2023
that is not contained in S. The following theorem is the main result of this section and it shows that sRSMs indeed certify a.s. asymptotic stability of Xg..
Theorem 1. Suppose that there exist e, M, 8 0 and an (e, M, (c, SRSM for Rg. Then N₂ is a.s. asymptotically stable.
The proof of the theorem and an overview of results from probability and martingale theory that we use in the proof are provided in Appendix and B In what follows, we outline the main ideas behind our proof. For each state Xo E X, we consider the probability space of all trajectories of the system that start in Xg- We first show that the (c, M, (M,5)-RRMM V for X, gives rise to an instance of the mathematical notion of supermartingales in this probability space. Next, we Supermartingale Convergence Theorem (Williams) 1991) to show that Conditions 1 and 2 in Definition 3 ensure that
the agent with probability converges to the set of states S = {x E X V(x) S M] S X, from any other state in the system. Finally, we use known concentration bound on the supremum value of a supermartingale process to show that the probability of the value of V increasing from M+
S M + Lv A to M Lv A + 8 is bounded from above by p M+ Hence, the agent with probability 1 converges to S C X, from any state, upon which by Conditions 2 and 3 in Definition 3 it leaves X, with probability at most < 1. The probability of this happening N times is most pd so by letting N + oo we conclude that the probability of the agent leaving X, infinitely many times is O. Therefore, the agent with probability 1 eventually stabilizes in X..
Bounds on stabilization time We conclude this section by showing that our sRSMs not only certify a.s. asymptotic stability of X',, but also provide bounds on the number of time steps that the agent may spend outside of X,- This is particularly relevant for safety-critica applications in which the goal is not only to ensure stabilization but also to ensure that the agent spends as little time outside the stabilization set as possible. For each trajectory p (X,; U, WeeNNo let Outx, (p) = l[t E No
X, & X,HI E No U {0o}.
Theorem 2. Let e, M,,6 > O and suppose that V X is an C,,M, -.SM for Xs. Let T supxEx, V(x) be the supremum of all possible values that V can allain over the stabilizing set
Ng. Then, for each initial state Xa E X, we have that
1. Exx [Ouxx] S V(xo) + (M++
6:6
2. IP Fx, (Outx,
2 S V(xu)
+ (M++v-))(++v--)) for any time t E N.
be
6-e-
Proof. See Appendix B
LEARNING STABLE POLICIES AND SRSMs ON COMPACT STATE SPACES
In this section, present method for learning stabilizing policy together with an sRSM that certifies a.s. asymptotic stability. As stated in Section 3 our method assumes that the state space X C RR compact and that f is Lipschitz continuous with Lipschitz constant L.y.
We parameterize the policy and the sRSM via two neural networks Ty X - U4 and V, : + IR. To enforee condition in Definition 3 which requires the sRSM be a nonnegative function, our method applies the softplus activation function x + log(exp(x) + 1) to the output of V,. The remaining layers of Te and V, apply ReLU activation functions, therefore To and V,, are also Lipschitz continuous (Szegedy et al. 2014). Our method draws insight from the algorithms Chang et al. (0119): Zikelić et al. (022) for learning policies together with Lyapunov functions or RSMs and it comprises of a learner and a verifier module that are composed into loop. In each loop iteration, the learner module first trains both To and V, on a training objective in the form of differentiable approximation of the sRSM conditions and 3 in Definition
Once the training has converged, the verifier module formally checks whether the learned sRSM candidate satisfies conditions and 3 in Definition 3 If both conditions are fulfilled, our method terminates and returns a policy together with an sRSM witnessing stability. If at least one sRSM condition is violated, the verifier module enlarges the training set of the learner module by system states that violate the condition in order to guide the learner towards fixing the policy and the sRSM in the next learner iteration. The pseudocode of the algorithm is shown in Algorithm | In what follows, we provide details on initialization, the learner and the verifier modules.
5

---

Under review as a conference paper at ICLR 2023
Algorithm 1 Procedure for learning stabilizing policy and an sRSM
Input Dynamics function f. distribution d, stabilizing region X, C X, Lipschitz constant L Parameters т > 0, Neond E N, N good E N, M -1, Errains òmain
Te policy trained by using PPO Schulman et al. (2017) MDP f, 1[x X.))
X f centers of grid cells of discretization of X with mesh
B< < centers of grid cells of subgrid of X while timeout not reached do
ne. V, + jointly trained by minimizing the loss function in eq. equation on dataset B Las Lv f- Lipschitz constants of TT.. V
+ Lv (L. (I^ + 1) +1)
XzM centers of grid cells whose at least one vertex x satisfies (x(x 2 M
Xee t counterexamples condition 2 in Definition on X
if X'e = { then
Cellsxi, < grid cells that intersect XX
Ao < the maximal step size of the system with the policy if (celll) > M + Lv - Ag for all cell E Cellsxr then return X, is a.s. asymptotically stable under policy Te end if
else
B (B fx B(V.()) < M)) Uxe end if end while
Return Unknown
Initialization We initialize the policy Ty by running several iterations of the proximal policy opti- mization (PPO) Schulman et al. (2117) RL algorithm. In particular, we induce a Markov decision process (MDP) from the given system by using the reward function + 1 E X,)) in order to learn an initial policy that drives the system toward the stabilizing set. The importance of initializa- tion was observed in (Chang et al. 2019). As for the training set B used by the learner, the state space X' by using a rectangular grid and define B to be the set of all centers of grid cells (discretization is defined formally below). Finally, note that we may always rescale sRSM by strictly positive constant factor. Therefore, without loss of generality, we assume the value M = in Definition for our sRSM.
discretize
Learner The policy and the sRSM candidate are learned by minimizing the loss
[(0,v) Leond 20, (0, + Leond s0, v).
(1)
The two loss terms guide the learner toward an sRSM candidate that satisfies conditions 2 and 3 in Definition 3 In particular, we set
(x (x()), Vz(x) + Cirain 0})-
Leand (6,
Σ
max
Σ
B
Necnd
XEB
W rod
Intuitively, for each x E B, the corresponding term in the sum incurs a loss whenever condition 2 violated at x. Since the expected value of Vv successor state of does not admit closed form expression due to V, being neural network, approximate it the mean of values of V, at Noond independently sampled successor states of x, with Neond being an algorithm parameter. For condition 3, the loss term samples Nound system states from X') X', with Noond algorithm parameter and incurs a loss whenever condition is not satisfied at some sampled state:
Locnds (0, v) = max((M + Lv. + Ag + Swain)
min
(x.),
In our implementation, we also add two regularization terms to the loss function used by the learner. The first term favors learning an sRSM candidate whose global minimum is within the stabilizing set. The second term penalizes large Lipschitz bounds of the networks To and V. by adding a regularization term. While these two loss terms do not directly enforce any particular condition in Definition 3 we observe that they help the learning and the verification process. Details on the regularization terms can be found in the Supplementary Material.

---

Under review as a conference paper at ICLR 2023
Verifier The verifier checks whether the learned sRSM candidate satisfies conditions 2 and 3 in Definition 3 (condition 1 is satisfied due to the softplus function applied to the outputs of V2), The key challenge is checking the expected decrease condition imposed by condition 2. To check this condition, following the idea of [Berkenkamp et al. (0017) and (Lechner et al. 2022) our method computes discretization X' of X' with mesh v > O so that for every x E X' there exists X E X such that | -x||1 < r. The discretization computed by considering centers of cells of rectangular grid of sufficiently small cell size. Then, due to the assumptions that the state space is compact and S. me and V, are all Lipschitz continuous, we show that it suffices to verify a slightly stricter condition at discretization points.
To verify condition 2 in Definition 3 the verifier first collects the set X of centers of all grid cells whose at least one state x satishes (x) 2 M. This set is computed via interval arithmetic abstract interpretation (IA-AI) (Cousot & Cousot 1977 Gowal et al. (018)) which for each grid cell propagates interval bounds across neural network layers in order to bound from below the minimal value that V, attains over that cell and adds the center of a cell to XzM whenever this lower bound is smaller than M. Once XzMM is computed, the verifier checks for each x XzM whether the following inequality holds
Euda Vo (1(R, (X)), < VZx() - T.
(2)
where Ly and Lv are the Lipschitz constants of me and Vú and K Lv
We
use the method of (Szegedy et al. 2014) to compute I.- and Ly. The reason behind checking this stronger constraint is that, due to Lipschitz continuity of all involved functions and due to r being the mesh of the discretization, we can show (formally done in Theorem 3 that this condition being sat-
isfied for each x XzA implies that the expected decrease condition Eu~aaVV (f oe xx(X), w)) <
(x(x) is satisfied for all x E X' with V(x) 2 M. Then, due to both sides of the inequality being continuous functions and {x X (x)x)
M} being compact set, their difference admits
strictly positive global minimum > 0 so that E (f To (x)) S Vx(x)
is satisfied
for all x E X' with V(x) 2 M. If eq. equation 2 is satisfied for each x E X²M. the verifier con- cludes that Vn satisfies condition 2 in Definition 3 Otherwise, any computed counterexample to this constraint is added to B to help the learner fine-tune sRSM candidate in the following learning iteration.
To formally check eq. equation 2 at some X X'M, need to compute upper bound on the expected value VV. (x))))) Note that this expected value does not admit a closed form expression due to V2, being a neural network function. Thus, we again employ IA-AI to com- pute an upper bound on the expected value of a neural network function over a probability distri- bution. First, we partition the disturbance space A C Rp into grid of finite amount of cells cell(NN = [Wi...., .Nk.: We denote maxvol = E.ell))) vol(NN.) the maximal volume of any cell in the partition. The expected value can then be bounded via
Ewwd Vi (f( No (x))
Σ
maxvol sup F(w) WEN,
.G.CCel(A))
where F(w) = (J To (x), w) and the supremum values are obtained by using the IA-Al-based method Gowal al. 2018). Note that maxvol is infinite in case A is unbounded. To compute the expected value of an unbounded N when assuming that d is product of univariate distributions, we Munssorm/Murphy Murphy (2012) each univariate probability distribution in d. As a result, the problem is reduced to the case of a probability distribution of bounded support.
apply the probability integral transform
To verify condition 3 in Definition 3] the verifier collects the set Cellsx of all grid cells that intersect X", X, Then, for each cell E Cellsxr,, it uses IA-AI to check
(3) with V, (cell) denoting the lower bound on V,, over cell computed by IA-AI. If this holds, then the verifier concludes that V, satisfies condition 3 in Definition with 5 = minlalleClllxx.,, {V (cell)-
(cell) M + Lv Ao.
M- Lv Ao). Otherwise, it proceeds the next learning iteration. The following theorem establishes the correctness of the verifier module.
Theorem 3. Suppose that the verifier shows that V,, satisfies eq. equation for each x 8 and
eq. equation 3 for each cell E C,, Then Vy is an sRSM and X, is a.s. asymptotically stable under no
7

---

Under review as a conference paper at ICLR 2023
2D system
Kernel
lteration
Iteration
0.00100
2
10.0110
0.00075
0.0005
0.00050
0.00025
0.5
-0.5
0.0
-0.5
0.0
0.0
-0.5
0.0
-0.5
0.5
0.5
Figure 2: Visualization of the sRSM candidate after 1 and 5 iterations of algorithm for the 2D system task. The candidate after 1 iteration does not fulfill all sRSM conditions, while the function after 5 learning iterations is valid sRSM. The plot the right shows the learned stabilizing subset (kernel) in green.
Inverted pendulum
Kernel
Iteration
Iteration 4
0.00150
0.0015
0,00125
10
0.00100
000005
0.00375
0.00060
0.00025
0
-2
-2
Figure 3: Visualization of the sRSM candidate after and 4 iterations of our algorithm for the inverted pendulum task. The candidate after iteration does not fulfill all sRSM conditions. while the function after 4 learning iterations is a valid sRSM. The plot on the right shows the learned stabilizing subset (kernel) green.
Proof. See Appendix D
EXPERIMENTAL RESULTS
In this section, we experimentally evaluate the effectiveness of our learning algorithm. We focus on the two benchmarks studied in Lechner et al. (2022). In particular, the authors could prove the stability of both systems when assuming that the stabilizing set closed under system dynamics. However, both environments violate this assumption. Here, aim to prove stability without suming a given set that is closed under the system dynamics. We parameterize both Te and V,, by two fully-connected networks with hidden ReLU layers with 128 units each. The first task two-dimensional linear dynamical system with non-linear control bounds and is of the form Tz-1 Ar, + Bg(u,) w, where is disturbance vector sampled from zero-mes mean triangular distribution. The function clips the action to stay within the interval [1. -1]. The state space is [x]] < 0.7, [z2| < 0.7) and we want learn policy for the stabilizing
X
{z
X.
X (fx 0.7 < -0.6, -077 < x2 < 0.43 U {o 0.6 < x S 0.7,0.4 S S 0.7)).
The second benchmark is modified version of the inverted pendulum problem adapted from the OpenAI gym Brockman et al. (2016). The system is expressed by two state variables that repre- sent the angle and the angu-
Environment
Iterations
Mesh (r)
Runtime
2D system
5
0.0007
0.80
3660
Inverted pendulum
4
0.003
0.97
2619 s
Table 1: Runtime statistics of our algorithm for both benchmarks.
8

---

Under review as a conference paper at ICLR 2023
lar velocity of the pendulum. Contrary to the original task, the problem considered here introduces triangular-shapee random noise to the state after each update step.
The state space is define as X' {a within the set
|
S 3, |22 - 3}, and objective the agent is to stabilize
X = 121 -3 σ1 1 2.9, -3 -3 22 I 03 2.9 S x - 5
Further details for both tasks well as additional plots provided in the Supplementary Material.
For both tasks, our algorithm could find valid sRSMs and prove stability. The runtime characteristics, such as the number of iterations and total run- time, is shown in T A In 2
2D system
Inverted pendulum
plot the sRSM found by gorithm for the 2D system task and
al-
Figure 3 we plot the sRSM found for the inverted pendulum task. We also visualize in Figure 2 and Fig- ure 3 in green the subset of X, im-
plied by the learned sRSM in which
-05
3.0
66
the system stabilizes for both of our example tasks. Finally, Figure 4 show the contour lines of the pected stabilization time bounds that obtained by applying Theorem to the learned sRSMs.
Figure 4: Contour lines of the expected stabilization time
implied by Theorem for the 2D system task on the inverted pendulum task on the right.
the left and
Limitations Verification of neural networks is inherently computationally difficult problem Katz ett al.] (2017): [Berkenkapp et al.] (2017); Sälzer & Lange (202T). Our method is subject to this barrier well. In particular, the complexity of the grid decomposition routine for checking the expected decrease condition is exponential in the dimension of the system state space. However, a key advantage of our approach is that the complexity only linear in the size of the neural network policy. Consequently, our approach allows learning and verifying networks that are of the size of typical networks used in reinforcement learning [Schulman decomposition procedure runs entirely on accelerator devices, including CPUs, GPUs, and TPUs, thus leveraging future advances these computing devices. A technical limitation our learning procedure that it is restricted to compact state spaces. However, this is a standard assumption in control theory and reinforcement learning. Our thcoretical results are applicable to arbitrary (potentially unbounded) state spaces, shown in Fig.
(2017). Moreover, our grid
7 CONCLUSION
In this work, we developed method for learning policies for stochastic control systems with formal guarantees about the systems" a.s. asymptotic stability over the infinite time horizon. Compared to the existing literature, which assumes that the stabilizing set is closed under system dynamics and cannot be left once entered, our approach does not impose this assumption. Our method is based on the novel notion of stabilizing ranking supermartingales (sRSMs) that serve as formal certificate of a.s. asymptotic stability. We experimentally showed that our learning procedure is able to learn stabilizing policies and stability proof certificates in practice.
REFERENCES
Alessandro Abate, Daniele Ahmed, Mirco Giacobbe, and Andrea Peruffo. Formal synthesis of æyapunov neural networks. IEEE Control. Syst. Lett 5(3):773-778, 2021a. doi: 10.1109SSSSS.. 2020.3005328. URL httthttts:// http:///oo..rgg////// 1109 TTT.0//..CSS... 2020 3005328

---

Under review as a conference paper at ICLR 2023
Alessandro Abate, Mirco Giacobbe, and Diptarko Roy. Learning probabilistic termination proofs. In Alexandra Silva and K. Rustan M. Leino (eds.), Computer Aided Verification -3rrd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II, volume 12760 of Lecture Notes in Computer Science, pp. 3-26. Springer, 2021 lb. doi: (0.10077978-3-030-8
_1. URL https:///dbl .rg 10. 007/ 978 0.30 688-9__8
Dario Amodei, Chris Olah, Jacob Steinhardt, Paul F. Christiano, John Schulman, and Dan Mané. Concrete problems in Al safety. CoRR, abs/1606.06565, 2016. URL http:///:///axx
abs/1606.1 06565
Felix Berkenkamp, Matteo Turchetta, Angela P. Schoellig, and Andreas Krause. Safe model- based reinforcement learning with stability guarantees. In Isabelle Guyon, Ulike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Gar- nett (eds.), Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, pp. 908-918, 2017. URL /RR/ittts///pprcceeinggg mereo wtt.ccp/ppaee cc/paper/2217/haai www 7766boc65922ee0557777 oat.aaaae........o.oaaaaaaaaaaa. .tw.aatttttmllm.
Greg Brockman, Vicki Cheung. Ludwig Pettersson, Jonas Schneider, John Schulman, Jie Tang, and Wojciech Zaremba. Openai gym. arXiv preprini wwx.v:1666.015440 2016.
Aleksandar Chakarov and Sriram Sankaranarayanan, Probabilistic program analysis with martin- gales. In Natasha Sharygina and Helmut Veith (eds.), Computer Aided Verification 25th Inter- national Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, vol- 8044 of Lecture Notes in Computer Science, pp. 511-526. Springer, 2013. doi: 10.1007/ 978-3- 3-644-39779-88 34. URL DEEDS:///O...cog100000///111-1-
34
Aleksandar Chakarov, Yuen-Lam Voronin, and Sriram Sankaranarayanan. Deductive proofs of al- most sure persistence and recurrence properties. In Marsha Chechik and Jean-François Raskin (eds.), Tools and Algoritimss for the Construction and Analysis of Systems 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Prac- tice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, vol- ume 9636 of Lecture Notes in Computer Science, pp. 260 279. Springer, 2016. doi: 10.1007/ 0-3-6662-4964-999
URL
15
Ya-Chien Chang and Sicun Gao. Stabilizing neural control using self-learned almost Iyapunov critics. In IEEE International Conference on Robotics and Automation, ICRA 2021, Xi'an, China, May 30 June 5, 2021, pp. 1803-1809 IEEE, 2021. doi: URL https://ddddt .rgg / 1ww.111194/444888 45066 2021. 9560886
Ya-Chien Chang, Nima Roohi, and Sicun Gao. Neural Зуаршпоv control. In Hanna M. Wal- lach, Hugo Larochelle, Alina Beygelzimer, Florence d' d'Alché-Bus Emily Fox, and Roman Garnett (eds.), Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NewrlPS 2019, December 8-14, 2019, Vancouver, BC, Canada, pp. 2240-3249, 2019. TRRUtttss:///poceeeeeee neurip................. cc/paper/ Abstract.
2019 http:/hhhhh244.1ceec
Krishnendu Chatterjee, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. Algorithmic anal- ysis of qualitative and quantitative termination problems for affine probabilistic programs. In Rastislav Bodík and Rupak Majumdar (eds.), Proceedings of the 43rd Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 22, 2016 pp. 327-342. ACM, 2016. doi: 10. 10.1445283761422337399 URL 11w.:////....1111111121 hEtE:s//0oa..oo/000.117777733332
Krishnendu Chatterjee, Petr Novotný, and Dorde Žikelić. Stochastic invariants for probabilistic termination, In Giuseppe Castagna and Andrew D. Gordon (eds.), Proceedings of the 44th ACM SIGPLAN Symposium
Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pp. 145- 160. ACM, 2017. doi: 10. 10.1145/3009837.300000 30099883. URL https::: //doi. 10. 11 wtt.:///..1111110011 30098873
10

---

Under review as a conference paper at ICLR 2023
Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analy- sis of programs by construction or approximation of fixpoints. In Robert M. Graham, Michael A. Harrison, and Ravi Sethi (eds.), Conference Record of the Fourth ACM Symposium Princi- ples of Programming Languages, Los Angeles, California, USA, January 1977, pp. 252-. ACM, 1977. doi: (0.1145/512950.512999 URI.https: //t:://doo..oo .or./oorg///0 1115//01.111552221 512973
Luis G. Crespo and Jian-Qiao Sun. Stochastic optimal control via bellman's principle. Autom, 39(12):2109-2114, 2003. doi: 10.1016//0005-10000 (18850000001198800000003333 05.1016/500550 10985000000008000000000008888080 (03) 00238-3
Gal Dalal, Krishnamurthy Dvijotham, Matej Vecerík, Todd Hester, Cosmin Paduraru, and Yuval Tassa. Safe exploration in continuous action spaces. ArXiv, abs/1801 00075777 2018.
Luis María Ferrer Fioriti and Holger Hermanns. Probabilistic termination: Soundness, com- pleteness, and compositionality. In Sriram K. Rajamani and David Walker (eds.), Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Lan- guages, POPL 2015, Mumbai, India, January 15-17, 2015, pp. 489 501. ACM, 2015. doi: 00.1145/667622.26770011 /Tt.:tpp///bb...og//0.11111/.//.
Javier García and Fernando Feránndez. A comprehensive survey on safe reinforcement learning. J. Mach. Learn. Res., 16:1437-1480, 2015.
cfm?
1d=2886795
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Ue- sato, Relja Arandjelovic, Timothy A. Mann, and Pushmeet Kohli, On the effectiveness of interval bound propagation for training verifiably robust models. CoRR, Abs/1810.12715. 2018. URL
httt:://axx: http:://rxxv..org wttp////////l/////ee 12715
Didier Henrion and Andrea Garulli. Positive polynomials in control, volume 312. Springer Science & Business Media, 2005.
Wanxin Jin, Zhaoran Wang. Zhuoran Yang, and Shaoshuai Mou. Neural certificates for safe control wtt.orgg..b..ooooooe/e/// 08465
policies. CoRR, abs/2006.08465, 2020.
Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International conference on computer aided verification, pp. 97-117. Springer, 2017.
H.K. Khalil. Nonlinear Systems. Pearson Education. Prentice Hall, 2002.
T. Koller, Felix Berkenkamp, Matteo Turchetta, and A. Krause. Learning-base based model predictive control for safe exploration. 2018 IEEE Conference on Decision and Control (CDC), pp. 6059- 6066, 2018
J. Zico Kolter and Gaurav Manek. Learning stable deep dynamics models. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d' Alché-Bue, Emily B. Fox, and Roman Gamett (eds.), Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC,
Canada, pp. 11 11126-11134, 2019. URL /tttpss:/pproeeediiss...ee neurips. wwt.:/uwwi.....pppeeee.eee cc/paper/ 2019/hass CaeeshhA4bbceeaala /ttp:///eeaaaaaaa2333333322222-2
htm.
Harold J Kushner. On the stability of stochastic dynamical systems. Proceedings of the National
Academy of Sciences of the United States of America, 53(1):8, 1965.
Harold J. Kushner. A partial history of the early development of continuous time nonlinear stochas- tic systems theory. Autom,, 50(2):003-334, 2014. doi: 10.1016/ automa/auoo 10.011.. URL
httpp:: //dp: .org//rg/... / C. 1tt.11166...utomaa....a..
ca. 2013. 10. 10.013
Nathan P. Lawrence, Philip D. Loewen, Michael G. Forbes, Johan U. Backström, and R. Bhushan Gopaluni. Almost surely stable deep dynamics. In Hugo Larochelle, Marc Aurelio Ranzato, Raia Hadsell, Maria-Florina Balcan, and Hsuan-Tien Lin (eds.),

---

Under review as a conference paper at ICLR 2023
Advances in Neural Information Processing Systems 33: Annual Conference Neu-
ral Information Processing Systems 2020, NewrIPS 2020. December 6-12. 2020, vir-
tual, 2020. URL https::/prrceeddnggg nww.ipps........................ CC/ wwtppppe///e//////e httper/////0/hhh//// hash./ 9b.31 9c3 rast ct html
Mathias Lechner, Dorde Žikelić, Krishnendu Chatterjee, and Thomas Henzinger. Infinite time hori- zon safety of bayesian neural networks. In Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2021, 2021.
Mathias Lechner, Dorde Žikelić, Krishnendu Chatterjee, and Thomas A. Henzinger. Stability ver- ification stochastic control systems via neural network supermartingales. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 36, pp. 73366. Jun. 2022. doi: 10. org/ index. wttp:nddw.ppppppppeppepppp pwtp/AAA/aaaiiiiiaceaappppppaapp
1609/aaai v36.............. 20695. URL. httthttts:///oop
vi view 20695
Anqi Liu, Guanya Shi, Soon-Jo Chung, Anima Anandkumar, and Yisong Yue. Robust regression for safe exploration in control. In LADC, 2020.
Kevin P. Murphy, Machine learning a probabilistic perspective. Adaptive computation and ma- chine learning series. MIT Press, 2012. ISBN 0262018020.
Pablo A Parrilo. Structured semidefiiite programs and semialgebraic geometry methods in robust- ness and optimization. California Institute of Technology. 2000.
Martin L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wi- ley Series in Probability and Statistics. Wiley, 1994. ISBN 978-0-47161977-2. doi: 10.1002/ 9780470316887. URL htttts:////c..ttt/ org 10. 0001110002994000 00000//998473311320
Spencer M. Richards, Felix Berkenkamp, and Andreas Krause. The Iyapunov neural network: Adaptive stability certification for safe learning of dynamical systems. In 2nd Annual Confer- ence Robot Learning, CoRL 2018, Zürich,, Switzerland, 29-31 October 2018, Proceedings, volume 87 of Proceedings of Machine Learning Research, pp. 466 466-476. PMLR, 2018. URL httt:://proceecingg.. mlr. /tt.:/adii.........peeee//////// htt.3///ccharrsss.cmm html
Marco Sälzer and Martin Lange. Reachability is np-complete even for the simplest neural networks. In International Conference on Reachability Problems, pp. 149-164. Springer. 2021.
John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov. Proximal policy optimization algorithms. arXiv preprint arXiv: 2017.
Richard S Sutton and Andrew G Barto. Reinforcement learning: An introduction. MIT press, 2018.
Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian J. Good- fellow, and Rob Fergus. Intriguing properties of neural networks. In Yoshua Bengio and Yann LeCun (eds.), 2nd International Conference on Learning Representations, ICLR 2014, Bansf, AB, Canada, April 14-16, 2014, Conference Track Proceedings, 2014. URL http:
6199
Toru Takisaka, Yuichiro Oyabu, Natsuki Urabe, and Ichiro Hasuo. Ranking and repulsing super- martingales for reachability in randomized programs. ACM Trans. Program. Lang. Syst. 43(2): 5:1-5:46, 2021. doi: 10.1145/3450967. URL /
Matteo Turchetta, Felix Berkenkamp, and A. Krause. Safe exploration for interactive machine learn- ing. In NewrIPS, 2019.
Jonas Umlauft and Sandra Hirche. Learning stable stochastic nonlinear dynamical systems. In Doina Precup and Yee Whye Teh (eds.), Proceedings of the 34th International Conference on Machine Learning. ICML 2017. Sydney, NSW, Australia, 6-11 August 2017, volume 70 of Proceedings of Machine Learning Research, pp. 3502-35100 PMLR, 2017. URL http: http::/pocceedddeego mlr. wtw.pp/ss//////omm auft 7a html
12

---

Under review as a conference paper at ICLR 2023
Umesh Vaidya. Stochastic stability analysis of discrete-time system using дyaрunov measure. In American Control Conference, ACC 2015, Chicago, IL. USA, July 1-3, 2015, pp. 4646 4651. IEEE, 2015. doi: 10.1099/ACC:2055.7772000 URL https://coi.org////
2015.7172061
David Williams. Probability with Martingales. Cambridge mathematical textbooks. Cambridge University Press, 1991. ISBN 978-0-521-4060555
Dorde Zikelić, Mathias Lechner, Krishnendu Chatterjee, and Thomas A. Henzinger. Learn- ing stabilizing policies in stochastic control systems. CoRR, abs/2205.1 11991, 2022. doi:
10.485550arXiv.2200. 11911. URLhttts:: //doi. http///o..ogg..../////o 48550/ /0 2205. 11 11991
A OVERVIEW OF PROBABILITY AND MARTINGALE THEORY
Probability theory A probability space is an ordered triple F,, IP) consisting of a non-empty sample space ?2 o-algebra F over Ω (i.e. collection of subsets of ! that contains the empty set 0 and is closed under complementation and countable union), and a probability measure P over F which is a function PP F + [0, 1] that satisfies the three Kolmogorov axioms: (1) P(0] 0, (2) P P[ [ = 1 [[A] for each A E F, and (3) (3) P A.] = Σ i== TP Ag for any sequence (A, of pairwise disjoint sets in F. Given probability space (2,F, P), random variable is function
X 0 - R U [ that is F-measurable, i.c. for each a E I we have {w E Q X(w) S a) E F. E[X] denotes the expected value of X. A (discrete-time) stochastic process is sequence (X:) of random variables in F.,FP))
Conditional expectation Let P, be probability space and X be random variable in PP) Given a sub-sigma-algebra F C F, a conditional expectation of X given F is an F'measurable random variable Y such that, for each A E F,, we have
E[X MΛ] = E IA]-
Here LA 14:0- {0, 1) an indicator function of A, defined via La(w) lif A, and (w) if w & A. If X is real-valued and nonnegative. then a conditional expectation of X given F exists and is almost-surely unique, i.e. for any two F'-measurable random variables Y and Y' which are conditional expectations of X given F we have that P|Y = Y = (Williams 1991). Therefore, we may pick any such random variable as a canonical conditional expectation and denote it by E[X F.).
Stopping time A sequence of sigma-algebras {F with Fo S F is filraation in the probability space (92, F, P). A stopping time with respect to a filtration {F is a random variable T .2 - No {oo} such that, for every i E No, have {w Ω T(w) < i] E F, Intuitively. T may be viewed as the time step at which some stochastic process should be "stopped", and since (w Q T(w) S i} E F, the decision to stop the time step is made solely by using the information available in the first i time steps.
Supermartingales and ranking supermartingales We now define the mathematical notion of rank- ing supermartingales. Let (S2, F, F,P) be a probability space, let e 2 and let T be a stopping time with respect filtration (FF An e-ranking supermartingale (e-RSM) with respect to T is stochastic process (x such that
* X₃ is ---masurable,, for each i 2 0,
Xww 2 0, for each 2 and w Ω, and
E[X [w) I (w)
Ir>>(w), for each i 2 0 and E Ω.
The name comes since RSMs are special instance of classical supermartingate processes Williams [1991]. A supermartingale with respect to a filtration (F is a stochastic process & which satisfies conditions and above with e = 0 (thus we define supermartingales only with respect to the filtration and not the stopping time). We conclude this overview with two results on RSMs and supermartingales that will later be used in our proofs. The first is a result on ranking supermartin- gales that was originally presented in works termination amalysis of probabilistic programs Fioriti & Hermanns (2013); CCatterjee et al. (2016). The second result (see Kushner (2014), Theorem 7.1) concentration bound the supremum value of nonnegative supemartingale.
13

---

Under review as a conference paper at ICLR 2023
Proposition 1. Let F. be a probability space, let (Fi) be filtration and let T be stopping time with respect to (Fi) Suppose that (X,) is an e-RSM with respect to T, for some 0. Then
1. P c0
2. [T] S 3|Xal and
3. T 2 1] 5 E|Xo| eit
for each E N.
Proposition 2. Let (2,,,P) be a probability space and let (Fi) be filtrationn Let (X:) be a nonnegative supermartingale with respect to (Fi) Then, every À > 0, we have
[X
P
sup X; i20
B PROOFS OF THEOREM AND THEOREM 2
We now prove Theorem and Theorem from the main text of the paper. For each initial state Xy X. denote by x Pxo) probability space over the set of all system trajectories that start in the initial state Xg that is induced by the Markov decision process semanties of the system (Puterman) 1994.. The key idea behind both proofs is to show that, for every state E (X the sRSM V for the set X, gives rise to a mathematical RSM in the probability space ( P We then use Proposition T and Proposition 2 to prove the claims of both theorems.
Canonical filtration and stopping time In order to formally show that V can be instantiated as mathematical RSM in this probability space, we first define the canonical filtration in this probability space and the stopping time with respect to which the mathematical RSM is defined.
Let Xo E X' and consider the probability space Fxo Px,) For each E No. define Fi S to be the o-algebra containing the subsets Qx, that, intuitively, contain all trajectories in 12x whose first states satisfy some specified property. Formally, we define Fi as follows. For each j E Nu, let C₁ : S2xo > X' be map which to each trajectory p p= (x,, u,,w))seN E Ωxx assigns the j-th state X, along the trajectory. Then F, is the smallest o-algebra over Ixx, with respect to which Co. CI...., C; are all measurable, where X C R is equipped with the induced Borel- o-algebra (Williams) 1991, Section 1). Clearly Fo C F. .... We say that the sequence of o-algebras (F;);=) is the canonical filtration in the probability space (Dxo: Fxo- PP,)
fx X V(x) S We then define Tg: Dxo - No U (oo} to be the first hitting time of the set
M). J. i... T's = inf(t E No Xx E 5}. Since whether (ps(p) < i depends solely on the first i states along p. clearly have {o E Ixx Ts(p) i} F, for each and so T's is stopping time with respect to (F.)
We now prove the theorems. Theorem. Suppose that there exist e, M, 6 > 0 and an (,, for Xg. Then X, is a.s. asymptotically stable.
Proof. In order to prove that X, is a.s. asymptotically stable we need to show that, for each xo E X.
Px Tim d(x,, X.)
1.
We prove the theorem statement by proving the following two claims. First, we show that, from each initial state E X, the agent with probability 1 converges to and reaches S = fx E X V(x) S M) which a subset of X, by condition that once the agent is in S it may leave X, with probability at most p = M+Lv-A+5 < We then prove that the two claims imply the theorem statement.
Definition of sRSMs. Second, we show M+Lv-A
Claim 1. For each Xy E X, Pxo [t E No s.t. x, E =
To prove Claim 1, let Xg E X. If
S, then the claim trivially holds. Thus suppose without loss of generality that X, & S so V(x)) > M, and consider the probability space (Ix,, Fx.,, Px.)). the canonical filtration (Fr) and the stopping time Ts with respect it.
14

---

Under review as a conference paper at ICLR 2023
Define stochastic process (X,) in ( Fxa Pxo via
[V(x)), xx(p) (V(XTe(o))
otherwise
In other words, X; is equal to the value of V at the i-th state along the trajectory until the stopping time Ts exceeded, after which X; is equal the value of V at the time step I's at which the process was stopped.
for each 2 O and p (x1, Ue We)eN E Exx
We prove that (x.) is an e-RSM with respect to the stopping time Tg. To prove this claim, check each defining property of e-SSMs:
Each X; is Fi-measurable. The value of X; is determined by the first states along trajectory, so by the definition of the canonical filtration we have that X; is Femeaaurable for each i 0.
Each X:(p) Since each X, is defined in terms of V and since know that V(x) for each state E X' by condition in Definition of sRSMs, it follows that Xi(p) IV for each i and p E 12x
Each E[X++1 (P) I (x(p) ITx,>> (p). First, we remark that the conditional expectation exists since X;+1 is nonnegative for each 2 0. In order to prove the desired inequality, we distinguish between two cases. Let (xt: Uy weeNo
V(x,). On the other hand, we have E[Xi+1| Fil(p) (f xxx), To see this, observe that
First, consider the case Ts(p) > i. We have that X2(p)
Ew-alVV =(x), satisfies all the defining properties of conditional expectation since the expected value of V at a subsequent state of x,, and recall that conditional expectation is unique whenever it exists. Hence,
E[ FF((P)
(x;), S Vxx) - X:(p) -,,
where the inequality holds by condition 2 in Definition 3 of sRSMs and since x; S as (s(p) > i. This proves the desired inequality.
Second, consider the case Ts(p) F.((e)] V (xTx(()) so the desired inequality follows.
We have X:(p) V(xTs(m)) and E[X
Thus, we may use the first part of Proposition to conclude that Ixx, [T's < oo] = 1, equivalently Px, [3t 1tt
No s.t. E S] This concludes the proof of Claim 1.
Claim 2. For each Xo E S, Px 31 E No s.t. & X.) < with M+LV-A M+Lv
To prove Claim 2, recall that S {x E X
V(x) < M). Thus, as V is Lipschitz continuous with Lipschitz constant Ly and as the maxmial step size of the system, it follows that the value
of V upon the agent leaving the set S is < M + Lv A. Hence, for the agent leave X, from Ly A and then also to reach
Xg E S, first has to reach a state X, with M < V(x,) S state X2 & X, from X₁ without reentering S. By condition 3 in Definition 3 of sRSMs, must
15

---

Under review as a conference paper at ICLR 2023
have (xx2) 2 M Lv A 466. Therefore,
P X0
3 No s.t. x $ X.
=P xo
12 No s.t. & b2 and M < V(x,) 1 M + Ly A and ((x2) 2 M + Ly A
with x2 E S for all & S t/
=Pxo
16 E No s.t. M (xx)) S M Lv .
Fx, 32 E No s.t. t < 12 and M < <V(x,) ) 1 M + Lv A and V(x2) 2 M + Ly A A6
3h E No s.t. M < <((,), & M + Lv A]
with X & for all 4 < t v l2
<Pxx 3t1 E No M < (x..) ) S + Lv |
sup x1EX, McV M
Px, 1tg E No s.t. V(xx,) 2 M + Lv A 5 and X & S for all 0 S <t 12
sup X1 McV ME M
Pxi Itz E No s.t. V(X.,) 2 M + Lv 6 and x & S for all 0 S t t 02
The first equality follows by the above observations. The second equality follows by Bayes' rule. The third inequality follows by observing that the trajectory satisfies the Markov property and there- fore that the supremum value of V upon visiting state does not depend on previously visited states. Finally, the fourth inequality follows since the value of the first probability term is S
Thus, to prove that Fx. 3t E No s.t. X2 & X₂] p 1 with p M+ A48 and therefore
M+
conclude Claim 2, it suffices to prove that, for each x X with M v(x.) S M + Lv A, have
Px 122 E No s.t. V(xx,) 2 M + Lv A + and x, & S for all 0 < t s 12
M+ A
S
M Lv A 8
To prove Claim 1, consider the probability space Fx, Pxz) and the stopping time T's with respect and define stochastic process (X.) in the probability space via
the canonical filtration (Fi)
[((x), (((T)))) otherwise
if < Ts(p)
X.(p)
for each 2 and a trajectory & that starts in X1. The argument analogous to the proof of Claim shows that it is an e-RSM with respect to the stopping time Ts. But note that sup,20 X; is equal to the supremum value attained by V until the first hitting time of the set S. Hence the above inequality follows immediately from Proposition 2 by observing that Ex, [Xo] V(x1) < M + Ly A and plugging in À= = M + Lv A + 8. This concludes the proof of Claim 2.
Proof that Claim I and Claim imply Theorem 1. By Claim 1, the agent with probability 1 converges to S C X, from any initial state. On the other hand, by Claim 2, upon reaching a state in S the probability of leaving X, is at most p < 1. Finally, by Claim again the agent is guaranteed to converge back to S even upon leaving X.. Hence, due to the system dynamics under a given policy satisfying Markov property, the probability of the agent leaving and reentering more than N times is bounded from above by p." Hence, by letting N + oc, we conclude that the probability of the agent leaving X, and reentering infinitely many times O, so the agent with probability eventually enters and S and does not leave X, after that. This implies that X, is a.s. asymptotically stable.
Theorem. Let e, M, > 0 and suppose that V : X + R is an (e, M, 8RSMM for X.. Let T supxex. V(x) be the supremum of all possible values that V can attain over the stabilizing set X,. Then, for each initial state Xg E X, we have that
1. E [Outx,] 5 V(xo) (M+Lv-A) (T--
6.6
16

---

Under review as a conference paper at ICLR 2023
2. Fx,, (Outx, 2 2 V(xo) (M+bv.A)-() (T for any time t N.
6-c
Proof. We start by proving the first item in Theorem 2. Let p = (x, ue LEN, be system trajectory. Recall that 5 = (x X V(x) M) C X, and that (s(p) inf No E X,) the first hitting time of S. Let us also denote by OutAfter,, (p) = (1 > Ts(p) x & X the number of time-steps that the trajectory p in states outside of the stabilizing X' after the first hitting time of S. Then, since S " X', for each system trajectory p = (x,, Up WoleN,, we have that
Outx, (p) & (p) + OutAfter.x,(p)
Therefore, for each initial state E X, we have
Ex [Outx, v Fx [Ts]
+ Exo [OutAfterx.]
E xx [Ts]
sup Ex OutAfterxx]
(4)
xEx
Now, by defining an e-RSM (X with respect to the stopping time Ts analogously as in the proof of Theorem 1 and by applying the second item in Proposition to it, can immediately deduce that
Exo
Xo)
V(xo)
Exp Ts
(5)
On the other hand, by Claim in the proof of Theorem know that the probability leaving X, M+ L+ < 1. Furthermore, once the stabilizing set X, is left, we know that the value of V is at most suPxe,x, V(x) + Lv A +'+ Ly A due Lv being the Lipschitz constant of V and A being the maximum step size of the system. Thus, we have
once in S is at most
sup Ex [OuAAftrrr Sp. xEX
sup XE +v
Ex [T's + sup Ex (OutAftte))
XEX
T Lv A
Sp
+ sup E [Ottffter.. xEX
where in the second inequality we again use the second item in Proposition but now applied to the c-SMM (X:) with respect to the stopping time Ts defined in the probability space of all system trajectories that start in the initial state x. Hence, by deducting supxex' [Ex(AfAfte from both sides of the inequality and then dividing both sides of the resulting inequality by p >>
conclude that
sup Ex (OutAfterxx] P- (T Lv A) xEX
(1-p)-
Therefore, since p A+5 deduce that
M My
sup Ex OutAfferrx) < (M Ly A) + Lv-
(6)
8.6
xEX
4 equation 5 and equation 6 we deduce the first item in Theorem 2. The second item in Theorem follows immediately from the first item in Theorem and an appli- cation of Markov's inequality which implies that P. Fxx Outx, 1]
By comgining eq. equation
Exn [Ouxx, for any >>
C REGULARIZATION TERMS
Here, provide details the two regularization objectives that we add to the training loss.
Global minimum regularization We add the term (=,(0,)) v)) to the loss function, which is an auxiliary loss guiding the leamner towards learning sRSM candidate V,, that attains the global minimum in the set {x E X (xx) < M). .. In particular, we impose a set C X, to have value M and the global minimum of the sRSM being in T. While this loss term does not enforce any
17

---

Under review as a conference paper at ICLR 2023
of the conditions in Definition 3 directly, observe that it helps our learning process. It is defined via
L (0, v/) = max{
max Ny DDM D
())
min Fiy,N N, Ex Fionn DDEM
(a(a)
min Vz(z),
where DCM is a set of states at which the sRSM canidate learned in the previous learning iteration M and N3 and N₂ are algorithm parameters.
Lipschitz regularization We regularize Lipschitz bounds of V, and Ta during trainin by adding the regularization term
X Ap (0) Liipcchie (V)) Liipsschitz (V);
the training objective, with
Lipschitz (0) = max
II max Σ 1Wiol-p.00 p.
Wibep
and
Lipschite (x) min
II max
Σ
W.be
D PROOF OF THEOREM 3
Theorem. Suppose that the verifier shows that V, satisfies eg. (2) for each X E NZM and (3) for each cell Cel Then V, is an sRSM and X, a.s. asymptotically stable under ng.
Proof. To prove the theorem, we first need to show that V, satisfies the three conditions in Defini- tion 3.
Condition in Definition 3 is satisfied by default since V, applies the softplus activation function to its output which ensures nonnegativity.
To deduce condition 2 in Definition 3, we need to show that there exists > 0 such that for each X' with (x) M we have
Eund Vo (F(x, $ V(x)- -c
We show that
min (v(x) - K - (((( (x), RENzM
satisfies this requirement. Fix x E X' with Vx(x) 2 M and let & E E be such that ||x - | S T. Such exists by definition of discretization. Furthremore, since Vx(x) 2 M, the center of the cell that contains x must be contained in Xz so therefore we may pick such E X (the correctness of the computation of Y²M follows from the correctness of IA-AI (Cousot & Cousot 1977
Gowal
ct al. 2018)). Then, by Lipschitz continuity of f. To and Vy, we have that
Ewnd Vi (x( Te Tx)x) w))
Ewwed
V, [xx To (x) w)
+ +1ff(x, No (x),, f(x, It (x), Ly +11(x, TO (x))) (x, π. w)), Lv L, -1 x|11 Lv Ly (1 Ln)
< Ewwnd
V. [(x, me (x), w)
(8)
Ewend
Vn [f(x no (x), w)
Eawnd V. f(( No (x),
Lv Lg (1 Izz),
On the other hand, by Lipschitz continuity of V, have
Vx(x)= > Vo(x) x||1 Lv Vx(x) - Ty.
18

---

Under review as a conference paper at ICLR 2023
Thus combining eq. eq.(8) and (9) get that
Vx(x) Bowdd Vv (fxx, (x(x)
2 (x) Lv Eundd Vi ( (x)) Lv Ls (1 Lx)
(10)
(x)) - T. K Eunn Vo [(xx TO (x), 2G
The last inequality holds by our definition e, therefore we conclude that V, satisfies condition in Definition 3.
Finally, to deduce condition 3 in Definition 3, we need to show that there exists 8 > such that (x(x) M + LV A + ö holds for each x X' But the fact that
{ (cell) M Lv Ao} Celle
min
satisfies the claim follows immediately from correctness of IA-AI and the fact that eq. (3) holds for each cell E Ce
Thus, this concludes the proof that V2 satisfies the three conditions in Definition 3. Then, by Theo- rem I on sRSMs, we know that X, is a.s. asymptotically stable under TT.
E EXPERIMENTAL EVALUATION DETAILS
We implemented our algorithm in JAX. All experiments were on CPU-core machine with 64GB of memory and an NVIDIA A10 with 24GB of memory.
Benchmark environments The dynamics of the two-dimensional dynamical system (2D) system) are defined as
(
0 0.98 X. 00.002
0.0196)
0.1 g(u)) (0.002
0 0.001)<>.
X
0.001 w.
(1I)
where is disturbance vector and w(1), [2] Triangular. The function bounds the range of admissible actions by g(u) = max(min( 4, 1), -1).
The probability density function of Triangular is defined by
i
Triangular(r) = 1 |o|
-
(12)
0
otherwise
The dynamics function of the inverted pendulum task is defined
X [2] b)x,
+ d 1.5 G
[in +x)
3 mf² 29(u:)
2/
+ 0.002w[1]
X(+1 == x:[
x [2] + 0.005w[2].
where the parameters d, G, m, 1, are defined in Table 2 For training a policy on the inverted
pendulum task, we used a reward Tt at time defined by := x,[1] - 0011x|2]]
The hyperparameters we used in the experiments for learning the policy and the sRSM are listed in Table 3 For each of the tasks, consider T {x | < 0.2, [x2z < 0.2).
We observed better convergence and more stable training when training only the sRSM candidate and keep the weights of the policy frozen for the first three iterations of our algorithm. For the second task we replaced Emain with Kg T during the training. Specifically, instead of using Leand v),
set
19

---

Under review as a conference paper at ICLR 2023
Parameter
Value
d 0,05
G
10
m 0.15
0.5
b 0.1
Table 2: Parameters of the inverted pendulum task.
Parameter
Value
Learning rate
0,0005
X
0.001
O
10
Pa
4
Pv
8
p'
0.01
Otrain
0.1
Ncond
16
N Nond
256
N3
256
Na 512
Eyrain
0.1
Table Hyperparameters used in our experiments.
Vo To(x), Vz(x) Ko - T, 07) Noond
Goond 20,
max
Σ
B
XEB
For the inverted pendulum task, the plots and the results in Table in the main paper are obtained by training with L'cond (0,, v) the loss function. Here, performed ablation study test whether using 2 (6, v) can improve the results, i.e., whether the number iterations is decreased. The results in Table show that the effectiveness of using 20 v) on the particular system.
Grid refinement
We implemented two types of grid refinement procedures refine the mesh of the discretization used by the verifier. The first refinement is scheduled to multiply by 0.5 every second iteration starting iteration 5 if no hard violation is encountered by the verifier module. A violation is counterexample to condition 2 in Definition in the main paper. Hard violations are violations that also violate the condition
Euwd (F(x, < Vxx).
Environment
Use Iterations
Mesh (r)
p
Runtime
No
5
0.0007
0.80
3660 s
2D system
Yes
7
0.0007
0.78
4405
No
8
0.003
0.97
7004
Inverted pendulum
Yes
0.003
0.97
2619:
Table 4: Ablation analysis of the impact of the loss term C'sna (0, v). Number of leamer-verifier loop iterations, mesh the discretization used by the verifier, p. and total algorithm runtime (in seconds).
20

---

Under review as a conference paper at ICLR 2023
Our second refinement procedure is invoked when there violations but no hard violations. In this case, our procedure tries to verify grid cells where violations were observed using a mesh of 0.5r.
E.1
PPO DETAILS
The settings used for the PPO Schulman al. (017) pre-training process follows. In each PPO iteration, 30 episodes of the environment are collected in training buffer. Stochastic is in- troduced to the sampling of the policy network zy using Gaussian distributed random variable added to the policy's output, i.e., the policy predicts Gaussian's mean. The standard deviation of the Gaussian is dynamic during the policy training process according to a linear decay starting from 0.5 at first PPO iteration to 0.05 at PPO iteration 50. The advantage values are normalized by subtracting the mean and scaling by the inverse the standard deviation of the advantage values of the training buffer. The PPO clipping value is 0.2 and is set to 0.99. In each PPO iteration, train the policy for 10 epochs, except for the first iteration where we train the policy for 30 epochs. An epoch accounts to pass over the entire data in the training buffer, i.e., the data from the the rollout episodes. We train the value network 5 epochs, expect in the first PPO iteration, where we train the value network for 10 epochs. The Lipschitz regularization is applied the learning of the policy parameters during the PPO pre-training.
21


Reviews:
[{"review_id": "skh9AWeQJ1B", "reviewer": "Reviewer_kbSM", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "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": "", "main_review": "", "summary_of_the_paper": "In this paper, the authors developed a method for learning policies for stochastic control systems with formal guarantees about the systems’ a.s. asymptotic stability over the infinite time horizon. This work is most relevant to the previous recent work on ranking supermartingales \n(RSMs) by Lechner et al. (2022), and it mainly extended that result by relaxing the restriction that \"the stabilizing set is closed under system dynamics and cannot be left once entered\" with the help of a novel notion of stabilizing ranking supermartingales (sRSMs). Experimental results demonstrated the effectiveness of the proposed method.", "summary_of_the_review": "Generally speaking, I think this paper studies an interesting problem and the proposed method is novel  with its effectiveness appropriately demonstrated by the examples. In my opinion, the paper contains some novel valuables results that might be publishable on ICLR.\n\nBut I'd like to see more more elaborations and explanation on the motivation and the significance of relaxing the restriction that \"the stabilizing set is closed under system dynamics\" to better judge the contribution significance, and I also have some concern about the unfair/inaccurate claim that \"it always achieves rigorous theoretical a.s. asymptotic stability guarantee for the closed-loop system using the proposed method\", which I'd like to see some more clarifications/explanations from the authors.", "strength_and_weaknesses": "Strength:\n\n[1] The studied problem about stochastic control systems with formal asymptotic stability guarantees is interesting. The proposed method is novel and the empirical studies is helpful to demonstrate the effectiveness of the proposed method. \n\n[2] The paper is written reasonably clear and well organized.\n\nWeakness:\n\n[1] Since the main contribution of this paper compared the previous recent work by Lechner et al. (2022) is that, this work relaxed the restriction \"the stabilizing set is closed under system dynamics\", it would be helpful for the authors to elaborate more about why relaxing this limitation is important. Is such restriction a major limitation in real world applications? How common or uncommon to see such restriction in real world applications? Will relaxing of this restriction significantly enlarge the family of systems in real world applications (if yes, any application examples?) that the asymptotic stabilization results could be applied to, or such relaxing of the restriction is mainly important from theoretical perspective, and so far no any obvious impacts on any example real world applications? Some more discussions and explanations would on this direction would be helpful to better understand the motivations and significance of the results.\n\n[2] I'm not fully convinced about the claimed rigorous theoretical a.s. asymptotic stability guarantee for the closed-loop system using the proposed method with neural networks approximation, and I think this claim is inaccurate and somewhat misleading. In particular, such asymptotic stability guarantee is based on the assumption that the approximating NN can learn a sRSM that satisfies all the 3 conditions in Definition 3, however, there is no any rigorous mathematical guarantee that the trained NN (which is an empirical/heuristic process) could always find such an appropriate sRSM. The description in page 5, i.e., using a NN training objective in the form of a\ndifferentiable approximation of the sRSM conditions 2 and 3 in Definition 3, plus \"if at least one sRSM condition is violated, the\nverifier module enlarges the training set of the learner module by system states that violate the condition in order to guide the learner towards fixing the policy and the sRSM in the next learner iteration\", are just some heuristic tips to help find a good sRSM, but there is not rigorous mathematical guarantee that an appropriate sRSM can always be found following these tips. Therefore, it might be unfair to claim that it always achieves rigorous theoretical a.s. asymptotic stability guarantee for the closed-loop system using the proposed method. I'd like to see some more clarifications/explanations from the authors on this.\n\n\n\n\n", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "_Rr69xIjsYw", "reviewer": "Reviewer_M27f", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "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": "", "main_review": "", "summary_of_the_paper": "The authors consider the problem of asymptotic stability for discrete-time stochastic systems. They introduce a class of supermartingales, which they call stabilizing ranking martingales (sRSMs), which can be used to prove asymptotic stability and they show how these can be parametrised as neural networks and learned together with a controller. The method is evaluated on two 2-D systems.", "summary_of_the_review": "Well written paper with interesting theoretical results. However, I feel that the results are a bit too incremental compared to the literature. Also, experiments are not very convincing.", "strength_and_weaknesses": "Strength\n\nThe paper is well written and clear and addresses an important problem. The theoretical results are non-trivial and proofs are clear and sound.\n\nWeaknesses\n\nMy main two doubts about the paper are the following:\n\n- Results are quite incremental compared to Lechner et al. (2022). In particular, the techniques employed to learn and verify a neural network as a sRSM follow from those of Lechner et al. (2022)., which was also considering stability of stochastic systems. The main difference in that in this paper the authors managed to remove the constraint that the system dynamics must be closed with the stabilizing set. However, while interesting,  also considering the weaknesses identified below, I am not sure this is enough contribution for a full paper at ICLR.\n\n- Experiments are limited to 2-D systems. Would it be possible to consider also a 3-D system? If not, what is the main challenge? Also, looking at the contour lines in in Fugure 4 the expected stabilization time obtained by Theorem 2 looks quite conservative. Can you compare the value that you get with an empirical estimate obtained by running n trajectories of the systems?\n\n- While the above are my main concerns on the paper, another weakness is that there are some claims that are not accurate compared to the literature. For instance, the authors claim that \"there are only few works that consider control with formal stochastic stability guarantees\" and that \"existing works assume that the stabilizing set is closed under system dynamics\". While this may be true wrt learning based approaches, formal results for asymptotic stochastic stability also without the assumption that the stabilizing set is closed under system dynamics have been widely studied, see e.g. [Kushner, Harold J. Stochastic stability and control. Brown Univ Providence RI, 1967] or [Khasminskii, Rafail. Stochastic stability of differential equations. Vol. 66. Springer Science & Business Media, 2011] for a more recent reference. Also, in the intro the authors  seem to claim that only recently the notion of Lyapunov functions have been extended to stochastic systems for certifying a.s. asymptotic stability, but as shown in the books above this was done way before. I suggest the authors to adjust these claims making them more precise.\n\n", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "H2ii3H2X9CC", "reviewer": "Reviewer_597U", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "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": "", "main_review": "", "summary_of_the_paper": "This paper focuses on learning control policies in stochastic systems that guarantee that the system stabilizes within some specified stabilization region with probability 1. The authors create an approach based on  stabilizing ranking supermartingales (sRSMs).\n\n", "summary_of_the_review": "This is a technically sound paper that unfortunately provides limited basis for evaluation of the results in comparison to state of the art.", "strength_and_weaknesses": "Strengths:\nThe technical basis is clearly defined, and supported by proofs.\n\nWeaknesses:\n\n1. A major issue with this article is the lack of comparison of the approach to known methods.\n a) I want to see a clear comparison to control synthesis for stochastic systems, , e.g., stochastic hybrid systems using barrier certificates [Huang et al. 2017]--see reference below.\n\nb). Can you clearly show a comparison to traditional stochastic control using state space methods, e.g., stochastic MPC? You assume knowledge of the state space model, so this is a natural comparison to understand.\n\nc) There is a big overlap with [Lechner et al. 2022]. Please identify what is novel in this submission. In particular, the empirical study seems almost the same.\n\n\nRelated work\n\nThe claim \"there are only a few works that consider control with formal stability guarantees\" is not entirely correct. The authors fail to mention a significant body of work in this area, e.g, [Huang et al. 2017], as well as numerous other papers. See survey by [Lavei et al. 2022].\n\n\nEmpirical analysis\n\nWhy in the experiments do you focus only on a disturbance vector sampled from a zero-mean triangular distribution? This is not realistic for real-world systems.\nAre the contour lines of the expected stabilization time (Figure 4) a function of the triangular-shaped random noise?\n\nThis method has been studied empirically only for toy systems. Can you comment on scale-up issues? is this approach meant to operate in real-time, or to be trained offline?\n\nVerification\n\nYou note that verification of neural networks is inherently a computationally difficult problem, but what of the semantics? Is this even well understood? In comparison to other formal-methods approaches to the same task, e.g., stochastic control verification, there is no well-defined reason why this proposed approach is suitable in terms of semantics. So a key question: why use verification via neural network control synthesis? What not use standard control-theoretic methods?\n\n\n\n\n\nHuang, C., Chen, X., Lin, W., Yang, Z., & Li, X. (2017). Probabilistic safety verification of stochastic hybrid systems using barrier certificates. ACM Transactions on Embedded Computing Systems (TECS), 16(5s), 1-19.\n\nJagtap, P., Soudjani, S., & Zamani, M. (2020). Formal synthesis of stochastic systems via control barrier certificates. IEEE Transactions on Automatic Control, 66(7), 3097-3110.\n\nLavaei, A., Soudjani, S., Abate, A., & Zamani, M. (2022). Automated verification and synthesis of stochastic hybrid systems: A survey. Automatica, 146, 110617.", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "2: Several of the paper’s claims are incorrect or not well-supported.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "C8VEye44zQ", "reviewer": "Reviewer_Mqvo", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "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": "", "main_review": "", "summary_of_the_paper": "This paper proposes theoretical results for the problem of stabilization in nonlinear stochastic control systems. The main contribution is that the authors introduce the notion of stabilizing ranking super-martingales (sRSMs) for certain stabilization regions, that can be used for ensuring almost sure stability.", "summary_of_the_review": "Overall, the paper is well written, and the results are well organized. I will try to finalize my decision after the rebuttal period to one of the accept or reject options.", "strength_and_weaknesses": "A non-inclusive list of things to be addressed is as follows. \n\n-  I am wondering that the suggested policy satisfies the asymptotically stability defined in Definition 1. For each step, the suggested policy controls an output to be included in the stabilizing region with probability at least 1-p satisfying the asymptotically stability. But, the asymptotically stability condition seems to require that p converges to 0 or other additional conditions. For example, suppose that the stabilizing region is X_S = [0,0,5] and the output x has the Bernoulli distribution with p. Then, x can be in the stabilizing region with 1-p, however, it does not satisfy the asymptotically stability. Theorem 2 shows that the probability p decreases over time, but it does not match the statement about the suggested policy. ------- The authors clarified this example in their rebuttal.\n\n-------------------------------------\npost rebuttal: Overall, the work does not seem to have significant novelties or important useful results. The setting is clearly hypothetical, and the theory seems like providing some conditions that their usefulness is not clear. To be a full paper, I believe that further contributions are needed, and also they must be contextualized better. Further, comparisons with the existing literature, e.g. on learning to stabilize linear systems and how this work generalize from linear to nonlinear systems, are required. \n", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}]

Author rebuttal:

Decision: Reject