Certifying Stability of Reinforcement Learning Policies using Generalized Lyapunov Functions

We thank the reviewer for their time and feedback. Below, we address each weakness and question in turn.

Weakness 1 Response:

We 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.

To improve clarity and better situate our contribution, we will revise the manuscript:

1. 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.

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.

3. 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.

References:

[1] "Learning k-inductive control barrier certificates for unknown nonlinear dynamics beyond polynomials."

[2] "Automatic synthesis of k-inductive piecewise quadratic invariants for switched affine control programs."

[3] "K-inductive barrier certificates for stochastic systems."

[4] "t-Barrier certificates: a continuous analogy to k-induction."

[5] "Safety verification and refutation by k-invariants and k-induction."

[6] "Restructuring dynamical systems for inductive verification."

Weakness 2 Response:

We 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.

Regarding 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.

Finally, 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.

In 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.

References:

[7] "Lyapunov-stable neural control for state and output feedback: A novel formulation."

[8] "Distributionally robust policy and Lyapunov-certificate learning."

Weakness 3 Response:

We 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.

1. 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.

2. 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.

3. 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.

We will revise the manuscript to clearly articulate these distinctions and to highlight the novelty of our approach.

Weakness 4 Response:

We 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.

Revised proof: Let $\varepsilon > 0$ be arbitrary. Define $m_\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.$

Choose $\eta:=m_\varepsilon/c$ and set $\delta:=\delta(m_\varepsilon/c)$ gives

$||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}$.

By 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 $V(x_{k+i}) < c \cdot V(x_k) < m_\varepsilon, \text{for } i = 1, 2$.

Since $V(x) < m_\epsilon$ implies $||x|| < \varepsilon$, we conclude $||x_{k+1}||, ||x_{k+2}|| < \varepsilon$. This shows that the trajectory remains within the $\varepsilon$-ball if it starts within a $\delta$-ball.

Moreover, 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 $V(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.

Weakness 5 Response:

We 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.

Limitations Response:

In the revised manuscript, we will make the following changes.

1. 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.

2. 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.

3. We will rewrite the proof of Theorem 6.2 in the standard $\varepsilon$-$\delta$ style to improve clarity.

4. We will add a discussion on scalability and outline potential directions to improve scalability in future work.

Authors have made a genuinely effort to address my comments, and I appreciate that. To me, it looks like an incremental work compared to k-induction, thus, it requires significantly better empirical evaluation.

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.

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.

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.

Empirically, 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.

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?

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.

Furthermore, if all weights are lower bounded by some $\underline{\sigma} > 0$, then temporary increases can be bounded explicitly, as discussed in Theorem 6.2.

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?

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.

In 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.

To 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.

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.

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.

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.

We will point out this opportunity explicitly in the revised version of the paper to help guide future extensions.

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.

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.

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.

Comment: This paper only evaluates on a limited set of environments.

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.

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).

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.

Certified ROA Volume (mean ± std over 5 runs):

Verification Time (seconds):

Comment: It would be good to see how your proposed method compares to alternative methods for stabilising stability.

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.

While 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.

References: [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.

Comment: It would be good to see the influence of the step weights rather than only using the weights selected via grid search.

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].

References: [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.

Comment: Typography errors.

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.

Question: What do you mean by detectable in Assumption 3.1?

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.

References: [3] Khalil, Hassan K., and Jessy W. Grizzle. Nonlinear systems. Vol. 3. Upper Saddle River, NJ: Prentice hall, 2002.

Question: Could this method be extended to work with higher-dimensional control systems (e.g. Walker Stand)?

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.

We thank the reviewer for their time and thoughtful feedback. Below, we respond to the weaknesses and questions raised, addressing each point individually.

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.

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.

In 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.

In 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.

Finally, 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.

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.

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).

We 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.

Comment: The experiments are quite limited to simple control problems, which follows from Weakness 2.

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.

Regarding 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 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.

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?

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.

We 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.

Formalizing 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.

Question: How did the authors choose $M=15$ or $M=20$ in the experiments?

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.

Question: What are the final values of $\sigma_i(\mathbf{x})$? Does the final values provide any further insights?

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.