While ensuring stability for linear systems is well understood, it remains a major challenge for nonlinear systems. A general approach in such cases is to compute a combination of a Lyapunov function and an associated control policy. However, finding Lyapunov functions for general nonlinear systems is a challenging task. To address this challenge, several methods have been proposed that represent Lyapunov functions using neural networks. However, such approaches either focus on continuous-time systems, or highly restricted classes of nonlinear dynamics. We propose the first approach for learning neural Lyapunov control in a broad class of discrete-time systems. Three key ingredients enable us to effectively learn provably stable control policies. The first is a novel mixed-integer linear programming approach for verifying the discrete-time Lyapunov stability conditions, leveraging the particular structure of these conditions. The second is a novel approach for computing verified sublevel sets. The third is a heuristic gradient-based method for quickly finding counterexamples to significantly speed up Lyapunov function learning. Our experiments on four standard benchmarks demonstrate that our approach significantly outperforms state-of-the-art baselines. For example, on the path tracking benchmark, we outperform recent neural Lyapunov control baselines by an order of magnitude in both running time and the size of the region of attraction, and on two of the four benchmarks (cartpole and PVTOL), ours is the first automated approach to return a provably stable controller. Our code is available at: https://github.com/jlwu002/nlc_discrete.
Paper
Similar papers
Peer review
Summary
The paper proposes a Lyapunov control method for discrete-time systems, in contrast to previous approaches targeted at continuous-time systems. The paper proposes a mixed-integer linear programming approach for verifying stability conditions in discrete-time systems, a technique for computing sub-level sets which define the region of attraction, and a heuristic gradient-based approach for finding counterexamples that can accelerate the learning of Lyapunov functions.
Strengths
I appreciate the counterexample generation method proposed in this work. It leverages the key ideas in adversarial training in the computer vision domain to use gradients to accelerate the discovery of counterexamples.
Weaknesses
- The Heuristic Counterexample Generation cannot guarantee all counterexamples are found. It relies on sampling in the state space, but sampling, the method itself, cannot exhaust the state space. Therefore, the verification is more like an empirical evaluation. I am not saying being “empirical” is not good, but it just simply does not match the verification objective which should be very strict. - The authors did not explain if it is truly challenging to train in discrete time system compared to training in continuos time system. In fact, the continuous time system and discrete time system can share the same framework in training. See https://arxiv.org/pdf/2101.05436.pdf how they computed dot{h} in the paragraph below (7). - I would like to discuss with the authors if verification is truly necessary in Learning for Control. As we know, real-world dynamics are much more complex than the dynamics in the neural Lyapunov studies. The verification methods presented in these papers are very difficult to be applied to the real world and make real impacts. Often, a method that pursues excellent empirical performance instead of 100% rigorous verification will be closer to real-world scenarios in control (other domains such as planning or chip design might be different).
Questions
See weaknesses.
Rating
6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.
Confidence
5: You are absolutely certain about your assessment. You are very familiar with the related work and checked the math/other details carefully.
Soundness
3 good
Presentation
3 good
Contribution
2 fair
Limitations
See weaknesses.
Summary
The stability of nonlinear systems has long been a challenge in the field of control systems, with current methodologies employing Lyapunov stability theory to derive control policies. However, finding suitable Lyapunov functions for these systems is notably complex. To address this, researchers have started using neural networks to approximate Lyapunov functions, though primarily for continuous-time systems. The paper introduces a first-of-its-kind approach for learning neural Lyapunov control in discrete-time systems. This approach has three critical components:A unique mixed-integer linear programming method to verify stability conditions.A new method for computing sub-level sets to identify the region of attraction.A heuristic gradient-based method to rapidly find counterexamples, which improves the learning process of Lyapunov functions.Experimental results show a significant improvement over current techniques, outperforming neural Lyapunov control baselines by an order of magnitude in both running time and the size of the region of attraction. For the 'cartpole' and 'PVTOL' benchmarks, this is the first automated method to yield a provably stable controller.
Strengths
This method outperform recent neural Lyapunov control baselines by an order of magnitude in both running time and the size of the region of attraction.
Weaknesses
The loss function is then a weighted sum of several terms, which is hard to balance.
Questions
How does your method compare in terms of advantages to similar works like "Reinforcement Learning Control of Constrained Dynamic Systems with Uniformly Ultimate Boundedness Stability Guarantee" by Han M, Tian Y, Zhang L, et al. (Automatica, 2021, 129: 109689)?
Rating
5: Borderline accept: Technically solid paper where reasons to accept outweigh reasons to reject, e.g., limited evaluation. Please use sparingly.
Confidence
3: You are fairly confident in your assessment. It is possible that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work. Math/other details were not carefully checked.
Soundness
3 good
Presentation
3 good
Contribution
2 fair
Limitations
This method leverages a mixed-integer linear programming approach, which is known to be NP- hard.
Summary
This paper extends the neural Lyapunov control method to the discrete-time dynamical systems and propose two tricks to quickly find the counterexamples to accelerate the training process. The proposed method is tested in several standard tasks with comparison to the SOTA methods.
Strengths
[1] The proposed mixed-integer LP and PGD method can efficiently find the counterexamples in the training process. [2] The proposed method can find the largest ROA compared to the existing methods.
Weaknesses
[1] The extension of neural Lyapunov control from continuous-time dynamical systems to discrete-time dynamical systems has little contribution to the existing neural control community because the Lyapunov theories for continuous/discrete system are essentially the same. [2] The current method has huge computational cost for the case where the high-dimensional tasks are taken into account. [3] Lemma 3.1 is NOT mathematically correct.
Questions
[1] Does the proposed method scale to the high-dimensional systems such as controlling the molecular dynamics? [2] The neural Lyapunov method for unknown system (UNL) focuses on the realistic model-free settings, while the proposed method relies on the fully known dynamics, is the comparison in terms of size of ROA fair? [3] The problematic Lemma 3.1 cannot guarantee the soundness of the proposed method.
Rating
2: Strong Reject: For instance, a paper with major technical flaws, and/or poor evaluation, limited impact, poor reproducibility and mostly unaddressed ethical considerations.
Confidence
5: You are absolutely certain about your assessment. You are very familiar with the related work and checked the math/other details carefully.
Soundness
1 poor
Presentation
2 fair
Contribution
1 poor
Limitations
The authors only test the proposed method in toy models; however, they do not show the current method can be applicable in the real-world scenarios.
Summary
This paper studies learning stabilizing controllers with neural Lyapunov functions in discrete-time nonlinear systems. Previous works on neural Lyapunov control focused on continuous-time systems, and this is the first work that studies discrete-time systems. The outline of the proposed approach is similar with prior works on continuous-time systems, while the authors propose several key novel techniques for each step: They only use ReLU activations in the neural Lyapunov functions so that the constraints can be verified by mixed-integer programming. The authors also proposed a heuristic way to generate counterexamples efficiently via projected gradient descent. The simulation results show that the proposed method can find larger ROA and be implemented efficiently in several examples.
Strengths
Learning neural Lyapunov control in discrete-time systems is important for many applications. This work proposes many novel techniques to handle the difficulties that have been found in prior works. The simulation results are promising.
Weaknesses
I have some minor concerns about the presentation. After reading this paper, it is not clear to me which challenges are specific to the discrete-time system. In the first part of verifying Lyapunov constraints, the authors take the motivation from SMT solvers. However, this is also a challenge for neural Lyapunov control in continuous-time systems. I hope the authors can add a discussion about what efforts have been made to improve efficiencies in the continuous-time systems and why we cannot directly apply them here. And for the proposed ReLU network plus mixed-integer programming, does this method also apply to continuous-time systems? Or is it limited to discrete-time systems because of some special properties? There is a similar question for proposed heuristic for generating counterexamples. Is this heuristic limited to discrete-time system? If not, can we replace the counterexample generation step in existing algorithms for continuous-time system and see if the performance improves? Another minor concern I have with the PGD heuristic is that it might fail to find a counterexample because gradient-based search can get stuck in local minimums. Thus, in the final step when the algorithm claims success, shall we use a less efficient way to verify the Lyapunov conditions are actually satisfied?
Questions
Please see my comments in the previous section.
Rating
6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.
Confidence
2: You are willing to defend your assessment, but it is quite likely that you did not understand the central parts of the submission or that you are unfamiliar with some pieces of related work. Math/other details were not carefully checked.
Soundness
3 good
Presentation
3 good
Contribution
3 good
Limitations
I didn't see the discussion about limitations or future directions in my read. But I don't think there is any potential negative societal impact.
Summary
This paper presents an algorithmic framework for learning neural Lyapunov control with stablizing control policy for discrete-time dynamic systems. It proposes to verify the stability condition with mixed-integer linear programming and speed up Lyapunov function learning with gradient based approximation. On four benckmarks, it outperforms SOTA baselines in terms of running time, size of regions of attraction and successful rate.
Strengths
- The paper is well structured and nicely presented - The approach has extended the learning of Lyapunov functions to discrete-time dynamic systems, and has been shown effective on 4 benchmarks with a significant improvement.
Weaknesses
See questions and limitations.
Questions
- The paper provides 2 options for setting the bias term in the training loss function. However, it is not crystal clear the impact of this term over the learning. An ablation study over the bias setting could help. - To better motivate the use of mixed-integer linear programming for stability verification in discrete-time systems, it would be good to show a case by comparing DITL-MILP with DITL-dReal. - Does the run time include the initialization time (for example by LQR)?
Rating
7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.
Confidence
3: You are fairly confident in your assessment. It is possible that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work. Math/other details were not carefully checked.
Soundness
3 good
Presentation
3 good
Contribution
3 good
Limitations
- The method is built upon the assumption that both the verification function and control policy can be simply represented with MLPs with ReLU activations.
Thanks for the Response
I appreciate the authors' response to my questions. Since the first weakness is a misunderstanding, I don't have further question on the techinical validity of the proposed approach. I will change to accept.
We appreciate the reviewer's thoughtful consideration of our paper and responses, and glad that we were able to clarify the misunderstanding. Please let us know if you have any further questions.
Thank you very much for the response. I will leave the scores as is.
Thank you for reading our response. Would you be able to clarify why you did not find our responses convincing? We had addressed all of the weaknesses, questions, and limitations that the reviewer had raised. Perhaps the most compelling evidence that our paper significantly advances the state of the art comes from our experimental evidence, in comparison with prior approaches. We explain, both in the paper, and in responses to other reviewers, what technical advances enabled the considerable improvements we observe in the experiments. In particular, what may perhaps be a misunderstanding is that our key observation is that Lyapunov conditions for discrete-time systems possess important structure that we take advantage of.
Mathematically, this reviewer still believes that the essence of the current framework is the same as that for the continuous-time model. I don't agree with the response by the authors for the difference between the discrete- and the continuous-time dynamical systems. Superficially, the stability criteria are different for two different systems; however, the essences are the same, not bringing novel stuffs. The results could be publishable; however, the NeurIPS, as a top-tier platform, is not an appropriate venue for this case. I am really sorry that I cannot be more positive from my experience for this case.
We appreciate the reviewer's continued engagement. Perhaps it is useful to step back for a moment. We surely agree that the two notions *are* different; we are not inclined to litigate here whether this difference is large or small, but simply observe that it exists. Now, our goal is a system with *provable stability guarantees*. While empirically, small differences are often inconsequential, when you aim to achieve provable guarantees, the smallest and most superficial seeming differences can prove consequential. Therefore, we argue that the only relevant question is whether the difference in the Lyapunov condition between continuous-time and discrete-time systems is consequential in regards to the goal of effectively learning provably Lyapunov stable control. Our paper demonstrates that it is. We now explain why in some detail. Recall that in continuous-time settings, the key condition is $\forall x \in D; \nabla_{f_u} V(x) \leq 0$, where $\nabla_{f_u} V(x)$ is Lie derivative of function $V$ w.r.t. vector field $f_u$ at point $x$. In discrete-time settings, it is: $\forall x \in D; V(f(x)) - V(x) \leq 0$. If $V$ is a neural network with ReLU activations, it is not continuously differentiable, which makes it non-obvious how we can construct a MILP to verify the condition on the Lie derivative uniformly over the state space that is needed in continuous-time systems. However, this issue does not come up for the Lyapunov condition in discrete-time systems. An alternative could be to replace ReLU units with continuously differentiable neurons, but these must now be approximated in an MILP formulation using piecewise linear functions, which is a major challenge to scalability and efficacy, as it introduces an approximation gap that makes the Lyapunov condition even more difficult to achieve as we get closer to the origin. Another alternative is to use dReal for verification, but as we demonstrate above (see the data in response to Reviewer NZiv, Comment 2), MILP is in fact a critical ingredient in enabling high efficacy of the proposed approach. The reviewer's intuition that the differences are insignificant is, indeed, an argument for the significance of our contribution. Superficially, the differences may appear small. However, our experiments demonstrate that they are, in fact, highly consequential in that we can fruitfully exploit the particular structure in the discrete-time Lyapunov condition which is absent in its continuous-time counterpart. In particular, the combination of (a) heuristic verification techniques that we propose, and (b) MILP-based verifier that exploits special structure in the discrete-time Lyapunov condition, yields a dramatic improvement in efficacy, as demonstrated by the fact that on two of the more complex domains in our experimental study, our approach *is the only one that successfully learns a provably stable controller*. Moreover, as our ablation studies demonstrate, both of these contributions are critical to the results.
Thank you very much for your reply to my previous comments. In the previous review and comments, I have emphasized the similarity and the difference between the stability results on continuous- and discrete-time dynamical systems. Definitely, they have the difference; however, the essences based for deriving stability criteria are the same. Probably, these authors may not know there is a uniform math framework, dynamical systems on time-scale, for different time-type of dynamical systems. All the stability criteria could be include in one framework. The so-called Lie derivative and the difference computations along the considered systems are essentially the same; all are called the Lyapunov second method or direct method. Actually, even for the continuous-time system, we allow the discussion for the discontinuity in V function or/and in the vector field. I have mentioned that the current results if correct could be publishable. Yet, NeurIPS is NOT an appropriate venue since the presented contribution does not seem to be that significant. Now, after a more care check, I have to report a fatal mistake emergent in the current work. The Lemma 3.1 is NOT mathematically correct. Since the difference between V(f(x))-V(x) upper bounded by only a negative Constant definitely leads to a contradiction and indeed an empty set where the conditions in this Lemma are valid there. Therefore, I cannot imagine how the convergence could be numerically made by the current incorrect theory and the correspondingly developed algorithm. There are a huge amount of rigorous results in the control and cybernetics literature on infinite or finite-time stability for continuous- and discrete-time dynamical systems. The mistake that was found in this manuscript will certainly leads me to the recommendation against the acceptance of this work. I also suggest the other experts to pay their attentions on this problem. I still believe that the essence driven by the rigorous mathematical foundation is crucial for a novel work, especially in the recent area of AI. I am sorry that I still cannot be more positive on this work. Due to the fatal mistake, I therefore will consider to decrease the score.
We appreciate the reviewer's continued engagement and comments. **Regarding Lemma 3.1.** There appears to be a misunderstanding, and we sincerely apologize for not being clear when stating Lemma 3.1. In our footnote 1 on page 3 (prior to the lemma) we mentioned that we introduce a constraint $|| x||\geq \epsilon$ (all norms are $\infty$-norm), where $\epsilon$ is a small pre-defined parameter, in order to mitigate numerical instability of verification. This constraint does not affect the overall convergence and is also employed in the baseline papers [Chang et al., 2019, Zhou et al., 2022]. Throughout the paper, this constraint is treated as a prior. We establish the Lyapunov condition for $|| x|| \geq \epsilon$ only, and our controller drives the system to converge to $|| x||< \eta$, a small region close to the origin. In Lemma 3.1, the symbol $\zeta$ should actually be $\zeta (\epsilon)$, indicating that the choice of the negative constant $\zeta$ depends on the chosen value of $\epsilon$ in order to ensure that the condition in Lemma 3.1 does not induce an empty set. Consequently, it will not lead to any contradiction when the conditions in Lemma 3.1 are met. Our experiments demonstrate this. We acknowledge that the footnote could easily be overlooked by the reader, and the proof sketch is, of course, incomplete (we did not have the space to include all of the details, and prioritized the algorithmic and empirical aspects of the problem). Nevertheless, the reviewer's point is well taken, and we will add a more precise statement and proof in the revision that also shows that we are both guaranteed to reach the $\eta$-ball around the origin in finite time, and remain in this ball thereafter. Specifically, we will revise Lemma 3.1 and its complete proof as follows: **Lemma 3.1:** Let $L_f$ and $L_v$ denote the Lipschitz coefficients of $\overline{f}(x)=f(x,\pi_\beta(x))$ and $V_\theta$, respectively. Suppose there exist positive constants $\epsilon$, $\rho$, $\gamma$, and a negative constant $\zeta$ such that the following properties hold: (a) $V_{\theta}(f(x,\pi_\beta(x))) - V_{\theta}(x) < \zeta$ for all $x$ with $\epsilon \leq ||x|| \leq \gamma$, (b) {$x: V_\theta(x) \leq \rho$}$ \subseteq B(0,\gamma)$ (where the ball is with respect to the $\infty$-norm), (c) $V_\theta(0) = 0$, (d) $f(0,\pi_\beta(0)) = 0$, and (e) $L_{v}L_{f}\epsilon \leq \rho$. Then the following properties hold: (i) The set {$x: V_\theta(x) \leq \rho$} is positive invariant under dynamics $f$ and control policy $\pi_\beta$, and (ii) If $V_\theta(x_0) \leq \rho$, then there exists $K \in ${$0,\ldots,\lceil \frac{\rho}{-\zeta} \rceil $} such that $||x_{K}|| < \epsilon$, and $||x_k|| < \eta$ for all $k > K$, where $\eta$ is the radius of the smallest $\infty$-norm ball containing the set {$x: V_{\theta}(x) \leq L_{v}L_{f}\epsilon$}. **Proof:** We first prove property (i). Suppose that $V_\theta(x) \leq \rho$. If $||x|| \in [\epsilon,\gamma]$, then $V_\theta(f(x,\pi_\beta(x))) < V_\theta(x) \leq \rho$ by conditions (a) and (b). If $||x|| \leq \epsilon$, then $V_\theta(f(x,\pi_\beta(x))) = |V_\theta(f(x,\pi_\beta(x)))-V_\theta(f(0,\pi_\beta(0)))|$ by conditions (c) and (d), and thus $V_\theta(f(x,\pi_\beta(x))) \leq L_{f}L_{v}||x|| \leq \rho$ by condition (e). Hence property (i) holds. To prove property (ii), suppose that $V_\theta(x_0) \leq \rho$. Since {$x: V(x) \leq \rho$} is positive invariant by the above, we must have that $||x_k|| \leq \gamma$ for all $k \geq 0$ by condition (b). Suppose that, for all $k^{\prime} \in ${$0,\ldots \lceil \frac{V(x_0)}{-\zeta} \rceil $}, we have $||x_{k^{\prime}}|| > \epsilon$. Then at time $k^{\prime} = \lceil \frac{V(x_0)}{-\zeta} \rceil$, we have that $V(x_{k^{\prime}}) = V(x_0) + \zeta k^{\prime} < 0$, contradicting positive-definiteness of $V$. This contradiction, together with the fact that $V_\theta(x_0) \leq \rho$, implies that $||x_K|| \leq \rho$ as in property (ii). Finally, by the discussion of the preceding paragraph, the set {$x: V_{\theta}(x) \leq L_{f}L_{v}\epsilon$} is positive invariant and contained in $B(0,\eta)$, and $||x_k||< \epsilon$ implies $V_{\theta}(x_{k+1}) \leq L_{f}L_{v}\epsilon$. Hence $||x_k|| \leq \eta$ for all $k > K$. This completes the proof. We observe that, within the network structures considered in our experiments, $\eta$ can be made arbitrarily small by reducing $\epsilon$, i.e., we can prove that the state converges to and remains within an arbitrarily small ball centered at the origin. We confirmed that all the conditions in Lemma 3.1 held in our numerical experiments. The negative constant $\zeta$ choosen in our experiments was -0.00001, which ensured that the conditions in Lemma 3.1 are meaningful. In any case, connecting all the relevant pieces here amounts to exploiting the Lipschitz continuity assumption on $f$, and Lipschitz continuity of neural networks with ReLU activations.
This reviewer thanks the efforts made by the authors of this work. However, clearly, the footnote 1 was only used for avoiding the numerical instability in simulations, not for realizing the stabilization of the equilibrium rigorously. Once Lemma 3.1 is fixed as the manner proposed in the above reply, the convergence of the equilibrium is no longer ensured mathematically and rigorously. Without a solid foundation, all the stabilization results obtained numerically in the present work is NOT convincing yet. Actually, there were compact and correct results from theoretical viewpoint to resolve the fatal problem in the literature even ten years ago. I believe with these stability results for discrete-time systems, the algorithm could be amended into a correct manner. Unfortunately, control protocol proposed in the reply is not correct, not assuring the stability of the equilibrium, but at most the attracting property of the small neighborhood of the equilibrium. Even using the proposed Lemma 3.1 for designing the numerical application, one needs to make a lot of discussions on the choice of the parameters including \epsilon. This has not been completely done yet in the current work, which could be included in the future work. Clearly, the core problem of the stabilization cannot be resolved at the present stage, which leads me definitely to sustaining my recently amended score.
**Regarding Dynamical Systems on time-scale.** The unified framework of dynamic Lyapunov equations on time scales is certainly elegant, but orthogonal to our goals. The former is a mathematical unification; our interest, however, is to develop new computational methods for checking stability of a discrete-time system. We are not trying to derive new conditions for discrete-time stability. The reviewer is correct that the discrete and continuous time Lyapunov direct methods are very similar; however, note that the algorithms for stability checking can be different. This difference allows us to exploit specific structures in the Lyapunov conditions in discrete-time systems and thereby obtain a learning-based approach with significantly better performance that all state-of-the-art alternatives. At the high level, we feel that our perspective on the problem is different from that of the reviewer. The reviewer views it predominantly through a mathematical lens. On the other hand, our perspective is largely computational and empirical. We hope that the reviewer can consider this contribution from an alterantive perspective of developing a learning algorithm that exploits problem structure to computational advantage, and yields compelling empirical results. We argue that contributions of this kind are no less significant in AI than work focused primarily on foundational mathematical issues.
Mathematical formulation of a problem is so important. If the authors knew very much about the stability theories for different time-type of dynamical systems, the current mistake would not happen. I am not argue with you the importance of the mathematics, but my point is: A correct mathematical principle can assure the correct development direction of engineering work. If the theory is wrong or not complete (this work unfortunately falls into this case), then how to guarantee the stability as expected in real applications. All results are empirical, which could be publishable, not in this venue of NeurIPS. I am really sorry that I cannot be more positive.
We appreciate the reviewer's quick response. In a nutshell, the two main issues raised by the reviewer are summarized below, with our comments about them. ***Comment:*** *Unfortunately, control protocol proposed in the reply is not correct, not assuring the stability of the equilibrium, but at most the attracting property of the small neighborhood of the equilibrium.* ***Response:*** We regret the reviewer's use of hyperbolic language of "incorrect" here. Because of numerical precision limits, in general all computational methods can ensure at most the attracting property of the small neighborhood of the equilibrium. We thought this was clear given prior work (such as [Chang et al., 2019, Zhou et al., 2022]) that we are after a weaker form of stability than conventional, but can see that the reviewer objects to calling it "stability". This is a criticism of this entire line of work, and one we disagree with. In any case, this issue is not a mistake, but a difference in the meaning of a term (that is, the term is indeed effectively overloaded in the literature on learning stable controllers). What is clear is that empirically this distinction is quite inconsequential (that is, reaching close enough to the origin suffices). $\ $ ***Comment:*** *All results are empirical, which could be publishable, not in this venue of NeurIPS.* ***Response:*** Correct, this is a computational and empirical work. We do not claim to develop new theory, but simply leverage known theory of Lyapunov stability in discrete-time dynamical systems. It is worth mentioning that two of our main baselines [Chang et al., 2019, Zhou et al., 2022], were both published at NeurIPS. $\ $ At this point, it is clear that the reviewer and the authors are effectively speaking different languages, with the same words having a different meaning. It is likely that we come from somewhat different subcommunities of NeurIPS with different publishing styles and traditions.
1. Clearly, in the manuscript, the authors claimed the efficacy of their neural control protocol in asymptotical stabilization of the equilibrium. The definition of this stability was clearly stated from lines 95 to 96 in the original manuscript, requiring x(t) approaching zero, NOT wandering in the neighborhood of the equilibrium (as defined in the reply). The revised Lemma 3.1 can only assure the boundedness of the trajectory, but cannot guarantee the asymptotical stability of the equilibrium. This is the typical and scientific language in the communities of control and cybernetics. If one leverages the theory of control and machine learning techniques to solve typical control problems, the elementary and standard terminology should be taken into account. More importantly, the authors clearly stated their definition of stability in their response to the comment #2 from Reviewer ruNW. "In contrast, the stability notion we are concerned with is defined as follows: a system is stable within a region of attraction (which includes the origin) if..." If they are going to change their definition, then the entire work, as well as the basic mission, should be completely and substantially rewritten. 2. To be frank, the mistake actually could be amended; however, the authors did not make a good of the hint given by this reviewer since there are CORRECT and existing theories to guarantee the stability of the equilibrium for discrete-time dynamical systems in control literature, not in math literature. 3. Probably, we do not use the same system of language because this reviewer not only focuses on the rigorous theory but also the empirical and feasible control methods. 4. Actually, all the continuous-time system, when put into simulations, should be discretized as a discrete-time system; otherwise the computation is not feasible. Understanding the basic principles of different time-scale of dynamical systems could be beneficial to avoiding a trap of common mistakes emergent in control community. 5. Here, I do not intend to comment the previous works mentioned by the authors. Indeed, I do not agree with the argument that they regarded as this work to be in the direction the same as the previous ones. Actually, the previous works presented the correct theory, allowing the minor errors in simulations because of the discretization. However, these authors actually go in an opposite way: using the incorrect or incomplete stability theory (see Lemma 3.1, their definition (lines 95-96) in original manuscript, and their reply to the other Reviewer ruNW's comment #2), generating the simulations whose fidelity are not thoroughly investigated. Above all, this work now is deviating from the original intention and needs substantial rewritten. Minor revision is not applicable.
Dear Reviewer ruNW. Thank you again for your review. As the author-reviewer discussion phase is closing relatively soon, we hope you will be able to take a look at our detailed responses, which address all three of your questions and concerns. In particular, we would be very happy to field any additional questions that you may have.
Thank you for the detailed response. The rebuttal has clearly clarified my questions and I would like to keep my current scores!
Thank you for the detailed response. I don't have other questions.
Overall Comment to the Reviews
We thank all reviewers for their comments and valuable feedback. Below we summarize our overall (main) response to the reviewers' questions and suggestions. 1. (reviewer NZiv) We have conducted two sets of additional experiments: 1) ablation study of the bias term; 2) DITL-dReal, where the MILP solver in our algorithm is replaced by the dReal solver. In both cases, our approach achieves the best results. 2. (reviewer qMzc, KEba) We have explained the challenges that are specific to the discrete-time system versus continuous time, and that we could leverage the specific structure of discrete-time system to significantly improve performance. 3. (reviewer qMzc, KEba) We have clarified that our work provides strict verification. We use both heuristic and sound counterexample generation (using MILP). That is, we achieve provable stability by resorting to full MILP-based verification whenever the PGD heuristic can no longer identify counterexamples. 4. (reviewer ruNW) We have clarified that the paper referenced by the reviewer solves a different problem from ours. Specifically, it is more useful for providing safety than stability guarantees. 5. (reviewer yt77) We argue that computational and empirical work also has significant value in the AI community, and disagree with the reviewer's view that this kind of work is not publishable at NeurIPS. It is worth mentioning that two of our main baselines [Chang et al., 2019, Zhou et al., 2022], were both published at NeurIPS. As of the dynamical systems on time-scale framework mentioned by the reviewer, it is orthogonal to our goals. The former is a mathematical unification; our interest, however, is to develop new computational methods for checking stability of a discrete-time system. 6. (reviewer yt77) We clarified and made more precise the claim in Lemma 3.1, and provided its complete proof. The lemma provides theoretical guarantee that our controller will both guaranteed to reach the $\eta$-ball around the origin in finite time, and remain in this ball thereafter. To clarify, this $\eta$-ball variation on traditional Lyapunov stability is also used in our baselines [Chang et al., 2019, Zhou et al., 2022], to mitigate numerical precision and stability issues that inevitably arise. **Lemma 3.1:** Let $L_f$ and $L_v$ denote the Lipschitz coefficients of $\overline{f}(x)=f(x,\pi_\beta(x))$ and $V_\theta$, respectively. Suppose there exist positive constants $\epsilon$, $\rho$, $\gamma$, and a negative constant $\zeta$ such that the following properties hold: (a) $V_{\theta}(f(x,\pi_\beta(x))) - V_{\theta}(x) < \zeta$ for all $x$ with $\epsilon \leq ||x|| \leq \gamma$, (b) {$x: V_\theta(x) \leq \rho$}$ \subseteq B(0,\gamma)$ (where the ball is with respect to the $\infty$-norm), (c) $V_\theta(0) = 0$, (d) $f(0,\pi_\beta(0)) = 0$, and (e) $L_{v}L_{f}\epsilon \leq \rho$. Then the following properties hold: (i) The set {$x: V_\theta(x) \leq \rho$} is positive invariant under dynamics $f$ and control policy $\pi_\beta$, and (ii) If $V_\theta(x_0) \leq \rho$, then there exists $K \in ${$0,\ldots,\lceil \frac{\rho}{-\zeta} \rceil $} such that $||x_{K}|| < \epsilon$, and $||x_k|| < \eta$ for all $k > K$, where $\eta$ is the radius of the smallest $\infty$-norm ball containing the set {$x: V_{\theta}(x) \leq L_{v}L_{f}\epsilon$}. **Proof:** We first prove property (i). Suppose that $V_\theta(x) \leq \rho$. If $||x|| \in [\epsilon,\gamma]$, then $V_\theta(f(x,\pi_\beta(x))) < V_\theta(x) \leq \rho$ by conditions (a) and (b). If $||x|| \leq \epsilon$, then $V_\theta(f(x,\pi_\beta(x))) = |V_\theta(f(x,\pi_\beta(x)))-V_\theta(f(0,\pi_\beta(0)))|$ by conditions (c) and (d), and thus $V_\theta(f(x,\pi_\beta(x))) \leq L_{f}L_{v}||x|| \leq \rho$ by condition (e). Hence property (i) holds. To prove property (ii), suppose that $V_\theta(x_0) \leq \rho$. Since {$x: V(x) \leq \rho$} is positive invariant by the above, we must have that $||x_k|| \leq \gamma$ for all $k \geq 0$ by condition (b). Suppose that, for all $k^{\prime} \in ${$0,\ldots \lceil \frac{V(x_0)}{-\zeta} \rceil $}, we have $||x_{k^{\prime}}|| > \epsilon$. Then at time $k^{\prime} = \lceil \frac{V(x_0)}{-\zeta} \rceil$, we have that $V(x_{k^{\prime}}) = V(x_0) + \zeta k^{\prime} < 0$, contradicting positive-definiteness of $V$. This contradiction, together with the fact that $V_\theta(x_0) \leq \rho$, implies that $||x_K|| \leq \rho$ as in property (ii). Finally, by the discussion of the preceding paragraph, the set {$x: V_{\theta}(x) \leq L_{f}L_{v}\epsilon$} is positive invariant and contained in $B(0,\eta)$, and $||x_k||< \epsilon$ implies $V_{\theta}(x_{k+1}) \leq L_{f}L_{v}\epsilon$. Hence $||x_k|| \leq \eta$ for all $k > K$. This completes the proof. We observe that, within the network structures considered in our experiments, $\eta$ can be made arbitrarily small by reducing $\epsilon$, i.e., we can prove that the state converges to and remains within an arbitrarily small ball centered at the origin.
Decision
Accept (poster)