Certifying Stability of Reinforcement Learning Policies using Generalized Lyapunov Functions
Authors: Kehan Long
Jorge Cortes
Nikolay Atanasov
Venue: NeurIPS 2025 poster ()
Keywords: Lyapunov Stability
Reinforcement Learning
Generalized Lyapunov Stability
Stability of Reinforcement Learning Policies
Primary area: theory
TL;DR: We construct generalized Lyapunov certificates by augmenting value functions with residual terms to certify the stability of control policies from optimal control or reinforcement learning.

Abstract: Establishing stability certificates for closed-loop systems under reinforcement learning (RL) policies is essential to move beyond empirical performance and offer guarantees of system behavior. Classical Lyapunov methods require a strict stepwise decrease in the Lyapunov function but such certificates are difficult to construct for learned policies. The RL value function is a natural candidate but it is not well understood how it can be adapted for this purpose. To gain intuition, we first study the linear quadratic regulator (LQR) problem and make two key observations. First, a Lyapunov function can be obtained from the value function of an LQR policy by augmenting it with a residual term related to the system dynamics and stage cost. Second, the classical Lyapunov decrease requirement can be relaxed to a generalized Lyapunov condition requiring only decrease on average over multiple time steps. Using this intuition, we consider the nonlinear setting and formulate an approach to learn generalized Lyapunov functions by augmenting RL value functions with neural network residual terms. Our approach successfully certifies the stability of RL policies trained on Gymnasium and DeepMind Control benchmarks. We also extend our method to jointly train neural controllers and stability certificates using a multi-step Lyapunov loss, resulting in larger certified inner approximations of the region of attraction compared to the classical Lyapunov approach. Overall, our formulation enables stability certification for a broad class of systems with learned policies by making certificates easier to construct, thereby bridging classical control theory and modern learning-based methods.

Certifying Stability of Reinforcement Learning Policies using Generalized Lyapunov Functions
Kehan Long Jorge Cortés Contextual Robotics Institute
Nikolay Atanasov
University of California San Diego
(k3long, cortes, natanasov)@ucad edu
Abstract
Establishing stability certificates for closed-loop systems under reinforcement learning (RL) policies is essential move beyond empirical performance and offer guarantees of system behavior. Classical Lyapunov methods require a strict stepwise decrease in the Lyapunov function but such certificates are difficult construct for learned policies. The RL value function is natural candidate but it be adapted for this purpose. To gain intuition,
is not well understood how we first study the linear quadratic regulator (LQR) problem and make two key observations. First, Lyapunov function be obtained from the value function an LQR policy by augmenting it with residual term related to the system dynamics and stage cost. Second, the classical Lyapunov decrease requirement be relaxed to a generalized Lyapunov condition requiring only decrease on average over multiple time steps. Using this intuition, consider the nonlinear setting and formulate an approach to learn generalized Lyapunov functions by augmenting RL value functions with neural network residual terms. Our approach successfully certifies the stability of RL policies trained on Gymnasium and DeepMind Control benchmarks. We also extend our method to jointly train neural controllers and stability certificates using a multi-step Lyapunov loss, resulting in larger certified inner approximations of the region of attraction compared the classical Lyapunov approach. Overall, our formulation enables stability certification for a broad class of systems with learned policies by making certificates easier to construct, thereby bridging classical control theory and modern learning-bast based methods.
Introduction
Designing and certifying stable control policies is core challenge in both control theory and reinforcement learning (RL). Although RL methods are capable learning policies that optimize long-term performance, their stability guarantees are often lacking. The classical Lyapunov theory [Lyapunov, 1992] offers principled framework for certifying stability but constructing a function that satisfies the required stepwise decrease condition is often challenging in practice. While value functions from optimal control or RL encode long-term cumulative cost, they do not naturally satisfy the Lyapumov stability conditions.
We propose certifying stability using a generalized notion of Lyapunov function [Fürmsinn al., 2023, 2025] that replaces the stepwise decrease condition with multi-step, weighted decrease criterion, allowing temporary increases over a finite horizon. As result, constructing a generalized Lyapunov stability certificate is casier, enabling stability verification for broader class of policies and systems.
For linear systems with quadratic cost under discounted optimal control, the value function typically fails to satisfy classical Lyapunov conditions due to the influence of the discount factor. Postoyan et al. [2017] show that augmenting the value function with quadratic residual term allows certifying
39th Conference on Neural Information Processing Systems (NeurIPS 2025).

---

stability via a linear matrix inequality (LMI), although the guarantees are conservative with respect to the discount factor. Leveraging this insight, we show that augmenting the value function with a quadratic residual leads to a valid generalized Lyapunov function, which certifies stability for boarder range of discount factors.
Building on the success of our approach in the linear setting, we extend it to nonlinear systems, where classical Lyapunov analysis is substantially more difficult. We augment value functions learned by PPO RL algorithms PPO [Schulman et al., 2017]. SAC [Haarnoja et al., 2018]) with a neural residual term to form generalized Lyapunov functions, and jointly learn state-dependent multi-step weights to satisfy the generalized decrease condition. This joint learning scheme enables certification of nonlinear RL policies in settings where classical Lyapunov functions are challenging to construct by learning generalized certificates that tolerate non-monotonic behavior along trajectories.
In addition to showing stability of fixed policies, we extend our approach to support the joint synthesis of stable neural controllers and generalized Lyapunov certificates. Prior works [Chang et al., 2019, Wu et al., 2023, Yang et al., 2024] frame this problem as learning a controller- certifcaee pair that maximizes the volume of a certifiable region, while iteratively training on counter-exann coumtes-xxapless where Lyapunov conditions fail. We incorporate our generalized multi-step condition into this formulation and show that it enables larger formally verifiable inner approximations of the region of attraction compared to standard one-step Lyapunov training.
Contributions. In summary, we make the following contributions:
We introduce an approach for certifying stability of reinforcement learning policies by constructing generalized Lyapunov functions, composed of the policy's 's value function and a learned neural residual. Empirically, our formulation certifies policies on Gymnasium [TTwwer et al., 2024] and DeepMind Control Suite [Tassa al., 2018] benchmarks where classical single-step Lyapunov methods fail.
We show analytically that, for the linear quadratic regulator (LQQR) problem, the validity of the proposed generalized Lyapunov function can be certified by set of LMIs.
We extend the formulation to jointly learn a control policy and a stability certificate using generalized multi-step Lyapunov loss, resulting in larger certified regions of attraction compared to classical Lyapunov approaches.
We provide an open- implementation of method at https: com/ ExistentialRobor weepootiiic/eeeeeaaieeee /et///eeeeaeeeeeeaaaaaaee Solicdoooccccccccliiiieeeeeeeeee
Optimal control [Bertsekas, 2012] and reinforcement learning (RL) [Sutton et al., 1998] offer a variety of principled techniques for designing control policies to optimize the per- formance of intelligent agents and dynamical systems. In the special case of linear systems with quadratic rewards, the optimality and stability of LQR policies [Anderson and Moore, 1990] are well understood. However, despite variety of methods for synthesizing policies (e.g., PPO [Schul- man et al., 2017], SAC [Haarnoja et al., 2018], and DDPG [Lillicrap et al., 2015] are among the most widely used) for nonlinear systems with nonlinear costs, very few techniques available for certifying the stability of the resulting closed-loop system.
Related Work.
Several works have explored connections between Lyapunov stability [Lyapunov, 1992] and RL, mainly in the context of safe RL. Perkins and Barto [2002] proposed a safe RL formulation by learning to switch among hand- sand-designed Lyapunov- stabbee controllers. Berkenkamp et al. [2017] developed a model- based RL algorithm that uses Gaussian process dynamics and Lyapunov verification to safely improve policies while guaranteeing stability with high probability. Chow et al. [2018] formulate Lyapunov-basee method for safe RL in constrained Markov decision processes. using linear constraints to ensure safety during training. Hejase and Ozguner [2023] regularized policy training by penalizing violations of learned Lyapunov condition to encourage stability in autonomous driving. Mittal et al. [2020] learn Lyapunov function from suboptimal demonstrations and incorporate it as a terminal cost a one-step model predictive control formulation to improve stability.
In parallel, there has been growing interest in jointly learning policies and Lyapunov functions from data to obtain stability guarantees for nonlinear systems. Chang et al. [2019] trained Lyapunov certificates with formal verification via satisfiability modulo theories. Other works constrain neural architectures to satisfy Lyapunov conditions structurally [Gaby et al., 2022. Boffi et al., 2021], apply mixed-ine -itteer programming [Dai et al., 2021]. Long et al. [2023] studied neural distributionally robust Lyapunov functions under additive uncertainty. Wu et al. [2023] learn provably stable controllers

---

