Neural Lyapunov Control of Unknown Nonlinear Systems with Stability Guarantees
Authors: Ruikun Zhou
Thanin Quartz
Hans De Sterck
Jun Liu
Venue: NeurIPS 2022 Accept (2022)
Keywords: neural networks
nonlinear dynamics
Lyapunov function
nonlinear control
stability guarantees

Abstract: Learning for control of dynamical systems with formal guarantees remains a challenging task. This paper proposes a learning framework to simultaneously stabilize an unknown nonlinear system with a neural controller and learn a neural Lyapunov function to certify a region of attraction (ROA) for the closed-loop system with provable guarantees. The algorithmic structure consists of two neural networks and a satisfiability modulo theories (SMT) solver. The first neural network is responsible for learning the unknown dynamics. The second neural network aims to identify a valid Lyapunov function and a provably stabilizing nonlinear controller. The SMT solver verifies the candidate Lyapunov function satisfies the Lyapunov conditions. We further provide theoretical guarantees of the proposed learning framework and show that the obtained Lyapunov function indeed verifies for the unknown nonlinear system under mild assumptions. We illustrate the effectiveness of the results with a few numerical experiments.

Neural Lyapunov Control of Unknown Nonlinear Systems with Stability Guarantees
Ruikun Zhou
Thanin Quartz
Department of Applied Mathematics
Department of Applied Mathematics
University Waterloo
University of Waterloo
ruikun. zhou@uaaterooo
tquartz@uwaterloo.
Hans De Sterek
Jun Liu
Department of Applied Mathematics
Department of Applied Mathematics
University of Waterloo
University of Waterloo j w.li@uvaterrloo.co
hans wet..deterrceuuaterroooooo
Abstract
Learning for control of dynamical systems with formal guarantees remains chal- lenging task. This paper proposes a learning framework simultaneously stabilize an unknown nonlinear system with a neural controller and learn a neural Lyapunov function certify region of attraction (ROA) for the closed-loop system. The algorithmic structure consists of two neural networks and satisfiability modulo theories (SMT) solver. The first neural network is responsible for learning the unknown dynamics. The second neural network aims to identify valid Lyapunov function and provably stabilizing nonlinear controller. The SMT solver then veri- fies that the candidate Lyapunov function indeed satisfies the Lyapunov conditions. We provide theoretical guarantees of the proposed learning framework in terms of the closed-loog stability for the unknown nonlinear system. We illustrate the effectiveness of the approach with set of numerical experiments.
Introduction
Finding the region of attraction (ROA) of an asymptotically stable equilibrium point for nonlinear dynamical system remains one of the most challenging tasks, especially for systems with uncertainty (26]. Even though the well-known Lyapunov theorems which use the level sets of Lyapunov function to estimate the ROA were proposed more than century ago, there is no general approach to finding a valid Lyapunov function for general nonlinear systems with provable guarantees [22]. Thanks to the development of learning-bar based methods, several data-driven approaches have recently shown their effectiveness in identifying unknown (or partly known) systems [8 30). However, how to simultaneously find Lyapunov functions and nonlinear controllers for systems with unknown
dynamics still an open and active problem control and roboties applications 20
By exploiting the expressiveness neural networks to tackle the complex nonlinearities of dynamical systems, we propose learning framework for simultancously learning control functions and neural Lyapunov functions. We build upon the framework in [5). but address the more challenging problem of stabilizing nonlinear system with unknown dynamics with formal stability guarantees. addition, we complement the computational framework in [3], by proving the existence of neural network satisfying the Lyapunov conditions, except on an arbitrarily small neighborhood of the origin, which offers theoretical basis for the learning framework here and in [5].
36th Conference on Neural Information Processing Systems (NcurIPS 2022).

---

Our proposed learning framework consists of two neural networks. The first neural network learns the unknown dynamics, while the second one aims to identify a valid Lyapunov function and a stabilizing nonlinear controller. After training the neural networks, we derive error bounds that can be verified directly by the satisfiability modulo theories (SMT) solver. We then use Lipschitz continuity of the nonlinear dynamics and its neural approximation to prove rigorous theoretical guarantees on the closed-loop stability of the unknown system under the learned nonlinear controller. To the best knowledge of the authors, no prior work has provided closed-loop stability analysis in such general setting of simultaneously learning the dynamics, a nonlinear controller, and a Lyapunov function.
We experimented on three typical nonlinear system examples: the Van der Pol oscillator, the inverted pendulum, and the unicycle path following. To align with the theoretical results, we carefully establish bounds for the Lipschitz constants, keep track of the training losses, and adjust the Lyаpunov conditions to be verified by the SMT solver accordingly so that the verified ROA is valid for the unknown system. The numerical experiments show that the ROA learned this way are comparable with the ones computed with actual dynamics, and improve that obtained from the LQR controller.
Related work. Artificial neural networks are capable of estimating any nonlinear function with arbitrarily desired accuracy [8]. As both the right-hand side of a differential equation and the Lyapunov function can be regarded as nonlinear (or linear) functions, mapping from the state spaces to some vector spaces, a natural question is: can we use neural networks to approximate the dynamies and find a Lyapunov function to attain a larger estimate of the ROA, compared with widely used linear quaddaati regulator (LQR) and sum of squares (SOS) methods (2 23
Various applications of neural networks for system identification and Lyapunov stability have been proposed recently [20 15]. For instance, Wang et al. [9] use recurrent neural network generate the state-space representation of an unknown dynamical system. A Lyapunov neural network is derived in 322] learn fixed quadratic format Lyapunov function for finding the largest estimated ROA. However, when it comes to finding a Lyapunov function with a typical feedforward neural network to certify the stability for the nonlinear systems, performing this kind of regression task is difficult for shallow neural networks, where only equality and/or inequality Lyapunov conditions, instead of explicit expression or values of the function, are given. Consequently, it is crucial to develop methods to test or verify the outputs of neural network. There are two main approaches to tackle this issue. One is converting the neural networks into a mixed-integer programming (MIP) format which can be solved by MIP solvers. The other is to encode the verification problem into an SMT problem. In the first category. 7 find robust Lyapunov function for an uncertain nonlinear system or a hybrid system which can be partly approximated by piecewise linear neural networks with method using mixed integer quadratic programming (MIQP),
the help of a counterexample-gun and the corresponding robust ROA is estimated. With a similar technique, [IO] synthesizes neural- network controller and Lyapunov function simultaneously to certify the dynamical system's stability by converting the dynamics, the Lyapunov function, and the controller into piecewise linear functions and solving it with mixed-integer lincar programming (MILP). On the other hand, several SMT solvers have been developed by various scholars (28 21). for instance, dReal [17). with which tasks with various nonlinear real functions can be elegantly handled. This can be employed in most cases for verifying existing neural network structures, e.g., with tanh and sigmoid activation functions. With the help of these SMT solvers, Chang et al. propose an algorithm to find and validate a neural Lyapunov function satisfying the Lyapunov conditions with heeehddee--laerr neural network (5). More recent work in [I] uses the same methodology to approximate control Lyapunov barrier functions for nonlinear systems to guarantee both stability and safety for reach-avoid robot tasks, while (36) uses a similar framework to design stabilizing controllers for unknown nonlinear systems with an implementation of Koopman operator theory. Gaussian process (GP) regression is used in [ 2 to learn the unknown systems while providing safety and stability guarantees for the states in the ROA with high probability, at the same time how to enlarge the estimated ROA is also well studied, On top of that, a method to obtain larger ROA by iteratively re-designing a control Lyapunov function is presented in (27]. Apart from the above traditional machine learning methodologies, [ proposes piecewise learning framework with piecewise affine models, where stability guarantees are verified with quadratic Lyapunov functions by solving an optimization problem. However, we have to contend with the safety-critical nature of certain control and robotics applications. As result, worse-case bounds and performance guarantees are more desirable. In a similar vein, an upper bound on the infinity- -orm bounds were established in the context of training deep residual networks (25). We remark that none of these works analyzed the closed-loop stability in the general setting as ours.
2