for discrete-timg nonlinear systems by jointly training policy and Lyapunov function, with formal verification via mixed-intedd -ixeeer linear programs. Yang et al. [2024] use gradient-guided falsification for training controller-certfficu pair, and apply formal verification via a, 3-CROWN [Wang et al., 2021] to certify stability post training. See also Dawson al. [2023] for a comprehensive survey.
2 Problem Formulation
Consider the discrete-time system:
x f(x;; uk), X EEECRR, Us Eu C Rm.
(I)
where X is open and f X' u + X' is locally Lipschitz. A control policy X u for the system can be obtained by solving an infinite-horizon discounted optimal control problem:
(x0) min JTT (Xo)
[(xi; (ONN,TT(xs)) (xx)),
(2)
km
s.t. X
f(X2,, π (x:),,
E N, (xx) E U,
where (0, 1) is a discount factor and É(x, u) is a stage cost (or reward in the case of maximization). specifying the performance criterion.
learning methods usually solve a problem like (2) to obtain a policy and associated value function J We consider deterministic problem in our theoretical development for simplicity but apply our approach to stochastic problems in the evaluation (Section 5). Note that, while reinforcement learning methods work with stochastic control policies during training, only the mode of the final trained policy is used at test time, allowing us to treat it as deterministic.
Optimal control and reinforcement
Given policy we are interested in certifying whether it stabilizes the closed-loop system:
X = f(x:: π (xx)).
We assume π (0,)) = Om f(O,,, 0..) On, (.... 0..) 0, and O,, E X. so that the origin is an equilibrium point of the system. Stability can be certified by identifying Lyapunov function.
Definition 2.1 (Lyapunov Function). Consider the closed-loop system (3). A continuous function X Rxo is Lyapunov function if it satisfies:
V(O.)) (f((x, (x))) (xx)
V(x) Vx X' {0,}. Vx E X' {0,).
(4a)
(4b)
Lyapunov functions certify the asymptotic stability of the system, as stated in the following result. Theorem 2.2 (Asymptotic Stability via Lyapunov Function [Khalil, 1996, Theorem 3.3)). If there exists Lyapunov function V as in Definition 2.1, then the origin x = O,, is an asymptotically stable equilibrium of the system (3).
When æ arises from (2), the corresponding value function J is also available. We are interested in whether J can itself certify the stability (3) or assist constructing a certificate.
Lyapunov Stability Analysis for Linear Quadratic Problems
To understand the relationship between discounted value function J obtained from (2) and Lyapunov function V certifying stability of the closed-loop system (3), we first study simple setting with linear system and quadratic stage cost.
Consider the discrete-time linear system: X Ax + Bug, where X E RR". uy I and A. B are known constant matrices.
Choosing the stage cost in (2) as {(x, u) x Qx + u Ru with leads to the discounted LQR problem [Anderson and Moore, 1990]. The optimal value function J7 (x) x P,,x is quadratic, where P., solves the discounted Algebraic Riccati Equation (ARE):
- > 0 and R > 0
P. A ( P.B P.B R -' B A+Q
(5)
3

---

The corresponding optimal feedback gain is K policy n (Xis) = X Under this policy, the closed-loop system evolves as
PB"P,,, -
which yields the
X
F XR, Xk.
where F
A+
(6)
Although J satisfies the discounted Bellman equation, it is well understood that it does not guarantee Lyapunov decrease due to 7 E (0, 1) [De Farias and Van Roy, 2003]. Moreover, verifying stability by directly analyzing the eigenvalues of F and solving the discounted ARE (5) nontrivial due to its nonlinear dependence on This motivates the idea [Postoyan et al., 2017] of constructing valid Lyapunov functions by augmenting J with residual term. To formalize this, we first state standard assumptions that ensure the existence of stabilizing policy and well-defined value function. Assumption 3.1. The pair (A, B) is stabilizable and the pair (A, C) detectable.
The following result shows the existence of a Lyapunov certificate derived from the value function.
Theorem 3.2 (Lyapunov Stability via LMIs for Discounted LQR [Pustoyan et al., 2017]). Suppose
Assumption 3.1 holds. Consider optimal policy गł, and value function J obtained from the LQR problem with discount ",. Let P denote the solution to the undiscounted ARE in (5) (with n = 1). If
there exist symmetric positive definite matrices So, S1 > 0 and scalars w, 0 such that:
A S.A
Su S1 - = S.A
S
B S - 30, aP S1,
(7)
then the function V(x) == (7( + _ Sax is a Lyapurov function for the closed-loop system (6), and certifies global exponential stability for any discount factor satisfying 7 =ta'
Theorem 3.2 shows that while the discounted value function J may not satisfy the Lyapunov condition on its own, can be modified into valid certificate when y is sufficiently large. The required residual term and computable lower bound y obtained by solving set of LMIs. However, this bound often conservative compared to the true stability threshold y obtained by analyzing the closed-loop dynamics via the discounted ARE, illustrated in the following example.
Example 3.3 ([Postoyan et al., 2017, Example 1]). Consider the scalar system Ik+11 = 22g + Uk
with stage cost [(r, u) x² + u² The optimal policy is uy K2TK where
= ( - - (5n - 1)"
The closed-loop multiplier F 2 K and the origin is globally exponentially stable if and only if F+ < 1, which is equivalent to t > 7" =1/3. However, applying the LMIs from Theorem 3.2 yields feasible solution for r 0.8090, which is significantly more conservative.
Example 3.3 highlights the limitation of classical Lyapunov analysis and motivates the development of an alternative formulation with less conservative conditions for certifying stability.
4 Generalized Lyapunov Stability and Applications to Linear Systems
Building on the observation from Example 3.3, we introduce a generalized notion of Lyapunov stability [Fürnsinn et al., 2023, Defimition 2.2] that relaxes the classical pointwise decrease condition.
Definition 4.1 (Generalized Lyapunov Function). Consider the closed-loop system in (3). continuous function V X - R2z0 is generalized Lyqpunov function if it satisfies (4a) and there exist an integer M E Nyo and state-dependent non-negative weights a (x),..., (x) such that
Σ
(x(x)21 21,
(8)
and, for any X') } the following generalized decrease condition holds:
Σ xx V(xi))
V(x) 0,
M
where X,41 f(x;, (xx)) with xg

---

Condition (9) generalizes the decrease requirement in (4b) by allowing temporary increases in V over individual steps, provided that its weighted average decreases over a finite horizon of length M. We state the stability guarantee provided by a generalized Lyapunov function in the next theorem.
Theorem 4.2 (Asymptotic Stability via a Generalized Lyapunov Function), Consider the closed- loop system in (3), and assume the policy is Lipschitz X. If there exists a generalized Lyapunov function V X + Rzo as in Definition 4.1, then x = 0,, is an asymptotically stable equilibrium.
See Appendix A for the proof (adapted from [Fürnsinn et al., 2023, Theorem 21), and Appendix B for an explicit construction of a classical one-step Lyapunov function from a generalized Lyapunov function when the step weights ]
J are staee-indeenndet.
Remark 4.3 (Relation to k-Inductive Verification). The generalized Lyapunov condition in (9) can be viewed through the lens of k--sep inductive verification | [Brain et al., 2015, Anand et al., 2022, Wooding and Lavaei, 2024]. In particular, by selecting weights d1
0k-1 0 and σ M. condition (9) reduces to ((T++k) & (V which is analogous to a k-step Lyapunov decrease condition used in k-inductive reasoning. Classical k-induction requires strict decrease at the final step while permitting bounded increases in intermediate steps. In contrast, Definition 4.1 enforces decrease in weighted average across multiple steps, with the weights d; chosen adaptively or learned during training. This distinction provides additional flexibility, enabling certificates that may be easier to construct for nonlinear systems with learned controllers.
Returning to the LQR setting in Section 3, we consider certifying the stability of (6) via a generalized Lyapunov function. Building on Theorem 3.2, augment J with quadratic residual and require the composite function to satisfy (9), leading to a new set of LMIs for stability certification.
Theorem 4.4 (Generalized Lyapunoy Stability for Discounted LQR via LMIs). Suppose Assump- tion 3.1 holds. Consider optimal policy T and value function J², obtained from the LQR problem
with discount ?, Let P denote the solution to the undiscounted ARE in (5) (with 7 = 1). If there exist symmetric positive definite matrices So, Sp.......,
scalars w, 01..... CM > 0, and weights
I M 2 0 satisfying EM 0; 2 M, such that:
E M
S
So
A
So
M B
30,
(10a)
01 M
B
S.A
T M
B
RR.
A
A
-
H M B
A S
M
30,- Vi I,..., M 1,
(10b)
0++1 M
B
A
G++1 M
S
R
o&P P S vi=1 1, 1,...,M.
(10c)
then the function
T[x)= 1 - Sox
(11)
a generalized Lyapunov fanction in the sense of Definition 4. (with constant weights), and certifies that the origin is globully exponentially stable for the closed-loop system (6), provided that:
ONW Man
62
01
Y max
Maz
M(++oj))
(12)
The proof is provided in Appendix C.
Remark 4.5 (Feasibility of Multi-Step LMIS). Note that when 01 = M and o, = 0 for all 2 < i < M, Theorem 4.4 recovers the classical Lyapunov result in Theorem 3.2. Therefore, if the original one-step LMIs (7) are feasible, then feusible solutions for (10) also exist. Empirically, the multi-step formulation can certify stability in additional cases where the one-step condition is infeasible, effectively enlarging the set of stabilizable systems. Formal characterization of this weaker feasibility property is left for future work.
Remark 4.6 (Choice of o; Weights). While the multi-step formulation enables optimizing the weights MM to minimize the certified lower bound on 7 in (12), finding globally optimal weights is challenging due its non-conveiity nature. In practice. heuristics such as grid search for small M and random sampling with local refinemetss for larger M are sufficient to achieve noticeable improvements over the one step baseline.
5

---

Example 4.7 (Example 3.3 Revisited). We illustrate the benefits of the generalized multi-step LMIs from Theorem 4.4 in Example 3.3. We first focus on the case M 2. Figure shows how the certified bound on varies with the choice of weights
and 02, constrained by + 02 = 2. Since the undiscounted value function (?y = 1) satisfies the Lyapunov condition, this bound is capped
The classical Lyapunov setting (2) (2, 0) yields a conservative bound of > 0.8090, whereas optimizing over 0 and d2 improves the bound to 7 > 0.6229 (2), (1.54, 0.46), Another important observation is that increasing M significantly reduces the certified lower bound on progressively approaching the true stability threshold 7- 1/3, shown in Figure
1.0
Certified bounds
Certified Bound
0.8
True y bound
0.9
V bound
0.7
0.8
0.6
01 0_
0.5
0.7
Min Certified
Classical LF (0) 2)
0.6
0.3
0.0
0.5
1.0
1.5
2.0
2
8
10
01
Number of steps (M)
Figure I: Certified y bound for M 2.
Figure 2: Certified y bound versus M.
Nonlinear Systems: Stability Certification of RL Policies
Inspired by the treatment of linear systems described in Section 4, we first formulate post-hoc approach certify stability of policies for nonlinear systems obtained by RL using generalized Lyapunov function. The key observation from Theorem 4.4 is that augmenting the optimal value function with residual term can result in valid generalized Lyapunov function, as (11). Here, we use the same idea to form generalized Lyapunov functions for nonlinear systems with unknown dynamics, which is a problem considered by RL. The value function and policy obtained by an RL algorithm are typically parameterized by neural networks. Let TRL be a pre-trained RL policy (e.g.. obtained by [Schulman et al., 2017, Haarnoja al., 2018, Hansen al., 2022]), and let J denote its corresponding learned value function. We consider generalized Lyapunov candidate as:
Vx; 01) = J (x) + (x;;; 01),
(13)
where (xx 01) is neural residual correction. To allow more flexibility in the generalized Lyapunov condition (9), we introduce a step-weighting network (x; 02) E R2% that outputs non-negative weights over a rollout horizon of length M. The weights are required to satisfy ΣM" (x; 02) M. These weights are then used to construct the generalized Lyapunov decrease condition:
F(x:) = M Σ (xs; 02) V(X++=:))) (1 - a) ((xx;
(14)
where ā 10 1) is user-specified decay parameter. We train the networks p(; 01) and o- 02) jointly by minimizing a loss that penalizes violations of the generalized Lyapunov condition:
C( 02)
N Σ (ex(
(15)
(8) 1 where {x( Mi=1 are sampled initial states.
Remark 5.1 (Network Architecture). In practice, the learned value function J may not be optimal, hence, may not satisfy J (0,) = O. To ensure that the generalized Lyapunov candidate satisfies V(O;; 01) = O and is positive definite, we modify (13) as:
(16) where 3 > 0 a small constant (the term B||x||| enforces strict positive definiteness for x # O,, and improves numerical stability near the origin.) The step-weighting network o (x;; 02) E 20 ends with
V(x; 01) = J (x) JT (O,)) |p(x; 01) (00:; (1)x+
softmax layer scaled by M, ensuring the output weights satisfy 1/ EM (x(x;0)) = =.

---

Remark 5.2 (Equilibrium Behavior). In practice, RL policies often converge to neighborhood near the origin rather than the origin itself. Thus, we train and verify the generalized Lyapunov condition over the set X B(0;; 6), where ,i 6) denotes a ball of radius ó around the origin.
Training and Evaluation Setup. We evaluate method two standard RL control benchmarks from Gymnasium [Towers et al., 2024] and the DeepMind Control Suite [Tassa et al., 2018). RL policies TRL and their corresponding value functions J are trained using implementations from Raffin et al. [2021], Hansen et al. [2022]. We collect a total of rollout trajectories by simulating the closed-loop system under RRL. with each trajectory 7 {x k= starting from randomly sampled initial state x0 Additional training and architecture details are provided in Appendix D.
Inverted Pendulum Swingup. We consider the inverted pendulum environment from Towers et al. [2024] with parameters m = 1, 1, = 10, and control limits |u] < mggl = 2. The state space is [- T) x [-8,8) 8). Due to tight torque limits, the pendulum must swing back and forth to build momentum before reaching the upright position. This makes it challenging synthesize policy with a Lyapunov certificate valid over the entire state space. Prior work (Yang et al., 2024, Long al., 2024] has shown that regions where stability can be verified small neighborhoods near the upright position, failing to cover the full swing-up trajectories. In contrast, modern RL policies
typically restricted to
discover effective swing-up behaviors but lack stability guarantees. Our method bridges this gap: we take a trained SAC policy Haarnoja et al. [2018] and apply our generalized Lyapunov function training with M = 15. Figure 3 shows the generalized Lyapunov function values along several trajectories from different initial states. As expected, the function exhibits non-monee m--ooooooo behavior but shows overall decline over the planning horizon. Figure visualizes the Lyapunov function across the state space. Figure 5 plots the residual F(x,) defined in (14), verifying that the generalized decrease condition is satisfied throughout the domain.
270
200
240
210
180
150
100-
120
90
-775
60
100.0
-1125
25
09
-2
Steo
Iradand)
tradianal
Figure 3: Generalized Lyapunov Figure 4: Generalized Lyapunov function values along trajectories.
Figure 5: Generalized Lyapunov de- condition.
function value over state space.
Cartpole Swingup. We consider the cartpole swing-up task from Tassa et al. [2018]. The system state is represented [r, cos(f), sin(O), àt, é), where is the cart position, 0 is the pole angle, and the remaining terms are their velocitics. The goal is to swing the pole upright = 0 and stabilize the TD-MPC policy [Hansen et al., 2022] and apply our certificate training (15) with M 20. Figure visualize the generalized Lyapunov condition across three representative 2D slices of the state space, with the remaining two states fixed at zero. The generalized decrease condition satisfied throughout these slices, suggesting asymptotic stability of the RL policy.
position at O. We
180
-15
20
30
5.
60
G
60
-75
100
-00
-005
120
140
-180
Thena (radlana)
Figure 6: Generalized Lyapunov decrease condition for the cartpole swing-up using TD-MPC policy.

---

In addition to qualitative visualizations, we quantitatively evaluate our learned certificates by sampling Nust states from the full state space and checking whether (14) satisfied. For each environment, we train certificates for multiple RL policies (the PPO policy fails to stabilize the cartpole from some initial states). As shown Table 1, the condition holds for all test states in both environments.
Table I: Percentage of sampled test states satisfying F(xx) S under different RL policies.
Environment
RL Methods
M
Nua
% Satisfying F(xe) I
Inverted Pendulum Cartpole
PPO, SAC. TD-MPC
15
10,000
100%
SAC, TD-MPC
20
1,000,000
100%
Concentration of Learned Step- Weights. To further analyze the learned generalized Lyapunov function, we examine the distribution of the learned step-weights across the horizon. For each trained policy, the step- weegh network was evaluated over 10, 000 uniformly sampled states from the state space, and the normalized weights were averaged across samples. The weights were then grouped into five equal bins corresponding to different segments of the Lyapunov horizon. Table 2 summarizes the fraction the total weight assigned each bin.
Table 2: Average fraction of total step- weight assigned to each portion of the rollout horizon. Results are averaged over 10,000 test states for each policy.
Environment Policy
Steps 0-20%
20-40%
40-60%
60-80%
80-100%
Pendulum PPO
12.3
11.4
16.7
21.8
37.8
Pendulum SAC
10.2
13.3
17.5
22.6
36.4
Cartpole SAC
10.8
10.5
16.2
25.6
36.1
Cartpole + TD-MPC
14.1
13.9
16.8
24.7
30.5
As shown in Table 2, the consistent concentration of weights toward the end of the horizon reveals a key strategy learned by our method. By assigning lower weights to initial steps and higher weights to later ones, the network effectively learns to tolerate initial non-monotonic transients in the Lyapunov candidate, focusing instead on ensuring decisive, weighted decrease over the full horizon. This behavior empirically realizes the central benefit of the generalized Lyapunov condition: providing a flexible yet formal basis for certifying complex neural policies.
Joint Synthesis of Stable Neural Policies and Certificates
So far, we addressed the certification of stability for fixed pre-trained control policies. In this section, we consider joint synthesis of neural controllers and Lyapunov certificates and employ formal verification inspired by Chang et al. [2019], Dai al. [2021], Wu al. [2023], Yang al. [2024]. Compared to prior methods, our generalized Lyapunov framework naturally extends this setting by replacing the standard one-step decrease condition with the proposed multi-step, weighted formulation in (9).
Definition 6.1 (Region of Attraction). The region of altraction (ROA) R C R" of the (locally asymptotically stable) origin for the diserete-time system (3) is the of all points from which the system trajectory converges to the origin, i.e., Xo E R. implies limg- X O,,
In general, precise characterizations of are challenging to obtain and one instead looks for suitable approximations, Here, we seek to jointly learn a policy π (x; Φ)) and a certificate function V(x; 0,) such that the closed-loop system X f(xg, π (xxx) is provably asymptotically stable and obtain at the same time an inner approximation S of the ROA R. Yang et al. [2024] formalized it as constrained optimization that maximizes the volume of Lyapunov sublevel set {x R
V (x) < p} under Lyapunov constraints
max 01.0
Vol(S)
(17a)
S.I.
V(On; 01) = V(x;01) 00 Vx Ex (Ox): V(x+110 01) (1-a)V 01) 5 Vx2 E ES
(17b)
(17c)
8

---

where ā E (0, 1) is user-specified decay parameter. To utilize generalized Lyapunov function, we replace (17c) with the generalized M-step condition for each X₁ S, with Σ (x())) 2 M:
M
1
F(xx) = M ox.(x))
- -x-aa)Vxx; 01) s O, (x 2 ug>g >0, 0, (18)
where E R250 is uniform lower bound on the weights. The condition (18) enables learning certificates that tolerate non-monotonic behavior along a trajectory, but it no longer guarantees that S is forward invariant. However, as Theorem 6.2 shows, S still defines valid inner approximation of the ROA and guarantees asymptotic stability of the origin.
Theorem 6.2 (Asymptotic Stability Relative to S). If the optimization problem (17) is solved with the generalized condition (18) instead of (17c), then S C RR.
See Appendix for the proof.
Training Formulation. Following [Yang et al., 2024], we reformulate the problem (17) into a learning objective by sampling states X2 X' and penalizing violations of the Lyapunov conditions using soft constraints. For each X; E DD we simulate M forward steps under the closed-loop dynamics and compute the generalized Lyapunov residual F(xx) defined in (18).
To enforce stability and domain constraints, we define the stability loss:
Lutab (xx) == ReLU (min (ReILU(F(xx)) + coH((x)), - (1))),
(19)
i=1 ReLUU(x++ Xup) + ReLU(xx, - x penalizes violations of the bounded domain X' = {x X x X x.p The inner min ensures that the generalized Lyapunov decrease condition is only enforced inside the certified region S.
where H(xx)) := Σ M
To expand the certifiable region, Yang et al. [2024] proposed surrogate region loss Eregion Σ₁=1 ReLU (V(x,; 01)/p 1), where the candidate states xj are obtained via random boundary sampling or projected gradient descent (PGD) to minimize (1)) PGD is also used for falsification by maximizing stability violations, generating additional training states for D.
The final training objective C(01. Φ) := Ex, (xx,) + C1 Ergginn + c2 c2l Φ111 where D contains states sampled randomly and generated by falsification.
Remark 6.3. Although the theoretical framework (Theorem 4.2) supports trainable weights a (x(x), including neural network parameterizations (see Section 5), certifying stability under jointly learned controllers, Lyapunov functiion, and weights remains computationally challenging with existing tools [Wang et al., 2021, Gao al., 2013]. In practice, we fix o; during training. For small values of M, we select the best-performing weight configuration via a simple grid search
Verification Formulation. After training, we verify that the generalized decrease condition holds within X' using the a-8-CROWN verifier [Wang et al., 2021J. We formally certify Lyapunov stability of the origin if the following holds for all X E X:
M A xh+t X (V(x+) p)
(-F(x)) 20
(20)
As Theorem 6.2 implics, if (20) holds for all X E X, then S is an inner approximation of R.
Evaluation. We evaluate our generalized Lyapunov synthesis approach three systems presented in [Yang et al., 2024]: inverted pendulum, path tracking, and 2D quadrotor (with a 6D state space). Detailed system dynamics and neural network architectures used are provided in Appendix F.
Figures and show the certified stability regions for different horizon lengths M. We use fixed step weights (a), ......) selected via grid search: for the inverted pendulum. (0.4, 1.6) for M-2 and (0.3, 1.5, 1.2) for M-3; for path tracking, (0.4, 1.6) and (1.2, 1.2, 0.6), respectively. As shown in the figures, multi-step training and verification yields consistently larger certifiable ROAS.
Table 3 reports the quantitative results, including the volume (S) and the verification time. The volume is estimated via Monte Carlo integration: we sample n = 10 points in X and compute the fraction satisfying V (x) S p. averaged across trials and scaled by the total domain volume. To assess

---

10
1-step
1-step
AngularVelocity (rad/s)
2-step
2 2-step
3-step
AngleError (rad)
3-step
-1
-5
-2
-10
-10
5
10
-3
-2
0
1
2
Angle (rad)
DistanceError (m)
Figure Certified ROAs for inverted pendulum.
Figure 8: Certified ROAs for path path-tracking.
robustness, we repeat each experiment 10 times with different random seeds and report the mean and standard deviation. The results confirm that our generalized stability formulation consistently certifies larger ROA volumes compared to the classical one-step Lyapunov approach. This improvement comes the cost of longer verification times, since bounding multiple intermediate states and their weighted combinations increases the complexity of bound propagation and branching decisions.
Table 3: Certified region volume (left) and verification time (right) under different M-step Lyapunov training. Abbreviations: I.P. Inverted Pendulum, P.T. = Path Tracking, 2.Q. 2D Quadrotor.
System
M
M
M
L.P.
42.9 1.2
76.7 1.3
89.2 = 1.2
11.7 + 0.5
21.5 0.8
39,2 1.3
21.8 1.8.000 0.6
23.6 0.5
23.9 +
0.5
19.5 1.0
36.7
2.Q.
103.5 + 1.8
109.1 + 2.0
113.7 + 2.0
2209.5 + 72.6
3858.7 + 112.4
5628.6 185.9
(a) Certified ROA volume (S).
(b) Verification time (seconds).
7 Conclusion, Limitations, and Future Work
We presented new approach for constructing stability certificates for closed-loop systems under policies obtained from optimal control and RI. We also showed that our method can be used for joint synthesis of neural policies and stability certificates. Rather than learning certificates from scratch, key insight is that the value function of a considered policy can be augmented with a residual term to obtain certificate candidate. We also replaced the classical Lyapunov decrease condition with generalized multi-step Lyapunov formulation, which provides asymptotical stability guarantees while improving learning flexibility. Our theoretical and empirical results show that this perspective enables construction more effective stability certificates compared to traditional Lyapumov approaches.
Our approach has several limitations. First, the certification horizon M is fixed during training, and it remains unclear how to determine the minimal viable M for given system. Second, the method has not yet been applied to high-dimensional systems such as humanoids or dexterous manipulators. Third, formally verifying neural policies (c.g., from RL). along with learned detendeeenddnt weights and certificate functions, remains computationally challenging with existing tools.
This work opens up several promising directions for future research. One key avenue is develop partial-state stability certification, providing guarantees for task-relevant components such as torso height velocity in humanoid locomotion rather than for the full system state, which improve both scalability and interpretability. formulation certify robust stability under bounded perturbations and stochastic disturbances, taking inspiration from input-to-state and robust Lyapunov theory. Another important direction is to relax the requirement of knowing the equilibrium state, allowing stability analysis when the equilibrium is unknown or non-isolated, as often occurs reinforcement learning, by inferring equilibria from data from the reward structure. Finally, investigating the connection between generalized Lyapunov conditions and optimality objectives may yield new insights for reward design and policy refinement in reinforcement learning.
second direction is to extend the generalized Lyapunov
10

---

Acknowledgments
We gratefully acknowledge support from ONR Award N00014-23-1-2353 and NSF Award CCF- 21 12665 (TILOS).
References
Mahathi Anand, Vishnu Murali, Ashutosh Trivedi, and Majid Zamani. K-inductive barrier certificates for stochastic systems. In ACM International Conference on Hybrid Systems: Computation and Control, pages 1-11, 2022.
Brian D. O. Anderson and John B. Moore. Optimal control: linear quadratic methods. Prentice- Inc., 1990.
Felix Berkenkamp, Matteo Turchetta, Angela Schoellig, and Andreas Krause. Safe model-based reinforcement learning with stability guarantees. In Advances in Neural Information Processing Systems, volume 30, page 908-919, 2017.
Dimitri Bertsekas. Dynamic programming and optimal control: Volume 1, volume 4. Athena scientific, 2012.
Nicholas Boffi, Stephen Tu, Nikolai Matni, Jean-Jacques Slotine, and Vikas Sindhwani. Learning stability certificates from data. In Conference on Robot Learning, pages 1341-1350. PMLR, 2021.
Martin Brain, Saurabh Joshi, Daniel Kroening, and Peter Schrammel. Safety verification and refutation by k-invariants and k-induction. In International Static Analysis Symposium, pages 145-161. Springer, 2015.
Ya-Chien Chang, Nima Roohi, and Sicun Gao. Neural Lyapunov control. In Advances in Neural Information Processing Systems, volume 32, 2019.
Yinlam Chow, Ofir Nachum, Edgar Duenez-Guzmant and Mohammad Ghavamzadeh. A Lyapunov- based approach to safe reinforcement learning. In Advances in Neural Information Processing Systems, volume 31, 2018.
Hongkai Dai, Benoit Landry, Lujie Yang, Marco Pavone, and Russ Tedrake. Lyapunov-stable neural-network control. In Robotics: Science and Systems, Virtual, July 2021.
Charles Dawson, Sicun Gao, and Chuchu Fan. Safe control with learned certificates: A survey of neural Iyapunov, barrier, and contraction methods for robotics and control. IEEE Transactions on Robotics, 3949)1779-1176,, 2023. doi: 10. 209/TRO.2022..22:333
Daniela Pucci De Farias and Benjamin Van Roy. The linear programming approach to approximate dynamic programming. Operations research, (1(6))850-88) 2003.
Annika Fürmsinn, Christian Ebenbauer, and Bahman Gharesifard. Relaxed feasibility and stability criteria for flexible-step MPC. IEFE Control Systems Letters, 7:2851-2856, 2023. doi: 10.1109/
(CSSSS2003332281555
Annika Fürnsinn, Christian Ebenbauer, and Bahman Gharesifard. Flexible-step model predictive control based on generalized Lyapumov functions. Automatica, 175:112215, 2025. ISSN 1005-1098. doi: http://owo.rrgooo.oooooaatttttte com/sci
112215. URL https: :tttps://www.c. http://wwwwiincciircc......
Nathan Gaby, Fumin Zhang, and Xiaojing Ye. Lyapunov-net: A deep neural network architecture for Lyapunov function approximation. In JEEE Conference Decision and Control, pages 2091-2096, 2022. doi:
Sicun Gao, Soonho Kong, and Edmund M Clarke. dreal: An smt solver for nonlinear theories over the reals. In International Conference Automated Deduction, pages 208-214. Springer, 2013.
Tuomas Haarooja, Aurick Zhou, Pieter Abbeel, and Sergey Levine. Soft actor-critic: Off-policy maximum entropy deep reinforcement learning with a stochastic actor. International Conference Machine Learning, pages 1861-1870, PMLR, 2018.

---

Nicklas Hansen, Xiaolong Wang. and Hao Su. Temporal difference learning for model predictive control. In International Conference on Machine Learning, pages 8387-8406. PMLR, 2022.
Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun. Delving deep into rectifiers: Surpass- ing human-level performance on imagenet classification. In IEEE International Conference Computer Vision, pages 1026-1034, 2015.
Bilal Hejase and Umit Ozguner. Lyapunov stability regulation of deep reinforcement learning control with application to automated driving. In American Control Conference, pages
2023.
Hassan Khalil. Nonlinear Systems. Prentice Hall, 1996.
Timothy Lillicrap, Jonathan Hunt, Alexander Pritzel, Nicolas Heess, Tom Erez, Yuval Tassa, David Silver, and Daan Wierstra. Continuous control with deep reinforcement learning. arXiv preprint arXiv: 02971, 2015.
Kehan Long, Yinzhuang Yi, Jorge Cortes, and Nikolay Atanasov. Distribationally robust Lyapunov function search under uncertainty. In Learning for Dynamics and Control Conference, pages 864-877. PMLR, 2023.
Kehan Long, Jorge Cortés, and Nikolay Atanasov. Distributionally robust policy and Iyapunov- certificate learning. IEEE Open Journal of Control Systems, 3:375-386, 2024. doi: 10.1109/ OJCSYS.2024.344009
Aleksandr Mikhailovich Lyapunow. The general problem of the stability of motion. International journal of control, 55(3)531--53, 1992.
Mayank Mittal, Marco Gallieri, Alessio Quaglino, Seyed Sina Mirrazavi Salehian, and Jan Koutník. Neural Lyapunov model predictive control: Learning safe global controllers from sub-optimal examples. arXiv preprint 2045: 2020.
Theodore J Perkins and Andrew G Barto. Lyapunov design for safe reinforcement learning. Journal of Machine Learning Research, 3DDec):803-832, 2002.
Romain Postoyan, Lucian Buşoniu, Dragan Nešić, and Jamal Daafouz. Stability analysis of discrete- time infinite-horizon optimal control with discounted cost. IEEE Transactions on Automatic Control, 62(6))2736-2744 2017. doi: 10. 16.1099/7
Antonin Raffin, Ashley Hill, Adam Gleave, Anssi Kanervisto, Maximilian Ernestus, and Noah Dormann. :asclne:: Reliable reinforcement learning implementationss Journal of Machine Learning Research, 22(268):1-8, 2021. URL http: www.elrrrrgpppppppppeeeee wttgp/ppppe//////000022/ 1364. html.
John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov. Proximal policy optimization algorithms. arXiv preprint arXiv: 2017. URL https://arziv... org/
abs/1707 (bb2/777000647.
Richard S Sutton, Andrew G Barto, et al. Reinforcement learning: An introduction, volume 1. MIT press Cambridge, 1998.
Yuval Tassa, Yotam Doron, Alistair Muldal, Tom Erez, Yazhe Li, Diego de Las Casas, David Budden, Abbas Abdolmaleki, Josh Merel, Andrew Lefrancq, et al. Deepmind control suite. arXiv preprint arXiv:1801.00690 2018
Mark Towers, Ariel Kwiatkowski, Jordan Terry, John U Balis, Gianluca De Cola, Tristan Deleu, Manuel Goulão, Andreas Kallinteris, Markus Krimmel, Arjun KG, et al. Gymnasium: A standard interface for reinforcement learning environments. arXiv preprint arXiv:2407.17033 2024.
Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsich, and J Zico Kolter. Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. Advances in Neural Information Processing Systems, 34, 2021.
Ben Wooding and Abolfazl Lavaci. Learning k-inductive control barrier certificates for unknown nonlinear dynamics beyond polynomials. arXiv preprint arXiv:2412.07233,, 2024.
12

---

Junlin Wu, Andrew Clark, Yiannis Kantaros. and Yevgeniy Vorobeychik. Neural Lyapunov control for discrete-tie time systems. Advances in Neural Information Processing Systems, volume 36, pages 2933,2955, 2023.
Lujie Yang, Hongkai Dai, Zhouxing Shi, Cho-Jui Hsich, Russ Tedrake, and Huan Zhang. Lyapunov- stable neural control for state and output feedback: A novel formulation. In International Confer- ence on Machine Learning, 2024, URL pestps://openrevieee net/ forum ? iid=ixiXXxXJJRR...
A Proof of Theorem 4.2
Proof. Attractivity. We first show attractivity. Fix any initial condition Xo E X') (0) and let (xx)a20
be the corresponding trajectory. For each & 2 0 choose an index
{(k) {I..... M) such that ((x++2()) < V(x+),
(21)
whose existence is guaranteed by (9). Define the strictly increasing sequence return indices
ko == O, kyt1 == kg + Elkg), j = =0011.... 0.1.....
(22)
for which, by construction,
0 kj+1 k M,
((xa)++) < V(xi;), 0,1.....
(23)
Due to the positive-definitenes of V. applying standard Lyapunov arguments on {V(T,,)) we conclude that lime, -00 V(xx,))
Because the gaps satisfy kj+1 - K2 < M and V is continuous, we have
lim Vxx) = 0.
(24)
k-
Finally, the positive-definiteness of V yields X2 - O as + co. Thus the origin is attractive.
Stability. Since both the system dynamics f and the policy π are assumed to be Lipschitz, the closed-loop map x f(x, (x)) is also Lipschitz on the forward-invariant set X. Let L denote the Lipschitz constant. Then, for all 0 < i < M and k 2 0,
|x++||| I L
(25)
Fix an arbitrary & > 0 and choose
8 : T,M-I
(26)
Consider any initial state with ||xo|| < 5. By construction of the return indices ky in (22) we have ||x;,_Il| S [|xe, for all j. so in particular
| < 6,
j = 0, 1,
(27)
For an arbitrary time index la pick j such that ki S k < k; + M. Applying (25) with i -- k2 < M and (27) yields
| L M-1 ||, || L M- E.
Because e was arbitrary, the c-8 condition holds and the origin is Lyapunov stable.
In conclusion, the origin is both attractive and Lyapunov-stable on X: therefore it is asymptotically stable relative X.
Remark A.1 (Exponential Stability). Suppose the function V X + E2o satisfies the positive definiteness condition (4a), and there exist constants 31, B2, p > 0 such that
|/ < V(x) S 3211x|IP, Vx E X.
(28)
Suppose further that V satisfies the strict generalized decrease condition for all E X,
M (xx - -
(29)
M
where a R20 + R20 is Class-K function. Then the origin O,, is exponentially stable.
13

---

B Construction of a Classical Lyapunov Function from a Generalized One
This appendix shows that when the generalized M-step Lyapunov decrease in Definition 4.1 holds with state-independent step weights, one can explicitly construct a classical one-step Lyapunov function, following a similar idea classical constructions that convert multi-step (non-monotone) decrease conditions into a one-step Lyapunov decrease 2. In contrast, when the step weights depend on the state, obtaining explicit closed-form classical Lyapunov function from the generalized certificate appears non-trivial; while asymptotic stability still follows from Theorem 4.2, deriving a simple one-step Lyapunov function construction in the state-dependent case is left for future work.
Assumption B.1 (Constant step weights). The step weights in Definition 4.1 are constant, i.e, there exist 01, оM 2 (independent of x) such that for all x E X \ (0),
M
M
1 M
Σ -x.V V(x) <0,
Σ., 2. M ==
1
21.
(30)
where X and X;+1 f(x,, (x,)) for - O..... -1
Lemma B.2 (Explicit construction of a classical Lyapunov function). Suppose V X - Rg0 satisfies Definition 4.1 and Assumption B.I. Without loss of generality, assume
Σ 0 M.
(31)
Define coefficients
1 M
0j = M
Σ Fi
1-1,
(32)
i=j+1
and the function
M-1
W(x) = Σ a(((((())))
(33)
where f denotes j-fold composition of the closed-loop map + f(x, π (x)). Then W is classical
Lyapunov function:
W(0) O,
W(x) > 0 Vx 0,
(34)
and it decreases strictly in one step:
Wf((x, (x))) (x) Vx + 0.
(35)
Proof. By (31) and (32), we have ag 1 and 0j > 0 for all j. Hence
(xx) 2 (x),
(36)
which implies (34). V is radially unbounded, then so W by (36).
Let {xt Ja20 be any closed-loop trajectory and define V& = V(x+). Using (33),
M
M-1
- -x(x)
Σ
az ajVk+1t>
Σ
a Vi+s
1=0
(37)
M-1
= +
Σ
(aj-1 ag) az)V + am -MM-VVMMM
1=1
By (32), aj-1 0g = //M for j 1,..., M 1 and aas-1 = OM /M, and by (31) we have
4g = 1. Substituting into (37) gives
1 M
W(x+-1) - W(xx)
Σ o. Vo4s Vz-
(38)
M
The right-hand side of (38) is strictly negative for all by (30), proving (35).
14

---

M Scaling the weights. If EE= > M, define o; == و== 0, Then o; 2 0 and Σ o; M.
Since د of E (0, 1). the left-hand side of (30) scaled down while V(x) is unchanged, so the strict inequality (30) remains valid. Hence (31) is without loss of generality.
C Proof of Theorem 4.4
For clarity, we present the detailed proof for the case M = 2. The general M- case follows analogously by extending the argument to multiple future steps.
Proof. We consider the generalized Lyapunov decrease condition over two steps:
1
(02 (x2V(xx-2) + V (xx++1) V(x+) O,
(39)
2
where 01, 02 2 0 and + 02 2.
Using the discounted Bellman equation for the optimal value function Vi+, (x++1) - (xx)) -(x,, u + (1 VV,
(40)
we can recursively expand the two-step generalized decrease condition for Vn. Direct computation yields:
(02 (X +
(x++++1)
-Vy+1)
(x(x))
VV
01
1x((x))
01
-((x,, u - 02
-
2 1[(xx+1,
2
[o
P
0
[x++1
02 (xx+1,, ub+1)
01
< |1411
x
l(xx uj!) (41)
19r-1-17
1)P
X
2
2
However, due to the presence of the discount factor y (0, 1), the value function V,, does not naturally satisfy the required decrease condition.
Following the approach in [Postoyan et al., 2017], introduce auxiliary quadratic function:
W(x) x Sox,
(42)
where So and x are design parameters.
Define the composite function:
(x)x = (x) W
(43)
Our goal to ensure that Y, satisfies the generalized Lyapunov decrease condition in (39).
We compute the change in the auxiliary function W(x) over two steps:
1
2 (o2 W (xx+2) + W (xx++))) W(x+)
2 2 + σ1 2 XIx x STSSXX))
(44)
Expanding the system dynamics
X Ax + Bu X = Ax + Bu
(45)
and substituting into (44), we express the change in W as
(xx+) + 01 (x(+1)))) W(x+)
2
01
(xx (A SoA - So)x + u B SoBu, + 2x A By
2
+ 2w
02
(xT_1 A S0AA441 + u B S + 2x A B,Bu41)).
(46)
15

---

To upper bound this change, we introduce positive definite matrices S1. S2 > 0 and impose:
2 (0 W (x6+2) + on W (x+++1) ((x))
02 X2 S1x: + 0n ((x,, ux) ((x++1,
S X S2x
(47)
Combining the changes in Vy and W, we obtain:
(02Y + +x (xx)
5 02 - Xk+1 Xk
1 S2
S 01 7- )
Xx.
(48)
2
Thus, ensure strict decay of Y,, it suffices require:
1 S2 // -Pp>>>1
(49)
S 11 - - 1) P 0.
(50)
This leads to the requirement that must satisfy:
22
01 2( + +a1) 20²
max
(51)
where 01,00 satisfy the comparison inequalities:
0g P,P 3 S1,
0ny Po S2.
(52)
Furthermore, by comparing (46) and (47), the auxiliary matrices must satisfy the following LMIs:
A
A
Su + S1 aQ
A
3 30,
(53)
2 B
S
B
B
2
Ø2
A
S
S2 w
A T
S
30.
(54)
B
S
" B
S RR
This concludes the proof.
D RL Certificates Training Details
D.1 Network Architectures
We use feedforward neural networks with LeakyReLU activations for both the residual network
(p(-,0) 01) and step-weighting network a-. 02). The architectures are summarized in Table 4. The residual network is initialized using Kaiming initialization [He al., 2015), and all biases are initialized to zero.
Table 4: Neural network architectures for the residual and weightigg networks.
Component
Architecture
Output
Residual Network
3 layers, width 64
Scalar value
Step-weighting Network
3 layers, width 64
MM-dimensional weights
D.2 Training Configuration
We train all networks using the Adam optimizer with initial learning rate of 5 10-4 Re- duceLROnPPlateau scheduler (factor 0.5, patience 500), and a batch size of 256 for 1000 epochs. Gradients are clipped at 5.0. We set the decay parameter to ā 0.02 and the slack to = 0.01. As discussed in Remark 5.2, we exclude a small ball around the origin during both training and evaluation. Specifically, we set 8 0.05 for the inverted pendulum and 8 0.5 for the cartpole.
16

---

D.3 Compute Resources
All experiments were run single workstation with NVIDIA RTX 4090 GPU, AMD Ryzen 7950X CPU, and 64 GB RAM. Training the Lyapunov certificate for the inverted pendulum takes approximately 40 minutes, and for the cartpole environment around 4 hours. These durations include all rollouts and training steps for both the residual and step-weight networks.
E Proof of Theorem 6.2
For clarity, we prove the result for M and assume 01, 02 are constants.
Proof. We restate the assumptions. Let the closed-loop system be:
Xk+1 = f(XE; (xx)),
and V: R R20 is continuous function satisfying
V(O,,) 0, V(x+) 0 Vxa E S (0.),
(55)
(o (x++1) + 02 02 (xx+2)) s (1 ax)((x);, Vxa E,
(56)
with 01.02 > a > and 01 02 2.
Attractivity. The attractivity proof follows as in Appendix A, we conclude lim X = On-
Stability. We follow the classical =-Ō Lyapunov proof in [Khalil, 1996, Thm. 3.3]. Fix an arbitrary radius and define
my == inf V(z). ||=||=
(57)
Because the s-sphere (x g" ||ж||| #} is compact and V is continuous, the infimum is achieved on E. Positive-defnniteness of further implies m. > 0. Define
2(1 -a) a)
0 0.
Because continuous at the origin and V(0) = 0, for every threshold vj > there exists a radius 8(m) 0 such that
| < 6(n) _ V(x) <1
Choosing me/c and setting ō = 8(ma/c), gives
| 5 V(x) mg
(58)
Now, pick any index & with xy e S and
| S. From (58), have the bound
V(*x) <
(59)
Using the two-step Lyapunov condition (56) and the fact that 01, 2 g. we obtain g(V(#x+1) ((x++2)) s 2(1 - V
= V(*x+)) S cV(x)), i= 1, (60)
Combining (60) with (59) gives
V(z+41) < mey
((x=2) < me.
By definition me, V(x)= < my implies ||ж||| < E; hence
| E,
|[ <.
(61)
Equation (61) shows that, starting from any state inside the 5-ball, the trajectory remains inside the prescribed e-ball.
Moreover, due to the strict decrease enforced by (56), it is not possible for both V(x++1) 2 V(x;) and V (xx+2) 2 (xx)) to hold simultancously. Therefore, at least one of the two future states must
17

---

satisfy V ((x++)) < (xx)) for i E {1,2}. hence the trajectory enters a strictly smaller sublevel set of V within two steps, allowing the generalized Lyapunov condition be re-applied.
We now distinguish two cases to formalize the re-application logic:
Case I: X E S. Then the generalized condition can be re-applied at X and since V(x++1) < <. the next steps X X will also lie within the c-ball by repeating the same argument.
Case 2: X & S. Then X1+2 E S, and again V(x++2) < < = ||x*+2|| < allowing the condition to be re-applied step + 2.
Conclusion. In both cases, the trajectory remains within the e-ball for all time, and the generalized decrease condition continues to hold along the sequence. Therefore, for all >> 0, there exists 5 > 0 such that:
|x01| < 5 proving Lyapunov stability of the origin relative S.
|xx <e vk 2
(62)
Therefore, we conclude that is a valid inner approximation of the ROA.
System Dynamics for Formal Verification
We describe below the continuous-time dynamics, control constraints, and verification domain X for each benchmark system used our evaluations. All systems are discretized using explicit Euler integration with time step of A/ 0.05
F1 Inverted Pendulum
The inverted pendulum is modeled single-link rigid body rotating about its base, subject to bounded torque control. The continuous-time dynamics are:
i w.
(63)
w sin(O)
8
u
(64)
mf2
mf²
where is the pendulum angle (upright at = 0), w is the angular velocity, and u is the control input. We use the following parameters: gravity = 9.81 m/s² mass m = 0.15 kg, length e 0.5 m, and damping coefficient 3 = 0.1.
The control input is saturated E [-6, 6] Nm. The state vector [0.w] T and the verification region is defined as:
X penduium ;= (x E IR2 0 E [-12, 12), 12, 12])
F.2
Path Tracking
We consider kinematic model for ground vehicle tracking circular path at constant forward speed u. The system state is x = [de, 0z] where de is the lateral distance to the reference path and 0g is the heading error. The control input is the steering angle. The continuous-time dynamics
d_ u sin).
(655
cos (0.)
0.
u
(66)
L
R de
where L = 1 m is the wheelbase length, R = 10 m is the radius of the reference path, and 2 m/s the constant forward speed. The control input is bounded by |u| 0.84.
The verification domain is defined as:
Xpach == {x E IR? de E 1-33), O [3333]
F.3 2D Quadrotor
The 2D quadrotor models rigid body with six states: horizontal and vertical positions pitch angle 0, and their corresponding velocities ă, غ, Ó. The system is controlled by two rotor thrusts
18

---

U2, and the continuous-timg dynamics are:
3 sin(O) + U2),
(67)
m
1
cos(O)(u) + +22) 9.
(68)
m
(U1 U2).
(69)
where m = -0.486 kg. L = 0.25 m, = 0.00383 kg m² and y = 9.81 m/s². The state vector is x [r, z, 0, 0J The control inputs are constrained to be within [0, 0.5 Weql where ule 2
w2
The verification domain is defined as:
Aquadrotor == {x E R x E (
x [- 2 x [-4,4]] x [-3,3]}
F.4 Neural Network Architectures and Training Parameters
We adopt the same network structures used in Yang et al. [2024]. The configurations are summarized Table 5. All networks use leaky ReLU activations.
Table Neural network architecture for each system.
System
Controller Network
Lyapunov Network
Inverted Pendulum
layers, width 8 layers, width 8
layers, widths [16, 16, 8]
Path Tracking
Quadratic form Quadratic form
2D Quadrotor
layers, width 8
19

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: The abstract and introduction accurately state the paper's two main claims: (1) stability certificate can be constructed by augmenting the value function of with residual term, and (2) the classical decrease condition in Lyapunov theory can be relaxed generalized multi-step Lyapunov condition. These claims supported by theoretical analysis and validated through examples and simulation results in Sections 4 to 6.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made in the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or
NA answer to this question will not perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results
be expected to generalize other settings.
is fine to include aspirational goals as motivation as long is clear that these goals are not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Justification:
The limitations are discussed in Section 7.
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create separate "Limitations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model sell-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested few datasets with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution is low or images are taken in low lighting. Or speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairesss.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory assumptions and proofs
20

---

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

---

some way (e.g., to registered users), but it should be possible for other researchers have some path reproducing or verifying the results.
5. Open access to data and code
Question: Does the paper provide open access to the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, as described in supplemental material?
Answer: [Yes]
Justification:
We open source our code and implementation details.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurlPS code and data submission guidelines (https://nips. cc/
for more details.
While we encourage the release of code and data, we understand that this might not be possible, "No" is acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for a new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurlPS code and data submission guidelines (https:
for more details.
The authors should provide instructions on data access and preparation, including how access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information as possible supplemental material (appended the paper) is recommended, but including URLs to data and code is permitted.
6. Experimental setting/details
Question: Does the paper specify all the training and test details (c.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification: All training and evaluation details provided in the Appendix D and Appendix F.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, or as supplemental material.
7. Experiment statistical significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer: [NA]
Justification: Our main results are based on verification of stability conditions, not stochastic evaluations or statistical comparisons. Therefore, notions such error bars or statistical significance do not apply.
Guidelines:
The answer NA means that the paper does not include experiments.
22

---

The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
The factors of variability that the error bars capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall
with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g.. Normally distributed errors).
should be clear whether the error bar is the standard deviation the standard error of the mean.
It is OK to report 1-sigma error bars, but should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful figures symmetric error bars that would yield results that are out of range (e.g. negative error rates).
show in tables or
error bars are reported in tables or plots, The authors should explain the text how they were calculated and reference the corresponding figures or tables in the text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed reproduce the experiments?
Question:
Answer: [Yes]
Justification:
We provide full compute resource details in Appendix D and in Section 6.
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental rums as well estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary failed experiments that didn't make into the paper).
9. Code of ethics
Question: Does the research conducted the paper conform, in every respect, with the NeurlPS Code of Ethics https attps://neurips: http///nurrrp.ppe wctppubicc/thicssuiiiiiiceeeeeee
Answer: [Yes]
Justification: This research does not involve human subjects, sensitive personal data, or potentially harmful applications. We have carefully reviewed the NeurIPS Code of Ethics and confirm that our work adheres to its guidelines.
Guidelines:
The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.
If the authors answer No. they should explain the special cireumstances that require deviation from the Code of Ethics.
The authors should make to preserve anonymity (e.g.. if there is special consid- cration due to laws or regulations their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive socictal impacts and negative socictal impacts of the work performed?
Answer: [NA]
23

---

Justification: This work proposes theoretical and algorithmic framework for stability certification of optimal control and reinforcement learning policies. It is foundational in nature and does not involve deployment, human interaction, or domain-speciin applications that would raise immediate societal concerns.
Guidelines:
The answer NA means that there is no societal impact of the work performed.
If the authors answer NA No, they should explain why their work has societal impact or why the paper does not address societal impact.
Examples of negatíve societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deploymentt of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and tied to particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology.
If there negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility ML).
11. Safeguards
Question: Does the paper deseribe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, scraped datasets)?
Answer: [NA]
Justification:
This paper does not release any models or datasets with potential for misuse.
Guidelines:
The answer NA means that the paper poses no such risks.
Released models that have a high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [Yes]
Justification: All external assets used in this work are properly cited. This includes simulation environments from Gymnasium [Towers et al., 2024] and the DeepMind Control Suite [Tassa et al., 2018 8), well baselines and architectures from Yang et al. [2024]. For formal verification, we reference and use tools from Wang et al. [2021], with appropriate credit and citations.
24

---

Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package or dataset.
The authors should state which version of the asset is used and, if possible, include URL.
The name of the license (c.g., CC-BY 4.0) should be included for each asset. For scraped data from a particular source (e.g.. website), the copyright and terms of service of that source should be provided.
If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswi thcode. com/ datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if has changed) should be provided.
this information not available online, the authors are encouraged to reach out to the asset's s creators.
13. New assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [NA]
Justification:
This paper does not release new assets.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/moodl part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset is used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing and research with human subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well as details about compensation (if any)?
Answer: [NA]
Justification: This paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then much detail as possible should be included in the main paper.
According to the NeurlPS Code of Ethics, workers involved in data collection, curation, other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
25

---

Justification:
This work does not involve human subjects or crowdsourcing and therefore does not require IRB approval.
Guidelines:
The answer NA means that the paper does not involve crowdsoureing nor research with human subjects.
Depending on the country in which research is conducted, IRB approval (or equivalent)
may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such the institution conducting the review.
16. Declaration of LLM usage
Question: Does the paper describe the usage of LLMs if it is an important, original, or non-standard component of the core methods this research? Note that if the LLM is used only for writing, editing, or formatting purposes and does not impact the core methodology, scientific rigorousness, originality of the research, declaration is not required.
Answer: [NA]
Justification:
The core method development does not involve LLMs.
Guidelines:
The answer NA means that the core method development in this research does not involve LLMs as any important, original, or non-standard components.
Please refer to our LLM policy (https: /ttpa///////ep..eeeeeeeeeeea cc/Confferences/2225 for what should or should not be described.
26


Reviews:
[{"review_id": "2lway9ReK8", "reviewer": "Reviewer_gbSe", "summary": "The paper considers identifying a Lyapunov function which is defined as addition of $M$-step value function induced by a policy $\\pi$ and a residual term. The Lyapunov function is adopted from the genearlized Lyapunov concept by Furnsinn et al. and the residual term is motivated from solving the discounted LQR problem by Postoyan et al.", "questions": "1. Remark 4.4 : The statement would benefit if it presents stronger result than feasibility other than that of classical Lyapunov problem. Can  we guarantee a weaker version of feasibility?\n\n2. How did the authors choose $M=15$ or $M=20$ in the experiments? \n\n3. What are the final values of $\\sigma_i(x)$ in the experiments? Does the final values of $\\sigma_i(x)$ provide any further insights?", "limitations": "yes;", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 3, "significance": 2, "originality": 2, "strengths_and_weaknesses": "**Strength**\n1. Theoretical contribution to the study of discounted LQR: The result of Furnsinn and Postoyan yields relaxed condition on $\\gamma$ in Theorem 4.3. \n\n2. Solid experimental results : The authors show that the proposed method indeed learns a valid Lyapunov function in simple experiments including Cartpole and inverted pendulum problems\n\n**Weakness**\n\n1. Even though deriving a relaxed condition on $\\gamma$ is a contribution, it is a result of  Furnsinn and Postoyan rather than proposing a new concept.\n\n2. The required method needs to know the equilibrium state (origin) to define Lyapunov function. In contrast to classical control, RL takes advantages when the equilibrium state is unknown. \n\n3. The experiments are quite limited to simple control problems, which follows from Weakness 2.", "was_revised": true, "final_justification": "My main concern was regarding the strength of the theoretical contributions, which I do not think differs much from the previous literature. Nonetheless, the paper’s primary contribution appears to be on the experimental side, focusing on learning a generalized neural Lyapunov function. As most of my concerns related to the experimental aspects have been addressed, and in agreement with the other reviewers, I am raising my score to Borderline Accept. Nonetheless, I do not have a strong stance in favor of the paper, as Reviewer A5kt noted, there is substantial overlap with existing literature.", "rebuttal": "We thank the reviewer for their time and thoughtful feedback. Below, we respond to the weaknesses and questions raised, addressing each point individually.\n\n**Comment:** Even though deriving a relaxed condition on $\\gamma$ is a contribution, it is a result of Furnsinn and Postoyan rather than proposing a new concept.\n\n**Response:** While our work is inspired by Fürnsinn et al. and Postoyan et al., it introduces several novel elements beyond re-deriving existing results. \n\nIn comparison with Postoyan et al., in the linear system setting, we extend the classical Lyapunov condition for stability using a generalized Lyapunov function, which leads to a new multi-step LMI condition (Theorem 4.3). We show that this enables significantly tighter stability certification with respect to the discount factor $\\gamma$, improving upon the thresholds derived in Postoyan et al.\n\nIn comparison with Fürnsinn et al., we use a generalized Lyapunov function, parameterized as a neural network, to learn a stability certificate for a reinforcement learning problem, while Fürnsinn et al. use a given generalized Lyapunov function to prove recursive feasibility and stability results for MPC. Hence, while the concept of generalized Lyapunov function is the same, it is applied to different problems. The novelty of our approach is to augment an RL value function with a learnable residual neural network and enforce a multi-step decrease condition via a trainable step-weight network. Our insight about how to parameterize the generalized Lyapunov function candidate comes from analyzing the linear system case via the results from Postoyan et al. Our formulation allows certifying stability for RL policies where classical methods fail. \n\nFinally, we extend our approach to joint synthesis of neural controllers and certificates, and show that the multi-step Lyapunov formulation leads to larger certified regions of attraction compared to standard Lyapunov training. These results are novel and useful for enabling certifiable stability in learning-based control systems.\n\n**Comment:** The required method needs to know the equilibrium state (origin) to define Lyapunov function. In contrast to classical control, RL takes advantages when the equilibrium state is unknown.\n\n**Response:** We agree with the reviewer that requiring knowledge of the equilibrium state (or set) is a limitation of our approach compared to the flexibility of reinforcement learning. In many RL settings, the equilibrium is not known a priori but is instead implicitly defined by the reward function structure. In our work, we focus on systems where the equilibrium can be reasonably identified either analytically (e.g., physical systems with known stable configurations) or empirically (e.g., the final resting state of an RL policy). Extending the our approach to settings with unknown or non-isolated equilibria (e.g., limit cycles) is an interesting direction for future work. In such cases, one could consider replacing the fixed equilibrium assumption with data-driven or reward-inferred equilibria, or more generally, formulate stability notions relative to an invariant set or trajectory (e.g., using contraction theory).\n\nWe plan to add this discussion to the revised paper and will also note that exploring the relationship between the reward landscape and candidate equilibria presents a promising direction for future research.\n\n**Comment:** The experiments are quite limited to simple control problems, which follows from Weakness 2. \n\n**Response:** We agree with the reviewer that our experiments focus on benchmark control problems but we would like to emphasize that even these systems present significant challenges for stability certification. For example, in the inverted pendulum task with tight control constraints (e.g., $\\|u\\| < 2$), synthesizing a Lyapunov function that certifies stability over the entire state space is nontrivial. Classical Lyapunov-based methods typically fail in such settings and can only certify stability for a small region near the equilibrium, whereas our approach successfully certifies stability across the entire state space. Moreover, we also observe that policies derived directly from Lyapunov functions often fail to stabilize the system, e.g., get stuck due to the limited control.\n\nRegarding more complex systems (e.g., humanoid standing or walking), we have observed that many RL policies learned via standard methods (e.g., PPO, SAC, TD-MPC) do not exhibit global stability. As a result, stability certification using our method is not possible in these settings without modifying the policy. We have preliminary results where we \\emph{jointly optimize} the RL policy and the generalized Lyapunov certificate using our multi-step loss. These initial experiments show promising improvements in the size of the certifiable region of attraction, suggesting that our approach may enable stability guarantees even in higher-dimensional, more complex control tasks.\n\n**Question:** Remark 4.4 : The statement would benefit if it presents stronger result than feasibility other than that of classical Lyapunov problem. Can we guarantee a weaker version of feasibility?\n\n**Response:** We thank the reviewer for the insightful suggestion. We agree that Remark 4.4 can be strengthened to clarify the practical advantage of the multi-step (generalized) Lyapunov formulation. While we do not yet provide a formal theoretical guarantee of feasibility that extends beyond the classical Lyapunov condition, our formulation strictly generalizes the classical case and has been empirically shown to succeed in scenarios where the single-step (classical) Lyapunov condition fails.\n\nWe will expand Remark 4.4 in the revision to emphasize the following: the multi-step LMI condition can always be used to certify stability in all cases where the single-step LMI condition (7) is feasible, and can also succeed in additional cases where (7) is not feasible. For example, in the linear system of Example 3.3, the classical LMI condition only certifies stability for discount factors $\\gamma > 0.8090$, while the generalized LMI with $M = 2$ lowers this bound to $\\gamma > 0.6229$, and approaches the true threshold $\\gamma^\\star = 1/3$ as $M$ increases. This demonstrates that our generalized formulation can strictly enlarge the set of stabilizable systems, offering a strictly weaker sufficient condition for stability in practice.\n\nFormalizing this observation into a theoretical weaker notion of feasibility is an exciting direction for future work, and we thank the reviewer for pointing it out.\n\n**Question:** How did the authors choose $M=15$ or $M=20$ in the experiments?\n\n**Response:** We selected $M = 15$ or $M = 20$ empirically to balance computational cost and learning effectiveness. Larger $M$ improves flexibility in satisfying the generalized Lyapunov condition but increases the required rollout length and training time, while smaller $M$ can make learning a valid certificate more difficult. Optimizing the choice of $M$ for a given system is indeed an interesting direction, and we have noted this in the limitations and future work section.\n\n**Question:** What are the final values of $\\sigma_i(\\mathbf{x})$? Does the final values provide any further insights?\n\n**Response:** We observe that the learned weights $\\sigma_i(\\mathbf{x})$ tend to concentrate on the last few steps of the horizon. This suggests that the certificate relies more heavily on long-term decrease in the Lyapunov function, especially for states farther from the equilibrium where short-term behavior may be non-monotonic. For states near the equilibrium (i.e., where stability is easier to verify), the weights remain closer to the initialization. These patterns highlight how the weighting network adapts to the local difficulty of certifying stability and help explain the flexibility of our generalized condition. We will include a figure in the revised version that illustrates the distribution of weights for states near and far from the equilibrium across several systems."}, {"review_id": "7tOkUSRems", "reviewer": "Reviewer_c9c6", "summary": "This paper addresses the important issue of certifying stable control of deep reinforcement learning policies. It starts by showing that with a small modification, the value function can be used as a Lyapunov function. They then show that stable control can be certified with a relaxed form of the step-wise convergence property, which converges on average.", "questions": "- What do you mean by detectable in Assumption 3.1?\n- Could this method be extended to work with higher-dimensional control systems (e.g. Walker Stand)?", "limitations": "yes", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 4, "clarity": 4, "significance": 4, "originality": 4, "strengths_and_weaknesses": "Strengths\n- Overall, the paper is very clear and easy to follow.\n- The paper provides a detailed account of the problem statement and related work before introducing the new method.\n- The paper provides strong theoretical foundations for the proposed method\n\n\nWeaknesses\n- This paper only evaluates on a limited set of environments. \n- It would be good to see confidence intervals for the quantitative metrics in Table 2, as you are making comparisons between different finite horizons (M).\n- It would be good to see how your proposed method compares to alternative methods for stabilising stability.\n- It would be good to see the influence of the step weights rather than only using the weights selected via grid search.\n\n\nTypography errors\n- Can you include brackets for Equations 9, 14, and 18 so it is clear what is being summed over?\n- Currently, the Y labels in figures 4, 5 & 6 are displayed as “Theta_dot”, instead of “Theta Dot” or $\\dot{\\theta}$.", "was_revised": true, "final_justification": "The authors addressed the concerns I had regarding confidence intervals and the distribution of the step-weights. The previous score of 5 is appropriate in my opinion.", "rebuttal": "We sincerely thank the reviewer for their thoughtful and encouraging feedback. We appreciate the positive assessment of our paper’s clarity, theoretical contributions, and overall quality. Below, we address the reviewer’s comments and questions one by one, including the suggested improvements and clarifications.\n\n**Comment:** This paper only evaluates on a limited set of environments. \n\n**Response:** We agree with the reviewer and would like to clarify that many standard RL policies are not globally stable for complex systems (e.g., humanoid walking), making it difficult to certify stability without explicitly modeling a region of attraction or restricting initial states. This is why our Section 5 focuses on simpler environments where RL policies already succeed in stabilizing the system. For more complex tasks, our preliminary results suggest that jointly optimizing the policy and generalized Lyapunov certificate can enlarge the certifiable region. We view this as a promising direction for future research to improve the reliability and robustness of RL algorithms.\n\n**Comment:** It would be good to see confidence intervals for the quantitative metrics in Table 2, as you are making comparisons between different finite horizons (M).\n\n**Response:** We thank the reviewer for this helpful suggestion. To address this, we repeated each experiment 10 times and report the mean and standard deviation of the certified ROA volume and verification time in the following Table. These results confirm the robustness of our findings across different random seeds. We will include this updated table in the final version of the paper.\n\n**Certified ROA Volume (mean ± std over 5 runs):**\n\n| System             | M = 1         | M = 2         | M = 3         |\n|--------------------|---------------|---------------|---------------|\n| Inverted Pendulum  | 42.96 ± 1.27  | 76.74 ± 1.32  | 89.24 ± 1.24  |\n| Path Tracking      | 21.77 ± 0.56  | 23.56 ± 0.58  | 23.95 ± 0.53  |\n| 2D Quadrotor       | 103.52 ± 1.81 | 109.06 ± 1.97 | 113.72 ± 2.04 |\n\n**Verification Time (seconds):**\n\n| System             | M = 1          | M = 2           | M = 3           |\n|--------------------|----------------|------------------|------------------|\n| Inverted Pendulum  | 11.66 ± 0.45   | 21.52 ± 0.82     | 39.24 ± 1.31     |\n| Path Tracking      | 8.62 ± 0.51    | 19.47 ± 0.98     | 36.72 ± 1.26     |\n| 2D Quadrotor       | 2209.52 ± 72.6 | 3858.72 ± 112.4  | 5628.56 ± 185.9  |\n\n**Comment:** It would be good to see how your proposed method compares to alternative methods for stabilising stability.\n\n**Response:** We believe the reviewer intended to refer to certifying rather than stabilizing stability. We appreciate the suggestion and agree that comparisons to alternative certification methods are valuable. In our work, we include the most directly comparable baseline: the classical Lyapunov formulation, which corresponds to our method with $M = 1$. This baseline is evaluated in both the linear system analysis (Section 4) and joint synthesis experiments (Section 6). As shown in Table 2 and Figures 1, 2, 7, and 8, our generalized formulation with $M > 1$ consistently yields tighter lower bounds on $\\gamma$ and larger certified regions of attraction. These results demonstrate improved stability guarantees over the classical (neural) Lyapunov function approach.\n\nWhile other methods ([1]) for certifying stability (e.g., polynomial Lyapunov functions or sum-of-squares techniques) exist, they typically assume access to analytical system models and are not directly applicable in the learning-based settings we study. We will clarify this point in the revised manuscript.\n\nReferences: \n[1] Papachristodoulou, Antonis, and Stephen Prajna. \"On the construction of Lyapunov functions using the sum of squares decomposition.\" Proceedings of the 41st IEEE Conference on Decision and Control, 2002.. Vol. 3. IEEE, 2002.\n\n**Comment:** It would be good to see the influence of the step weights rather than only using the weights selected via grid search. \n\n**Response:** Thank you for the suggestion. In Section 5, the step weights are modeled by a neural network and jointly optimized with the certificate function. We observe that the network adapts the weights based on the difficulty of certifying stability at each state, often concentrating more weight on later steps for harder regions. In Section 6, we fix the weights and perform grid search to select effective configurations. This design choice is made to ensure compatibility with formal verification tools [2].\n\nReferences: \n[2] Wang, Shiqi, et al. \"Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification.\" Advances in neural information processing systems 34 (2021): 29909-29921.\n\n**Comment:** Typography errors. \n\n**Response:** We thank the reviewer for pointing out these typos and formatting issues. We will revise the equations for clarity and update the figure labels in the final version.\n\n**Question:** What do you mean by detectable in Assumption 3.1? \n\n**Response:** Thank you for the question. In control theory, a pair $(\\mathbf{A}, \\mathbf{C})$ is observable if the full system state can be inferred from output measurements over time. Detectability is a weaker condition: it requires that any unobservable mode of $\\mathbf{A}$ is stable, meaning that all eigenvalues $\\lambda$ with $|\\lambda| \\geq 1$ are observable through $\\mathbf{C}$. In our context, this condition guarantees that a valid Lyapunov function can be constructed for the closed-loop system. See, for example, Section 6.3 in [3] for a formal definition and further discussion.\n\nReferences: \n[3] Khalil, Hassan K., and Jessy W. Grizzle. Nonlinear systems. Vol. 3. Upper Saddle River, NJ: Prentice hall, 2002.\n\n**Question:** Could this method be extended to work with higher-dimensional control systems (e.g. Walker Stand)?\n\n**Response:** We refer the reviewer to our response to the first comment. We believe our approach can be extended to higher-dimensional systems; while obtaining formal stability certificates may be more challenging in such cases, the framework can still be used to improve robustness or expand the certifiable region of attraction. Preliminary results suggest that jointly optimizing the policy and the generalized Lyapunov certificate is effective in this setting. We view this as a promising direction for future research to enhance the reliability of RL algorithms in complex control tasks."}, {"review_id": "N4A9XlsQpI", "reviewer": "Reviewer_9j8F", "summary": "This paper develops generalized Lyapunov certificates for verifying stability of reinforcement learning policies. The generalized Lyapunov functions are constructed by augmenting the value function with a neural residual correction term. The method is shown to successfully verify stability of RL policies on Gymnasium and DeepMind control benchmarks.", "questions": "I do not have any additional questions.", "limitations": "Yes.", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 4, "significance": 3, "originality": 4, "strengths_and_weaknesses": "Strengths:\n1. Certifying stability of RL policies is an important consideration the RL community has ignored for a long time. In this regard, the authors make a strong and timely contribution.\n2. The authors invoke two clever insights in the development: i) use of generalized Lyapunov condition which requires a Lyapunov decrease only on an average over multiple timesteps instead of a single step, ii) using neural residual error correction term in addition to the value function. These insights solve the difficult problem of certifying stability of RL policies.\n3. The writing is engaging to the reader. The intuition discussing stability of LQR controller with discounted cost provides a strong motivation for their approach.\n\nWeaknesses:\n1. The Lyapunov certificates lack guarantees on robustness to small (bounded) perturbations. For typical RL controllers, robustness to disturbances is a bigger concern that just the stability of the policy. Modifying the generalized Lyapunov condition to account for bounded perturbations and proving stability of a corresponding neighborhood of the origin would make the result stronger. \n2. The discrete-time system in (1) does not account of stochastic effects, e.g., as in Markov processes typically considered in RL problems. Extending the approach to stochastic systems by developing stochastic Lyapunov certificates would make the contribution stronger.\n\nHowever, the strengths far outweigh the weaknesses in my opinion.", "was_revised": true, "final_justification": "The paper is acceptable and the previous score of 5 is appropriate in my opinion", "rebuttal": "Thank you for the thoughtful and encouraging feedback. We appreciate your recognition of the key ideas and contributions. Below, we address the two main suggestions regarding robustness and stochasticity, and we will highlight both as important directions for future work in the revised manuscript.\n\n**Comment:** The Lyapunov certificates lack guarantees on robustness to small (bounded) perturbations. For typical RL controllers, robustness to disturbances is a bigger concern that just the stability of the policy. Modifying the generalized Lyapunov condition to account for bounded perturbations and proving stability of a corresponding neighborhood of the origin would make the result stronger.\n\n**Response:** We thank the reviewer for the insightful suggestion. We agree that robustness to bounded perturbations is important, especially in the context of RL policies. While our current formulation focuses on stability for deterministic systems, we believe that incorporating robustness into the generalized Lyapunov condition is a promising direction and, in fact, our approach is very conducive to doing so. For instance, one could introduce additive perturbation terms in the dynamics and adapt the decrease condition to hold over a disturbance set, similar in spirit to robust Lyapunov or input-to-state stability (ISS) frameworks. Extending our method to certify robust stability under such perturbations is a compelling direction for future work.\n\nWe will point out this opportunity explicitly in the revised version of the paper to help guide future extensions.\n\n**Comment:** The discrete-time system in (1) does not account of stochastic effects, e.g., as in Markov processes typically considered in RL problems. Extending the approach to stochastic systems by developing stochastic Lyapunov certificates would make the contribution stronger.\n\n**Response:** We thank the reviewer for the valuable suggestion. We agree that extending the approach to stochastic systems is an important direction, especially given the prevalence of Markov decision processes in RL. While our current formulation focuses on deterministic systems, the generalized Lyapunov framework can be adapted to the stochastic setting by requiring the decrease condition to hold in expectation or under suitable risk measures, as in stochastic Lyapunov or risk-sensitive stability formulations. We will highlight this possible extension explicitly in the revised version of the paper to clarify the scope of our current results and guide future work."}, {"review_id": "o2jTNZ41n5", "reviewer": "Reviewer_Ubo7", "summary": "This paper propose a method to cetificate the stability of a RL policy by learning a Lyaponv value function based on the value function of RL policy and a resudual network. It also introduce a generalized multi-step fomulation of the lyanapov condition to extend the bound of the disounted factor which guarantees the stability. The paper provides comprehensive mathmatical proof of the proposed theorms and the examples to illustrate the performance of the proposed theory.", "questions": "The questions are essentially the same as those listed in the Weaknesses section.", "limitations": "yes", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 4, "clarity": 4, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strengths:\n\n1. The paper addresses the important problem of bridging the stability guarantees of Lyapunov functions with value functions in RL, helping clarify the gap between provably stable control methods and learning-based approaches.\n\n2. It provides a concrete example by extending the analysis to the LQR setting, illustrating the necessity of the proposed generalized Lyapunov function.\n\n3. The paper presents a complete pipeline to incorporate the generalized Lyapunov function into the RL framework, including the formulation of a loss function and a thorough analysis of experimental results.\n\nWeaknesses:\n\n1. The proposed method is parameterized by M and corresponding weights. It would be helpful to analyze how the grid search range for these weights affects the results. In particular, since there is no explicit upper bound on the sum of weights (which is set equal to M in the experiments), further explanation of this choice is needed.\n\n2. The generalized Lyapunov function allows the value to temporarily increase over short horizons. Is there any theoretical bound on this temporary increase? As M grows, such increases may become more significant—does this affect convergence speed or stability?\n\n3. In the RL application, is the policy trained with a fixed discount factor λ? If so, how do the authors ensure that the resulting policy satisfies the certification condition under that λ? In other words, how can we guarantee that the chosen λ lies within the bounds established by the proposed method?", "was_revised": true, "final_justification": "I recommend keeping the original score of 5. The rebuttal addressed most of my concerns:\nWeight Parameterization: The authors clarified the rationale for setting the total weight sum to M, which improves optimization stability. While an empirical analysis of this choice would still be helpful, this issue is largely resolved.\nTemporary Lyapunov Increases: The response points to Theorem 6.2 for bounding temporary increases, which addresses my theoretical concern. More explicit guidance in the paper would strengthen the presentation.\nDiscount Factor in RL: The authors provided a clear distinction between the linear and RL settings and acknowledged the limitations of post hoc certification. Their mention of joint policy-certificate optimization is promising.\n\nOverall, the clarifications are sufficient, and the paper makes a meaningful contribution. Some open questions remain, but they do not significantly detract from the main contributions.", "rebuttal": "We thank the reviewer for their positive and constructive feedback. We appreciate the recognition of our efforts to bridge Lyapunov stability and reinforcement learning, as well as the clarity and completeness of our proposed framework. Below, we address the reviewer’s questions regarding weight selection, temporary increases in the Lyapunov value, and the role of the discount factor in the RL experiments. These clarifications will be incorporated into the revised manuscript.\n\n**Comment:** The proposed method is parameterized by M and corresponding weights. It would be helpful to analyze how the grid search range for these weights affects the results. In particular, since there is no explicit upper bound on the sum of weights (which is set equal to M in the experiments), further explanation of this choice is needed.\n\n**Response:** We thank the reviewer for the thoughtful comment. While the theoretical condition only requires $\\sum_{i=1}^M \\sigma_i(\\mathbf{x}) \\geq M$, enforcing $\\sum \\sigma_i = M$ makes the generalized Lyapunov condition less conservative and easier to satisfy, as increasing the total weight effectively tightens the decrease constraint. We adopt  $\\sum \\sigma_i = M$ in both Section 5 (learned weights via neural networks) and Section 6 (fixed weights via grid search) for consistency, interpretability, and stable optimization. We will clarify this design choice explicitly in the revised version of the paper to aid reader understanding.\n\nEmpirically, we observe that different weight combinations under this constraint lead to different certified ROAs (see Figures 1, 2, and Table 2). In Section 5, the learned weights often concentrate on the final few steps of the rollout horizon, especially for states farther from the equilibrium, indicating that the certificate relies more on long-term decrease. \n\n**Comment:** The generalized Lyapunov function allows the value to temporarily increase over short horizons. Is there any theoretical bound on this temporary increase? As M grows, such increases may become more significant—does this affect convergence speed or stability?\n\n**Response:** We thank the reviewer for the insightful question. While our formulation does not impose an explicit bound on temporary increases in the Lyapunov function, overall convergence is still guaranteed as long as the weighted average over $M$ steps decreases. Theoretically, increasing $M$ provides greater flexibility in handling non-monotonic dynamics, but may slow down convergence. Importantly, this does not affect the stability guarantee.\n\nFurthermore, if all weights are lower bounded by some $\\underline{\\sigma} > 0$, then temporary increases can be bounded explicitly, as discussed in Theorem 6.2.\n\n**Comment:** In the RL application, is the policy trained with a fixed discount factor λ? If so, how do the authors ensure that the resulting policy satisfies the certification condition under that λ? In other words, how can we guarantee that the chosen λ lies within the bounds established by the proposed method?\n\n**Response:** We thank the reviewer for the thoughtful question. In the linear system setting (Section 4), where the value function and policy are known exactly, we can explicitly analyze the range of discount factors $\\gamma$ (in the terminology of the reviewer, $\\lambda$) for which a generalized Lyapunov function can be constructed. In particular, we derive tight lower bounds on $\\gamma$ under which stability is certifiable.\n\nIn contrast, in the RL setting (Section 5), the value function and policy are learned and approximate. As a result, we do not have an explicit bound on $\\gamma$, though in practice RL algorithms typically use large values (e.g., $\\gamma = 0.99$). Instead, we attempt to construct a generalized Lyapunov function for the given closed-loop behavior. Certification may fail if the learned policy is not stabilizing, which we have observed empirically for more complex tasks such as humanoid walk.\n\nTo address this, we conduct preliminary simulations that jointly optimize the RL policy and the generalized Lyapunov certificate, and observe that this improves stability and the size of the certifiable region. We view this as a promising direction for future work."}, {"review_id": "c3xIQYhHtI", "reviewer": "Reviewer_A5kt", "summary": "This paper proposes a less conservative formulation for certifying stability in learning enabled systems. Traditionally, existence of a Lyapunov function is functional proof of stability. Conditions of a Lyapunov function can be conservative in certain systems, it requires strict decrease w.r.t evolution of the system. Authors relax this condition by allowing increase in the value, but the value should decrease over a horizon.", "questions": "See weaknesses.", "limitations": "Contribution seems quite incremental, especially compared to the work mentioned in the weaknesses. \nI am not quite sure how this method scales with higher dimensional systems, since it is model-based, I expect more complicated systems. I also suspect this method does not scale well with number of layers and neurons of the controller.", "rating": 2, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 3, "significance": 2, "originality": 1, "strengths_and_weaknesses": "Strengths: \n\n1-Authors provide a less conservative condition for Lyapunov function, which in my experience, helps when you have multiple integrators in a system.\n\n2-Overall, paper is well written and easy to follow. \n\nWeaknesses:\n\n1- Though authors provide a new formulation for Lyapunov function, this idea is not novel, and has been studied extensively in barrier certificates and software verification. I believe following work deserve citation:\n\nk-Inductive Barrier Certificates for Stochastic Systems, HSCC 2022.\n\nt-Barrier Certificates: A Continuous Analogy to k-Induction, ADHS 2018.\n\nAutomatic synthesis of k-inductive piecewise quadratic invariants for switched affine control programs, CLSS 2017.\n\nSafety Verification and Refutation by k-invariants and k-induction, SAS 2015.\n\nSoftware Verification Using k-Induction, SAS 2011.\n\nI believe if authors frame this problem in a k-inductive manner, it would strengthen the paper.\n\n2- Experiments are not convincing. I do understand that methods that provide formal guarantee do not scale well, however I believe authors could have done a better job at selling their method by providing more experiments. Furthermore, there is no comparison with state-of-the-art methods, such as Yang et al (which this work is heavily inspired by), or other model-based methods (since the verification part requires exact mathematical model of the system). There are works that provide formal guarantee using Lipschitz continuity that have more complicated experiments, and they do not require mathematical model of the system. \n\n3- Contribution seems incremental compared to Yang et al.\n\n4- Bulk of mathematical vigor of the paper is borrowed from previous work, and I am not sure if the proof for Theorem 6.2 is correct (which is the main theoretical contribution of the paper). How does equation 56 imply 62? Moreover, the claim in line 532 by authors does not guarantee ``progress\" towards origin. If the increase is substantially more than decrease, then you cannot say you are making progress towards origin (hence I suggested to use k-induction formulation). \n\n5- There is not discussion on how does verification scale with respect to number of layers or neurons, controllers in the paper are relatively simple (since systems are low-dimensional or simple).", "was_revised": true, "final_justification": "This work seems incremental compared to traditional k-induction, therefore I believe strong empirical results on high dimensional systems is warranted.", "rebuttal": "We thank the reviewer for their time and feedback. Below, we address each weakness and question in turn.\n\n**Weakness 1 Response:** \n\nWe thank the reviewer for highlighting the connection to k-inductive verification. We agree that this connection strengthens the paper and appreciate the citation. That said, we would like to clarify that our generalized Lyapunov condition is distinct from the standard k-inductive formulation. Specifically, k-induction requires a strict decrease at the final step t+k, while allowing bounded increases at intermediate steps. In contrast, our formulation enforces a decrease in a weighted average over multiple future steps, allowing more flexible trajectories. Additionally, the step weights in our formulation can be learned or tuned, enabling more expressive certificates.\n\nTo improve clarity and better situate our contribution, we will revise the manuscript:\n\n1. We will add a paragraph on k-inductive certificates, citing both the papers recommended by the reviewer and additional relevant works [1-6]. This will place our contribution in context and make the relation to k-induction explicit.\n\n 2. After Definition 3.2, we will clarify how our generalized Lyapunov condition can be interpreted through the lens of k-inductive verification. For example, by choosing weights $\\sigma_1 = \\cdots = \\sigma_{k-1} = 0$ and $\\sigma_k = M$ in the inequality $\\sum_{i=1}^k \\sigma_i \\cdot \\left(V(x_{t+i}) - V(x_t)\\right) \\leq -\\alpha V(x_t)$, we obtain the condition $V(x_{t+k}) \\leq (1 - \\alpha) V(x_t)$, analogous to a k-step Lyapunov decrease condition. This shows that our approach may be formulated from the perspective of k-inductive verification by defining the decrease condition over a fixed horizon k. While k-inductive approaches typically require a strict decrease at the final step and allow bounded increases at intermediate steps, our formulation instead enforces a decrease on a weighted average across multiple future steps. This allows greater flexibility, as the weights can be optimized during training rather than fixed in advance. We believe this distinction is important and will clarify it in the revised manuscript.\n\n3. We note that existing k-inductive certificates have been used to certify safety or invariance properties, whereas our work may enable certification of stability or convergence. Our formulation allows temporary increases in $V$, yet enforces an overall decrease over a finite horizon, enabling the certification of asymptotic stability when single-step tests fail. \n\nReferences:\n \n[1] \"Learning k-inductive control barrier certificates for unknown nonlinear dynamics beyond polynomials.\" \n\n[2] \"Automatic synthesis of k-inductive piecewise quadratic invariants for switched affine control programs.\" \n\n[3] \"K-inductive barrier certificates for stochastic systems.\" \n\n[4] \"t-Barrier certificates: a continuous analogy to k-induction.\" \n\n[5] \"Safety verification and refutation by k-invariants and k-induction.\" \n\n[6] \"Restructuring dynamical systems for inductive verification.\" \n\n**Weakness 2 Response:**\n\nWe thank the reviewer for the constructive feedback. We would like to clarify that we compare against Yang et al., which corresponds to the classical Lyapunov formulation. This comparison is presented in Section 6, Table 2, and Figures 7 and 8. The method of Yang et al. is equivalent to our formulation with $M = 1$. As shown in the results, our generalized formulation with $M > 1$ consistently outperforms this baseline by certifying larger regions of attraction. We also conducted simulations on a 2D quadrotor system with 6 state variables. \n\nRegarding Section 5, we focus on benchmark control tasks such as the pendulum and cart-pole. While simple, these environments pose challenges for stability certification due to control limits. These difficulties have been documented in prior work [7,8]. Our method successfully certifies stability in such constrained regimes. Moreover, in these RL environments (e.g., Gym, DM Control), we do not require access to system dynamics, as our approach operates directly from trajectory rollouts.\n\nFinally, for higher-dimensional systems, many RL policies are not inherently stable across the entire state space, limiting the ability to construct valid stability certificates. To address this, we have begun exploring a joint optimization of the RL policy and the generalized Lyapunov certificate using our multi-step loss. We have preliminary results that show promising improvements in the size of the region of attraction, suggesting that our approach may enable stability guarantees even in higher-dimensional control tasks. \n\nIn the revision, we will clarify the distinctions between our method and [7], explicitly highlight the benefits of our approach under control constraints, and emphasize that it can operate in a model-free setting. We will also include a brief discussion of our joint optimization results and their implications for extending the method to higher-dimensional systems.\n\nReferences:\n\n[7] \"Lyapunov-stable neural control for state and output feedback: A novel formulation.\" \n\n[8] \"Distributionally robust policy and Lyapunov-certificate learning.\" \n\n**Weakness 3 Response:** \n\nWe thank the reviewer for the comment. While our synthesis experiments in Section 6 are inspired by [7], our paper introduces several key advances that go beyond their method. We respectfully disagree with the assessment that our theoretical contributions are incremental. Our contributions include the following.\n\n1. A generalized multi-step Lyapunov formulation that extends beyond the classical one-step condition used in prior work. This allows us to certify and train neural network policies that are not admissible under classical Lyapunov conditions.\n    \n2. Theoretical analysis in the linear system setting that establishes a novel connection between stability and optimality. Theorem 4.3 introduces new multi-step linear matrix inequality conditions for verifying stability of linear systems under optimal policies obtained by minimizing quadratic cost functions. Both the statement and the proof of this result are novel and form a foundational component of our result, which we subsequently extend to nonlinear systems in later sections.\n    \n3. Practical improvements in the size of certifiable regions and the conservativeness of the stability certificate. Our experiments demonstrate consistent gains over the baseline method in different baseline systems.\n\nWe will revise the manuscript to clearly articulate these distinctions and to highlight the novelty of our approach.\n\n**Weakness 4 Response:**\n\nWe thank the reviewer for the feedback on the proof of Theorem 6.2. In response, we rewrote the proof using the standard $\\varepsilon$-$\\delta$ style to show how the generalized decrease condition leads to Lyapunov stability.\n\n**Revised proof:**\nLet $\\varepsilon > 0$ be arbitrary. Define $\nm_\\varepsilon := \\min_{||x|| = \\varepsilon} V(x)$, which is strictly positive due to the positive-definiteness of $V$ and continuity over the compact $\\epsilon$-sphere. Let $c := \\frac{2(1 - \\bar{\\alpha})}{\\underline{\\sigma}} > 0$. Since $V(0) = 0$ and $V$ is continuous, for every threshold $\\eta>0$ there exists a radius $\\delta(\\eta)>0$ such that $||x||<\\delta(\\eta) \\Longrightarrow V(x)<\\eta.$\n\nChoose $\\eta:=m_\\varepsilon/c$ and set $\\delta:=\\delta(m_\\varepsilon/c)$ gives\n\n$$||x||<\\delta \\Longrightarrow V(x)<\\frac{m_\\varepsilon}{c}.$$ Now pick any index $k$ with $x_k\\in\\mathcal S$ and $\\|x_k\\|<\\delta$, we have $V(x_k) < \\frac{m_\\varepsilon}{c}$.\n\nBy the generalized two-step Lyapunov condition and $\\sigma_1, \\sigma_2 \\ge \\underline{\\sigma}$: $\\underline{\\sigma}(V(x_{k+1}) + V(x_{k+2})) \\le 2(1 - \\bar{\\alpha}) V(x_k)$. So $\nV(x_{k+i}) < c \\cdot V(x_k) < m_\\varepsilon, \\text{for } i = 1, 2$.\n\nSince $V(x) < m_\\epsilon$ implies $||x|| < \\varepsilon$, we conclude $\n||x_{k+1}||, ||x_{k+2}|| < \\varepsilon$. This shows that the trajectory remains within the $\\varepsilon$-ball if it starts within a $\\delta$-ball. \n\nMoreover, by the generalized decrease condition, it is not possible for both $V(x_{k+1}) \\ge V(x_k)$ and $V(x_{k+2}) \\ge V(x_k)$ to hold simultaneously. Therefore, at least one of the two states must satisfy $\nV(x_{k+i}) < V(x_k) \\text{for some } i \\in \\{1, 2\\}$, which guarantees that the trajectory enters a strictly smaller sublevel set of $V$ within two steps. This allows the generalized Lyapunov condition to be applied recursively, ensuring asymptotic convergence to the origin.\n\n**Weakness 5 Response:** \n\nWe agree that scaling to higher‑dimensional systems is an essential research direction. Verification complexity grows with (i) the dimension of the state space, (ii) the size and depth of the neural network, and (iii) the functional form of the Lyapunov candidate. In the present work we rely on the $\\alpha$-$\\beta$-CROWN verifier, which combines linear bound propagation with branch‑and‑bound search to give complete and certified guarantees for neural networks. However, as also reported by Yang et al., its run‑time grows rapidly beyond $6$ state variables or networks exceeding a few thousand hidden units.\n\n**Limitations Response:** \n\nIn the revised manuscript, we will make the following changes.\n\n1. We will explicitly highlight the theoretical and empirical differences between our method and prior work, particularly Yang et al., including our generalized multi-step condition, the connection to value functions, and the ability to certify neural policies learned via reinforcement learning.\n    \n2. We will cite recent work on k-inductive literature and discuss how our generalized Lyapunov condition can be interpreted as a k-inductive property while clarifying the differences. \n    \n3. We will rewrite the proof of Theorem 6.2 in the standard $\\varepsilon$-$\\delta$ style to improve clarity.\n  \n4. We will add a discussion on scalability and outline potential directions to improve scalability in future work."}]

Author rebuttal:

Meta-review: The paper extends a previous framework for stability analysis of discounted optimal control problems to the case where the Lyapunov function is allowed to temporarily increase but must decrease on average across N  steps. Furthermore, the authors propose a way to learn an augmentation term that certifies stability in addition to the value function, and show how this can be used to certify stability in some problems.

Reviews are mixed. Reviewers recognize the usefulness of the framework and (after discussion) the empirical strengths of the paper. There are some ways to generalize (like robust stability, stochastic systems) that the authors convincingly motivate that they will address in future work. The math is judged as a little incremental since it combines Postoyan and Furnsinn, but remains useful and there is methodological innovation independent from this in learning the neural residual correction to certify stability of RL policies.

The main point of contention is on the relation to k-induction (A5kt). In my view, the Lyapunov phrasing of the problem is different enough and remains useful as long as the authors make an effort to relate their work properly to k-induction (which they seem to do in good faith given their response, even though they did seem to not be aware of the literature initially). Irrespective from this, there is still the methodological contribution of learning the neural residual correction, which the reviewer does not really weigh heavily in their review but is a significant part of the paper.

Overall, I think the positives outweigh the negatives for this paper and recommend acceptance.
Decision: Accept (poster)