---

Contributions. We summarize the main contributions of the paper as follows.
We propose framework for simultaneously learning nonlinear system, stabilizing nonlinear controller, and a Lyapunov function for verifying the closed-loop stability of the unknown system.
We provide theoretical analysis on the existence of a neural Lyapunov function that verifies the I Lyapunov conditions, except arbitrarily small neighborhood of the origin, provided that the origin is asymptotically stable. This provides theoretical support for the proposed method as well other neural Lyapunov frameworks in the literature.
Combining classic Lyapunov analysis with rigorous error estimates for neural networks, establish closed-loop stability for the unknown system under the learned controller. This is accomplished with the help of SMT solvers and recent tools for estimating Lipschitz constants for neural networks.
2 Preliminaries
Throughout this work, we consider a nonlinear control system of the form
i = f(x, u), x0)
(I)
where x D is the state of the system, and D C IR an open set containing the origin; u E 2 R is the feedback control input given by = < <x))), where k(x)) is a continuous function of a. Without loss of generality, we assume the origin is an equilibrium point the closed-loop system
f (ar, <(x),,
s000) T0-
When there is no ambiguity, we also refer to the right-hand side of (2 by f.
We assume that do not have explicit knowledge of the right-hand side of the system T The main objective is to stabilize the unknown dynamical system by designing a feedback control function k. Stability guarantees are established using Lyapunov functions. We next present some preliminaries on model assumptions and Lyapunov stability analysis.
Model assumptions
Assumption 1 (Lipschitz Continuity). The right-hand side of the nonlinear system ! assumed to be Lipschitz continuous, i.e,
[s(x u) - v(y, S T.[(,, u) - (y. w)ll Vx, y E D and Yu, EM, where called the Lipschitz constant; ux) and (y. v) denote the concatenation of the corre- sponding two vectors. We assume the Lipschitz constant I. is known.
Assumption 2 (Partly Known Dynamics). The linearized model about the origin in the form of i = Ar + Bu, where A and B are constant matrices, is known for the nonlinear system ①
To analyze the stability properties of the closed-loop system for ①1 in the presence of uncertainty (due to the need to approximate the unknown dynamics), we introduce a more general notion of stability about a closed set A (see, e.g., 224, and the Appendix for a definition). When A {0). this coincides with the standard notion of stability about an equilibrium point. Intuitively, set stability w.r.t. to A is measured by closeness and convergence of solutions to the set A. To this end, define the distance from æ to A by ||~||A = ynf ||x 3/1-
Set invariance 3 plays an important role in our analysis.
Definition 1 (Forward Invariance). set Ω RR" said to be forward invariant for (2) if u0 implies that zi) E for all 1.20
Ω
Definition 2 (Region of Attraction). For closed forward invariant set A that is uniformly asymptot- ically stable (AS), the region of attraction is the set of initial conditions in 'D such that the solution for the closed-loop system (2) is defined for all i and ||=(()]|A +
06.
Remark 1. Any set satisfying Definition] 2 called a region of attraction. The ROA is the largest set contained in D satisfying Definition 2
Definition 3 (Lie Derivatives). The Lie derivative of continuously differentiable scalar function
V D + IR over vector field and nonlinear controller u is defined
0v
n
0V
V
f1 u).
(3)
Oz:
Da:
3

---

The lie derivative measures the rate of change along the system dynamics.
The following standard I. Lyapunov theorem for the UAS property of compact invariant set. Theorem 1 (Sufficient Condition for UAS property). Consider the closed-loop nonlineur system 2
Let 'D a compuct invariant set of this system. Suppose there exists continuously differentiable function V D + R that is positive definite with respect to A, i.e.,
V(z) 0 Vo E A and V(x) > 0 Ve E D A,
(4)
and the lie derivative is negative definite with respect to A, i.e.
VvV(x) 0 VD D A.
(5)
Then, is UASfoo the system.
See [24 35 for sufficiency and necessity of Lyapunov conditions for set stability under more general settings. The function V satisfying (4) and (5) called a Lyapunov function with respect to A.
From the forward invariance of level sets of Lyapunov function follows that these sets provide an estimate of the ROA (see [22
Lemma 1 (Region of Attraction with Lyapunov Functions). Suppose that V satisfies the conditions in Theorem 7 Denote
: {x e D Vx) cJ. For every e >> 0, v is region of attraction for the closed-loop system
3 Learn and Stabilize Dynamics with Neural Lyapunov Functions
In this section, we show how to use two shallow neural networks to learn the dynamics and find a valid neural Lyapunov function. The first network is designed to learn the dynamics shown in (1) and the second network aims to identify a valid neural Lyapunov function and its corresponding nonlinear controller. The algorithmic structure be found in Fig. and the pseudocode in Algorithm
Bounded inputs U
Learn the dynamics f(r.u)
@(x.u)
Estimate of B
k(x)
(b(kk())
States
Learn Neural Lyapunov function Vs nonlinear controller
SMT Solver with Eq. (11)
added for Ve and
Couterexamples
No
UNSAT?
Yes
Veis valid Neural Lyapunov function
Section 3.2
Figure 1: The schematic diagram of the proposed algorithm.
3.1 Learn the Unknown Dynamics
According to the well-known universal approximation theorem (9. shallow neural networks are able approximate the right-hand side fx, u) of the nonlinear system ( arbitrarily well. Here we use a one-hidden-
feedforward neural network, denoted as ø(x, u), conduct this regression task with mean square loss. For notational convenience, we slightly overuse notation of Φ to denote both the the learned dynamics and the parameters that define the function. Note that if we use the tanh or sigmoid function as activation functions, the output layer should not have such activation functions, is not bounded in most cases.

---

When learning the dynamics, f is regarded as function of two variables, x and u. The input dimension of the neuron network is (n + m). and output dimension is n. The training data of z and are sampled uniformly and independently over their respective spaces. In most robotic systems the input is provided by motors, which is typically saturated in practice. To reflect this, we use the activation function tanh to simulate this property. The format of the controller is
= x(x) = Co(kx + b),
(6)
where C' is a constant matrix, determined by the saturation property of the controller in real systems, which defines the bounds of U. k and are the weight matrix and bias vector, respectively, which are initialized with an LQR controller based on the linearized system I = Ar + Bu. The bias b is chosen such that f(0,, (b) O, i.e., the origin an equilibrium point for the closed-loop system (2). Note that the bias vector b is not updated in the learning process.
3.2 Neural Lyapunov Function and Nonlinear Controller
Following learning the dynamics using é the other neural network is designed learn nonlinear controller and neural Lyapunov function simultaneously during the same training process. The detailed structure can be found in the Appendix. Lyapunov function with data generated by the learned dynamics, which is an approximation of the actual dynamics, we rewrite (4 and (5) as follows to accommodate for approximation errors:
worth mentioning that since we train the
V(0) O, and Vo E ()) V(x) > and VvV(x) < -3.
Here B is a positive real number, which can be determined follows.
Assume that (z, u) is a pair of unsampled state and inputs, and (y. v) is its nearest known sample used in training testing the neural network for learning the dynamics. Let ó > 0 be such that [1 u) (v. u)]l < 8 holds for all such (z. u) and (y. v) and let M > 0 be such that || 11 || < M for all æ E D. Denote a as the maximum of the 2-norm loss among all known samples, which can be from either the training dataset or the test dataset. Then the bound on the generalization error can be calculated as
(x, u) ((,, w)ll S (1 u) - f(y, 1) (I ov, w) + lo(., v) - 6(x; u)ll
B
(8)
S K5 + KgO <
M
where ff and & are Lipschitz continuous with respective Lipschitz constants K K and /3 is some sufficiently large constant. Then, choosing 3 to satisfy (8) implies that
OV dz
3
V (zV(z) - VaV(z) <
[Ilf(x,<(z)) olz, x(x))] < M = B.
(9)
M
In view of 7 and 9b, we have
(x)( (ZV(z)+B+ - 0, Vr E DV(0),
(10)
which implies that the actual dynamics is also stable with the obtained neural Lyapunov function.
Here, calculate K₂ by using LipSDP-network. developed in [13, and M can be determined by checking the inequality with an SMT solver. An initial guess of is needed according to some prior knowledge, and it will be re-computed in each epoch with (8).
valid neural Lyapunov function can be guaranteed by the SMT solver with all the Lyapunov conditions written as falsification constraints in the form of first-order logic formula over reals []
(x)
2 2 A (V(x)= S SOV Σ
(11)
where E is a numerical error parameter, which is explicitly introduced for controlling numerical sensitivity around the origin. If the SMT solver returns either UNSAT this means that the falsification constraint is guaranteed not to have any solutions and confirms all the Lyapunov conditions are met. If the SMT solver returns 8-SAT, this means there exists at least one counterexample under the 5- 6-weakening condition [16] that satisfies the falsification conditions.
5

---

We use & to denote the parameter vectors for a neural Lyapunov function candidate Vg. The parameters 0 and l are found by minimizing the following cost function, which is modification of the so-called empirical Lyapunov risk in [5] by adding one more term @Y as we need / to be small as well:
1 k(0,k) - N 1=1
Σ
N
σv C1 max (-Vo 0) max (0, (2 +CaV3(0)+Cal
(12) dr
where C1, C2. C3 and C4 are tunable constants. The cost function can be regarded as the positive penalty of any violation of the Lyapunov conditions in (4) and (5). Note that the ROA can also be maximized by adding L2-like cost term to the Lyapunov risk with L(A. k)
N
Σ ii=1 |
a.oo (xt), where a is a tunable parameter, as shown in the original paper S
Algorithm 1 Neural Lyapunov Control with Unknown Dynamics
1: function LEARNINGDY (AMiss(Xams U(bd4))
2:
Set learning rate (r), input dimension (n + m), output dimension (n)
3: repeat
4:
f + N-NNo(a)
Output of forward pass of neural network
5:
Compute MSE L(f,
6:
< V L(f.
> Updates Weights using SGD
7: until convergence
8: return &
9:
end function
10:
function YEEARINGGYYPUNOVOXX fe. k
11: Set learning rate (a), input dimension (n), output dimension (1)
12:
Initialize feedback controller to LQR solution A/
13: repeat
14:
Vo(z), u(x) (z)
Output of forward pass of neural network
15:
(zV(2) + Ei= dr, [o](())
ay
16:
Compute Lyapunov risk L(O,A) 0 0 LO, k)
18:
+ k a L
> Updates Weights using SGD
until convergence
20:
return V/
end function
22:
function FALSIFICATION( u, Vo, 6,,, ,3)
Encode conditions from (1T)
24: Use SMT solver with 8 to verify the conditions
return satisiiability
26:
end function
27:
function MAIN()
28:
input initial guess of bound (3), parameters of LQR (1'44), radius (e), precision (6*), sampled
states X, sampled inputs U
29:
+- LEARWIXGDYNAMCSSX.C
U(bdd))
30:
while Satisfiable do
31:
Add counterexamples to X
32:
Vg. u + LEARNING-LXXPUNOO(XX.. &. k
33:
update 3 according 8
34:
CE < FALSIFICATION( u, V..
35:
end while
36:
end function
4 Theoretical Guarantees
In this section, we analyze the theoretical guarantees of using neural networks to learn to control an unknown nonlinear system and a Lyapunov function for certifying the closed-loop stability.

---

4.1 Approximation guarantee of unknown dynamics
Our analysis provides stability guarantees for the unknown system by rigorously quantifying the errors using Lipschitz constants of the unknown dynamics and its neural approximation. To this end, we need a theoretical guarantee that extends the universal approximation theorem, stating that we can approximate the Lipschitz constants and function values by a neural network to an arbitrary precision.
Theorem 2. (Approximation of Lipschitz constants). Suppose that K C IR" is compact set. (a) If K + R is L-Lipschitz in the uniform norm, i.e.
lf(x)) - f( & L||x- - yllso,
(13)
then for every > 0 there exists a neural network of the form δ(x) C(a (wr + b)) for C¹ (R) and not polynomial,
E R b R and C E R&x" for some k E N such that sup,ek lf(x) <(x) < e and ó has a Lipschitz constant of L + e in the same norms as (b) ff K + R is L-Lipschitz in the two norm, i.e.
If(x) f(u)l S L - yy12,
(14)
then for every there exists a neural network & of the same form such that s K
[(x))
((x)) < and & has Lipschitz constant of L+ /Vntn/e + I.)
in the same norms as 144.
The idea of the proof is to first approximate f by smooth function F and then approximate F by a neural network and the details can be found in the Appendix. Remark 2. The equivalence of norms gives an upper bound on the Lipschitz constant for all norms.
4.2 Existence of neural Lyapunov functions
As theoretical guarantee we show that it is possible train neural network as Lyapunov function, provided that a Lyapunov function exists. According to converse Lyapunov theorems (24. 35]. Lyapunov functions do exist when the origin is UAS. More specifically. we show that the learned neural network satisfies the Lyapunov conditions outside some neighborhood of the origin that can be chosen to be arbitrarily small in measure. The idea will be to perform an under- approxiappoiiiioonnn of the domain 'D in controlled way. Let (IR", ((RB", ), 1)) denote the standard measure space where B(R") is the Borel o-algebra and p is the Lebesgue measure. The following lemma from [33] states that it is possible to arbitrarily under-approximate open sets by compact sets in measure.
Lemma 2. For every open set O E B((R) such that μ(O) < co and every > 0, there exists a compact set K such that μ(O \ K)= < c.
By the pointwise approximation of the universal approximation theorem, it is not possible to satisfy the Lyapunov conditions on D as this set contains the origin. However, if there is a Lyapunov function for (2) that a neural network could learn and if practical stability (i.e., set stability w.r.t. a sufficiently small neighborhood of the origin) sufficient, Theorem 3 states that there exists neural network satisfying the Lyapunov conditions on a compact set K except on a closed neighborhood B of the origin that is UAS. Moreover, this approximation can be controlled in measure. The details of the proof can be found in the Appendix.
Theorem 3. Suppose that the origin is UAS for system 2 and I is a forward invariant set contained in the ROA of the origin. Fix any 7/1, 72 > 0. There exists forward invariant and compact set K C. I satisfying the under approximation μ((T) \ K) < 711 On K there exists a neural network V that satisfies the Lyapunov conditions on K \ A, where i closed neighborhood of the origin. The neural Lyapunov function V can certify that a closed invariant set B containing A and satisfying ((B), A) < ?22 is UAS. Furthermore, the set K is contained in the ROA of B.
An important feature of Lyapunov functions is that the level sets approach the ROA. We can show that the neural Lyapunov function Vo has such a property. Details can be found in the Appendix.
4.3 Asymptotic Stability Guarantees of Unknown Nonlinear Systems
With the theoretical guarantee of learning a neural Lyapunov function established above, we show that the neural network trained with the learned dynamics is robust, that is this neural network also
7

---

satisfies the Lyapunov conditions with respect to the actual dynamics f. Since the SMT solver verifies the Lyapunov conditions outside of some e-ball which is not necessarily forward invariant, the following technical assumption helps bridge this gap. The assumption is mild, because for the nonlinear system to be stabilizable, it reasonable to assume that it has a stabilizable linearization. A linear system å = Ax + Bu is said to be stabilizable if there exists matrix K. such that A + BK is Hurwitz, i.e., all eigenvalues of A + BK have negative real part. If (A, B) is stabilizable, then the gain matrix K can be obtained by an LQR controller.
Assumption 3 (ROA of LQR Controller). Suppose that the linearized model i: = Ax + Bu from Assumption 2 is stabilizable. Consequently, an LQR controller and a quadratic Lyapunov function can be found such that the origin is UAS for the closed-loop system 2 Furthermore, we assume that the set Be which is not verified by a SMT solver lies in the interior of a ROA of the closed-loop system, provided by the quadratic Lyapunov function.
Since this E-ball is small, we further assume that the level sets of the Lyapunov function are contained in the ROA of the LQR controller.
Assumption 4 (Controlled Level Sets), Denote B := {= ||-||| S $). Let V be continuously differentiable function satisfying the Lyapunov conditions on D \ Be. Suppose that there exists constants 0- < C1 C2 such that the following chain of inclusions holds
Sa) c B. (xED:
V(x s2),
(15)
and {x E D: (z) S c2 lies in the interior of the ROA of the closed loop system provided by the quadratic Lyapunov function.
(Stability Guarantees for the Unknown System) Let & be the approximated dynamics of right-hand side of the closed-loop system (2) trained by the first neural network. There exists neural Lyapunov function V which is learned using & and verified by an SMT solver that satisfies the Lyapunov conditions with respect the actual dynamics f. Furthermore, if the system satisfies Assumption 3 and V satisfies Assumption 4 then the origin is UAS for the closed-logy system (2).
Theorem 4.
The details of this proof can be found in the Appendix. This theorem proves that if the dynamics are approximated to sufficient precision then the neural Lyapunov function satisfies the Lyapunov conditions on D \ B3 for the actual dynamics. Furthermore, if the level sets of the neural Lyapunov function are sufficiently well behaved and the set Bg excluded from SMT verification is small then this learning framework certifies that the origin is UAS for the actual system
Experiments
In this section, we demonstrate the effectiveness of the proposed algorithm on learning the unknown dynamics and finding provably stable controllers as well as neural Lyapunov functions for various classic nonlinear systems. In all the following problems, we a two-layer neural network with one hidden layer for both learning the dynamics and learning the neural Lyapunov function. For learning the dynamics, the number of neurons in the hidden layer varies from 100 200 without output layer activation function as stated before, and we call this neural network FNN for convenience. However, for learning the neural Lyapunov function, there are six neurons in the hidden layer for all the experiments, and we name this neural network VNN in short. Regarding other parameters, we use the Adam optimizer for both FNN and VNN, and we use dReal as the SMT solver, setting the precision 8* for the falsification as 0.01 for all experiments. All the training of FNN is performed on Google Colab with 16GB GPU, and VNN training done on GHz 6-Core Intel Core i5.
5.1 Van der Pol Oscillator
As starting point, we test the proposed algorithm on the nonlinear system without input first to show its effectiveness in learning unknown dynamical systems and finding the valid neural Lyapunov function. The Van der Pol oscillator is a well-known nonlinear system with stable oscillations as a limit cycle. The area within the limit cycle is the non-convex ROA, as shown in the Appendix. According to the algorithm described in Section 3 we learn the two nonlinear dynamical equations with 100 hidden neurons. To ensure an accurate model, we use 9 million data points sampled on (-1.5, 1.5) x (-1.5, 1.5), and the learning rate of the training process varies from 0.1 to le-5 to
8

---

acquire small enough With the learned dynamics, we aim to find valid Lyapunov function over the domain ||||| 1.2, and the obtained neural Lyapunov function shown in Fig. 2a The corresponding ROA estimate can be found in Fig. 2b as the black ellipse. For comparison, the ROAs found by the neural Lyapunov function and the classical LQR techniques in 22 using actual dynamics are also plotted, as the blue and magenta ellipses respectively. The phase portrait of the system is given as the grey curves with small arrows. It obvious that the neural Lyapunov function after tuning obtains a larger ROA. We also have comparable verified ROA for the system with the one obtained with actual dynamics based on the same neural Lyapunov approach, both larger than LQR case. The values of the parameters can be found in Table I The dynamics, the neural Lyapunov function, and the nonlinear controller for all experiments are described detail the Appendix.
Table 1: Parameters in Van der Pol Oscillator case
K
K
6
B
3.4599
5.197
5e-4
8.5e-3
1.249
0.02
0.2
Lyapunov Function
Van der Pal
Valid region
0.8
0.8
0.6
R
0.0
0.4
0.2
-05
0.2
-1.0
0.5
-1.0
0.0
-1.0
-0.5
0.5
005
4
0.5
-1.0
NN MN_Jeareed
1.0
NNLactual
Valid Reg ion
(a) Neural Lyapunov function
(b) ROA comparison with LQR
Figure 2: Neural Lyapunov function and the corresponding estimated ROA for Van der Pol oscillator.
5.2 Unicycle path following
The path following task is typical stabilization problem for a nonlinear system. Here, we consider path tracking control using a kinematic unicycle with error dynamics (4. With the learned dynamics é, neural Lyapunov function can be learned on the valid region ||æ||| < 0.8, and the neural controller set as tanh(kz + b). The ROA comparison with the LQR method can be found in Fig. Ba Apparently, the neural network method yields larger estimated ROA, compared to the classical LQR approach in which the level set is determined by considering some relaxation of the largest reasonable range of linearization for practical systems under a small angles assumption (< } given the fact that the actual dynamics is unknown.
The parameters for this valid neural Lyapunov function and the learned dynamics in this case are listed in Table The Lipschitz constant Ký computed by using the bound ||ا S /m|l lla. where J, is the Jacobian matrix of f and m is the number of rows of Jy. Note that a can be the maximum of the 2-norm loss over a test dataset as stated Section 3.2 since what we need here is the discrepancies between the actual value and the approximated value of some known samples. In this regard, we can train FNN with fewer data samples, which is more computationally efficient. Then top of that, much larger dataset uniformly sampled over state and input spaces is used to calculate a, which contributes to a smaller ö. We implement the same approach for the inverted pendulum case well.

---

Table 2: Parameters in unicycle path following case
K
K
8
a
Dz
< 45
108
le-4
7e-3
4.43
0.1
0.1
Path Follwing
Region of Attraction
0.72
MN
0.6
LQR
0.90
Region
Valid Region
0.4
0.75
2-
0.56
enor (tad)
Angular velecity
0.2
0.0
0.45
0.40
-04
0.15
-2
0.24
0.00
-0.8
-0.15
0.08
Distance error de
Angleirad:
(a) ROA comparison for path following
(b) ROA comparison for inverted pendulum
Figure 3: Comparison of obtained ROAs for path following and inverted pendulum.
5.3 Inverted pendulum.
The inverted pendulum is another well-known nonlinear control problem. This system has two state variables 0, and one control input u. Here, 0 and respectively represent the angular position from the inverted position and angular velocity. The valid domain is ||>||| < 4. The similar ROA comparison is shown in Fig. 3b where the LQR approach uses the same function as given in [5]. The details regarding the bounds and / are given in the Appendix.
6 Conclusion
This paper explores the ability of neural networks to approximate an unknown nonlinear system with sufficient precision and find neural Lyapunov function as well as a feedback controller to stabilize the unknown dynamics. Provable guarantees are also provided with the help of bounds on the approximation error and partial derivatives of the Lyapunov function. Moreover, experimental results show that the proposed approach outperforms the existing classical approach given part of the dynamics is known. The algorithm only tested on low-dimensional systems. How to address this issue for high-dimensional systems is an interesting future research direction.
Acknowledgements
This work was funded in part by the Natural Sciences and Engineering Research Council of Canada (NSERC), the Canada Research Chairs (CRC) program, and the Ontario Early Researcher Awards (ERA) program.
References
[1] Felix Berkenkamp, Riccardo Moriconi, Angela P Schoellig, and Andreas Krause. Safe learning of regions of attraction for uncertain, nonlinear systems with gaussian processes. 2016 IEEE 55th Conference on Decision and Control (CDC), pages 4661-4666 IEEE, 2016.
[2] Felix Berkenkamp, Matteo Turchetta, Angela Schoellig, and Andreas Krause. Safe model-based reinforcement learning with stability guarantees. Advances in neural information processing systems, 30, 2017.
[3] Franco Blanchini. Set invariance in control. Automatica, 35(11):1747-1777, 1999.
10

---

[4] Ricardo Carona, A Pedro Aguiar, and José Gaspar. Control of unicycle type robots tracking. path following and point stabilization. In International Proceeding of IV Electronics and Telecommunicationn. Citeseer, November 2008.
[5] Ya-Chien Chang, Nima Roohi, and Sieun Gao. Neural Lyapunov control. Advances in neural information processing systems, 32, 2019.
[6] Shaoru Chen, Mahyar Fazlyab, Manfred Morari, George J. Pappas, and Victor M. Preciado. Learning Lyapunov functions for hybrid systems. In Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control, pages 1-11, Nashville Tennessee, May 2021. ACM.
[7] Shaoru Chen, Mahyar Fazlyab, Manfred Morari, George Pappas, and Victor M Preciado. Learning region of attraction for nonlinear systems. In 2021 60th IEEE Conference on Decision and Control (CDC), pages 6477-6484, IEEE, 2021.
[8] Alessandro Chiuso and Gianluigi Pillonetto. System identification: A machine learning per- spective. Annual Review of Control, Robotics, and Autonomous Systems, 2:281-304, 2019.
[9] George Cybenko. Approximation by superpositions of sigmoidal function. Mathematics of control, signals and systems, 2(4):303-314, 1989.
[10] Hongkai Dai, Benoit Landry, Lujie Yang. Marco Pavone, and Russ Tedrake. Lyapunov-stable neural-network control. arXiv:2109. 14152 [cs, eess), September 2021. arXiv: 2109. 14152.
[11] Charles Dawson, Zengyi Qin, Sicun Gao, and Chuchu Fan. Safe nonlinear control using robust neural Lyapunov-barrie functions. Conference on Robot Learning, pages 1724-1735. PMLR, 2022.
[12] Milad Farsi, Yinan Li, Ye Yuan, and Jun Liu. A piecewise learning framework for control of unknown nonlinear systems with stability guarantees. In Learning for Dynamics and Control Conference, pages 830-843. PMLR, 2022.
[13] Mahyar Fazlyab, Alexander Robey, Hamed Hassani, Manfred Morari, and George Pappas. Efficient and accurate estimation of lipschitz constants for deep neural networks. Advances in Neural Information Processing Systems, 32, 2019.
[14] A. F. Filippov. Differential equations with discontinuous righthand sides, volume 18 of Mathe- matics and its Applications (Soviet Series). Kluwer Academic Publishers Group, Dordrecht, 1988. Translated from the Russian.
[15] Nathan Gaby, Fumin Zhang, and Xiaojing Ye. Lyapunov-Net: A Deep Neural Network Architecture for Lyapunov Function Approximation. WwXiv=2109.13333 [cs, math), September 2021. arXiv: 2139.13359.
[16] Sicun Gao, Jeremy Avigad, and Edmund M Clarke. 8-complete decision procedures for satisfiability over the reals. International Joint Conference on Automated Reasoning, pages 286-300. Springer, 2012.
[17] Sieun Gao. Soonho Kong, and Edmund M Clarke. dreal: An SMT solver for nonlinear theories over the reals. In International conference on automated deduction, pages 208 214. Springer, 2013.
[18] Kurt Hornik, Maxwell Stinchcombe, and Halbert White. Multilayer feedforward networks are universal approximators. Neural networks, 255):359-366, 1989.
[19] Jeen-Shing Wang and Yen-Ping Chen. A fully automated recurrent neural network for unknown dynamic system identification and control. IEEE Transactions on Circuits and Systems I: Regular Papers,
June 2006.
[20] Yu Jiang and Zhong- Ping Jiang. Robust adaptive dynamic programming. John Wiley Sons, 2017.
11

---

[21] Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. International conference on computer aided verification, pages 97-117. Springer, 2017.
[22] H.K. Khalil. Nonlinear Control. Always Learning- Pearson, 2015.
[23]
Larissa Khodadadi, Behzad Samadi, and Hamid Khaloozadeh. Estimation region attraction for polynomial nonlinear systems: A numerical method. ISA Iransactions, 53(1):25-32, 2014.
[24] Yuandan Lin, Eduardo D Sontag, and Yuan Wang. A smooth converse Lyapunov theorem for robust stability. SIAM Journal on Control and Optimization, 34(1):124-10) 1996.
[25] Matteo Marchi, Bahman Gharesifard, and Paulo Tabuada. Training deep residual networks for uniform approximation guarantees. In Learning for Dynamics and Control, pages 677-688. PMLR, 2021.
[26] Luis G. Matallana, Aníbal M. Blanco, and J. Alberto Bandoni. Estimation of domains of attraction: A global optimization approach. Mathematical and Computer Modelling, 52(3- 4):574-585, August 2010.
[27] Arash Mchrjou, Mohammad Ghavamzadeh, and Bernhard Schölkopf. Neural Lyapunov redesign. arXiv preprint arXiv:2006. 03947,, 2020.
[28] Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. International conference Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340. Springer, 2008
[29] A. Papachristodoulluu and S. Prajna. A tutorial on sum of squares techniques for systems analysis. In Proceedings of the 2005, American Control Conference, 2005., pages 2686-2700. Portland, OR, USA. 2005, IEEE.
[30] Gianluigi Pillonetto, Francesco Dinuzzo, Tianshi Chen, Giuseppe De Nicolao, and Lennart Ljung. Kernel methods in system identification, machine learning and function estimation: A survey, Automatica, 50(3):657-682, 2014.
[31] Allan Pinkus. Approximation theory of the MLP model in neural networks. Acta Numerica, 8:143-195, 1999.
[32] Spencer M Richards, Felix Berkenkamp, and Andreas Krause. The Lyapunov neural network: Adaptive stability certification for safe learning of dynamical systems. In Conference on Robot Learning, pages 466-476. PMLR, 2018
[33] H.L. Royden and Fitzpatrick. Real Analysis. Prentice Hall, 2010.
[34] J.T. Schwartz and H. Karcher. Nonlinear Functional Analysis. Notes on mathematics and its applications. Gordon and Breach, 1969.
[35] Andrew R. Teel and Laurent Praly. A smooth Lyapunov function from class-KLL estimate involving two positive semidefinite functions. ESAIM: Control, Optimisation and Calculus of Variations. 5:313-367, 2000.
[36] Vrushabh Zinage and Efstathios Bakolas. Neural Koopman Lyapunov Control. arXiv:2201.05098 [cs, eess), January 2022. arXiv: 2201.05098.
Checklist
1. For all authors...
(a) Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope? [Yes]
(b) Did you describe the limitations of your work? [Yes] See Appendix A.4
(c) Did you discuss any potential negative societal impacts of your work? [N/A]
12

---

(d) Have you read the ethics review guidelines and ensured that your paper conforms to them? [Yes]
2. If you including theoretical results...
(a) Did you state the full set of assumptions of all theoretical results? [Yes] See Section and Section
(b) Did you include complete proofs of all theoretical results? [Yes] See Appendix A.2
3. If you ran experiments...
(a) Did you include the code, data, and instructions needed to reproduce the main experi- mental results (either in the supplemental material or as a URL)? [Yes] See Section and Appendix [A.3 where the link of the code is provided.
(b) Did you specify all the training details (e.g., data splits, hyperparameters, how they were chosen)? [Yes] See Section S and Appendix (A.e [A.3
(c) Did you report error bars (e.g.. with respect the random seed after running experi- ments multiple times)? [N/A]
(d) Did you include the total amount of compute and the type of resources used (e.g., type
of GPUs, internal cluster, or cloud provider)? [Yes] See Section [
4. If you are using existing assets (e.g., code, data, models) or curating/releasing new assets...
(a) If your work uses existing assets, did you cite the creators? [Yes] This paper follows up on a recent work of [5], and the code is developed based on this paper as well. Citation of the results from this paper be found in Section 3 and Section 5
(b) Did you mention the license of the assets? [N/A]
(C) Did you include any new assets either the supplemental material or as URL. [Yes] The link of the code can be found in Appendix A.3
(d) Did you discuss whether and how consent using/curating? [N/A] The dataset we use is generated by ourselves
obtained from people whose data you'l 're
(c) Did you discuss whether the data you are using/curating contains personally identifiable information or offensive content? [N/A]
5. If you used crowdsourcing conducted research with human subjects...
(a) Did you include the full text of instructions given to participants and screenshots, if applicable? [N/A]
(b) Did you describe any potential participant risks, with links to Institutional Review Board (IRB) approvals, applicable? [N/A]
(c) Did you include the estimated hourly wage paid participants and the total amount spent on participant compensation? [N/A]
13


Reviews:
[{"review_id": "scoLZxMgLjB", "reviewer": "Reviewer_Y9Y1", "summary": "This paper proposes a neural architecture that can (1) learn dynamics, (2) find a Lyapunov function and corresponding nonlinear stabilizer simulatenously. Using a satisfiability modulo theories (SMT) solver is also applied to verify the Lyapunov conditions of the candidate Lyapunov function. The authors claim that simultaneous learning of both the function and stabilizer helps to draw stability guarantees and overall better performance. This paper contains detailed theoretical guarantees and multiple experimental evidence, including comparison studies with existing methods.\n", "questions": "1. I am interested in using a solver in the algorithm. How did you choose an SMT solver for the experiments? Was there an extenstive ablation study for choosing an appropriate solver?\n", "limitations": "Even though most of the claims are sound, I also believe that the amount of experiments that are shown in this paper is limited, and the network sizes used in this work are relatively small. I am concerned about the general usability of this model for the complex nonlinear dynamical system, which is a core claim of this paper. The generality of the method needs to be validated with bigger data and larger neural networks.\n", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "This is overall a solid paper that retains theoretical and empirical novelties for challenging nonlinear control problems. This paper provides detailed theoretical guarantees and various experimental results. Meanwhile, I have also noted some concerns about the proposed methodology. I hope to see a response to these points during the rebuttal.\n\n\n### Strengths\n\n* This paper is quite well written. The authors put a lot of effort into providing relevant information in the Introduction and Preliminaries sections. The algorithm and learning schemes were easy to follow.\n* As far as I know, the proposed neural network architecture and algorithm are novel. These can contribute to finding the Lyapunov function for learning real-time physical systems with unknown dynamics. The theoretical results presented in this paper are sound.\n* This work presents trainable nonlinear controllers and Lyapunov function using neural networks. I think involving an SMT solver in the algorithm is a good approach.\n\n### Weaknesses\n\n* In the algorithm, I think the part of learning dynamics is not polished. The authors make assumptions that the dynamics are unknown. In this sense, oftentimes, it will be hard to collect trainable data, and it cannot be appropriate for a neural network to train dynamics by only using SGD. It seems that the overall performance of the algorithm is tightly coupled with the performance learned dynamics $f_\\phi$. Although Theorem 2 (\"an extension of the universal approximation theorem\") is presented, I think there are some real challenges that dynamics learning struggles. I can imagine multiple realistic issues regarding model complexity and data, so the learning dynamics might fail.\n\n* In the experiments, it would be better if there was a metric to compare ROA estimation performance between the proposed approach and LQR. I cannot grasp \"how much\" learning the Lyapunov function outperforms LQR.", "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": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "ZhtIbsM1Dp8", "reviewer": "Reviewer_psi4", "summary": "This paper proposed a framework to learn the non-linear system and control it with a neural controller and certified Lyapunov function. The system asymtotic stability can be proved by the negative Lie derivative of Lyapunov function. The satisfiability of Lyapunov function is achieved by running the SMT solver and learning framework iteratively. The effectiveness is demonstrated by 3 illustrative experiments.", "questions": "1. In Assumption 1 and line 166, the distance of (x,u1) and (y,u2) is a bit ambiguous with undefined “-” operator. It’s better to denote (x,y) as the concatenated vector for clarification.\n2. Can you provide the proof for theorem 5 from your reference [29]? \n3. Theorem 2 claims the existence of 1-hidden-layer neural network $\\phi$ to approximate the unknown dynamics, based on universal approximation theory. However, this only proves the existence but not the actual learn  $\\phi$ would satisfy such approximation accuracy. Similar for theorem 5. For instance, in line 503 of appendix, I’m wondering how to prove the actual $V_{\\phi}$ satisfy the Lyapunov condition given theorem 5 only claims the existence?\n4. I’m curious how to approximate M in line 167. If upper bound of $\\lVert \\frac{\\partial V}{\\partial x}\\rVert $is approximated by sampling then this is not a guarantee. Same question applied to other Lipschitz constants.", "limitations": "This paper does not have potential negative societal impact.", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 2, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths\n\n1. The paper structure is easy to follow. The experiments are well organized and helpful for theorem illustration.\n2. Under the framework of [1], The paper provides the proof of Lyapunov function existence and stability guarantee by quantifying the errors among unsampled states and nearest training samples.\n\n[1] Ya-Chien Chang, Nima Roohi, and Sicun Gao. Neural Lyapunov Control. In arXiv:2005.00611 [cs, eess, stat], December 2020. arXiv: 2005.00611.\n\nWeaknesses:\n\n1. With many of the methods inherited from previous [1], other than the theoretical improvement, I suggest the authors to include the methodology difference of this paper and [1], along with the experimental comparison. \n2. The formation of the problem(low dim system) and neural network structure are relatively simple. It would be interesting to see how the method applies in more complex system.\n3. The major improvement of this paper is the theoretical proof of stability over the previous work. However, I’m confused by the derivation logic. See my question 3 and 4. ", "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": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "FmKqPI2ol1", "reviewer": "Reviewer_KQuS", "summary": "The paper addresses the challenging task of guaranteeing asymptotic stability of an unknown nonlinear system by simultaneously learning the unknown dynamics (via a neural network) and a valid Lyapunov function for the learned dynamics. They provide an extension of the method proposed by Chang et. al (ref. [6]) to unknown nonlinear systems.\n\nThe problem is fundamental in the sense that it bridges the gap between theoretical control theory and data-driven control by being able to guarantee strong stability properties for unknown and general nonlinear systems.\n", "questions": "I have the following issues with your approach\n\n1) How do guarantee the existence of a feedback nonlinear controller that would steer the unknown nonlinear system to the origin? For instance, the recent work by Zinage et al. titled “Neural Koopman Lyapunov control” simultaneously learns a Koopman-based bilinear model and a valid Control Lyapunov Function (CLF) for the unknown nonlinear system and consequently guarantees the existence and computes a feedback controller by using the universal Sontag’s formula (provides necessary and sufficient conditions for asymptotic stability for controlled nonlinear systems) which is well studied in the control theory literature.\n\n2) How do you ensure that your designed nonlinear controller would ensure forward invariance for the unknown nonlinear system? In other words, how do you ensure your controller will keep the trajectories within the ROA?\n\n3) The SMT solver is not scalable and hence the computational time needed to compute a valid Lyapunov function increases exponentially as the dimension of the state increases. Consequently, this would restrict your approach to toy examples and therefore the applicability of your approach to real-world robotics problems like humanoids, manipulators, etc. becomes nontrivial.\n\n4) One of the Lyapunov conditions is that V(0)=0. This is a “hard constraint”. However, this condition is added as a soft constraint in your loss function. Hence after the learning process is over, V(0) might not be “exactly” zero which violates one of the Lyapunov conditions thereby not making it to learn a valid Lyapunov function.\n\n5) How is the value of beta chosen? It is mentioned that beta is kept relatively high so as to account for the approximation errors between the unknown nonlinear system and the learned system. I believe that if that is the case it might be sometimes difficult for the SMT solver to satisfy one of the Lyapunov conditions involving beta. It would be beneficial to add a table describing the influence of beta on the computational time required by the SMT solver to generate counterexamples.\n\n6) How do you guarantee the learning process finally converges i.e it is possible to reach a state where there are no more counterexamples that satisfy the falsification constraint?\n\n7) The proof of Theorem 4 is basically from the logic presented in Section 3.2 (Eqns. 8,9 and 10). I would suggest that you add this theorem before Eqns. 8, 9, and 10 and remove it from Appendix (page 14)\n\n8) For some nonlinear systems, there does not exist any linear feedback controller that could stabilize the nonlinear system (however a nonlinear feedback controller exists). In view of that, the controller design in your paper is restricted to only a linear feedback controller (Lines 12-18 of Algorithm 1) which might not steer the nonlinear system in some cases.\n\n9) Please elaborate on how Theorem 6 helps in the proof.\n\n10) I think some important references are missing which are relevant with your work. For instance, the papers titled\n“ Neural Lyapunov redesign”\n“A ‘universal’ construction of artstein’s theorem on nonlinear stabilization”\n“ Neural Koopman Lyapunov Control”\n\n", "limitations": "I would suggest adding a section to discuss the limitations of this approach. For instance, based on the following question\n1) Does the learning framework finally converges?\n2) SMT solver scalability?\n3) Existence of linear feedback controllers?\n4) Forward invariance when a linear controller is used?", "rating": 7, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "The strength of the paper is as follows:\n1) To the best knowledge of mine, this is the first paper that attempts to provide stability guarantees for unknown nonlinear systems\n\nThe weakness of the paper is as follows:\n1) Since the SMT solver is not scalable, the approach is restricted to low-dimensional problems and might not be suitable for real-world robotics applications\n\n2) The convergence of the algorithm depicted in Figure 1 is not clear.\n\nMore details about the approach are presented under \"Questions\"", "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": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}]

Author rebuttal:

Decision: Accept