Venue: NeurIPS 2022 Conference

Reviews:

final_score: rating: 6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.
review_content: summary: This paper proposes a neural architecture that can (1) learn dynamics, (2) find a Lyapunov function and corresponding nonlinear stabilizer simulatenously. Using a satisfiability modulo theories (SMT) solver is also applied to verify the Lyapunov conditions of the candidate Lyapunov function. The authors claim that simultaneous learning of both the function and stabilizer helps to draw stability guarantees and overall better performance. This paper contains detailed theoretical guarantees and multiple experimental evidence, including comparison studies with existing methods.

strengths_and_weaknesses: This is overall a solid paper that retains theoretical and empirical novelties for challenging nonlinear control problems. This paper provides detailed theoretical guarantees and various experimental results. Meanwhile, I have also noted some concerns about the proposed methodology. I hope to see a response to these points during the rebuttal.


### Strengths

* This paper is quite well written. The authors put a lot of effort into providing relevant information in the Introduction and Preliminaries sections. The algorithm and learning schemes were easy to follow.
* As far as I know, the proposed neural network architecture and algorithm are novel. These can contribute to finding the Lyapunov function for learning real-time physical systems with unknown dynamics. The theoretical results presented in this paper are sound.
* This work presents trainable nonlinear controllers and Lyapunov function using neural networks. I think involving an SMT solver in the algorithm is a good approach.

### Weaknesses

* In the algorithm, I think the part of learning dynamics is not polished. The authors make assumptions that the dynamics are unknown. In this sense, oftentimes, it will be hard to collect trainable data, and it cannot be appropriate for a neural network to train dynamics by only using SGD. It seems that the overall performance of the algorithm is tightly coupled with the performance learned dynamics $f_\phi$. Although Theorem 2 ("an extension of the universal approximation theorem") is presented, I think there are some real challenges that dynamics learning struggles. I can imagine multiple realistic issues regarding model complexity and data, so the learning dynamics might fail.

* In the experiments, it would be better if there was a metric to compare ROA estimation performance between the proposed approach and LQR. I cannot grasp "how much" learning the Lyapunov function outperforms LQR.
questions: 1. I am interested in using a solver in the algorithm. How did you choose an SMT solver for the experiments? Was there an extenstive ablation study for choosing an appropriate solver?

limitations: Even though most of the claims are sound, I also believe that the amount of experiments that are shown in this paper is limited, and the network sizes used in this work are relatively small. I am concerned about the general usability of this model for the complex nonlinear dynamical system, which is a core claim of this paper. The generality of the method needs to be validated with bigger data and larger neural networks.
review_title: null

final_score: rating: 6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.
review_content: summary: This paper proposed a framework to learn the non-linear system and control it with a neural controller and certified Lyapunov function. The system asymtotic stability can be proved by the negative Lie derivative of Lyapunov function. The satisfiability of Lyapunov function is achieved by running the SMT solver and learning framework iteratively. The effectiveness is demonstrated by 3 illustrative experiments.
strengths_and_weaknesses: Strengths

1. The paper structure is easy to follow. The experiments are well organized and helpful for theorem illustration.
2. Under the framework of [1], The paper provides the proof of Lyapunov function existence and stability guarantee by quantifying the errors among unsampled states and nearest training samples.

[1] Ya-Chien Chang, Nima Roohi, and Sicun Gao. Neural Lyapunov Control. In arXiv:2005.00611 [cs, eess, stat], December 2020. arXiv: 2005.00611.

Weaknesses:

1. With many of the methods inherited from previous [1], other than the theoretical improvement, I suggest the authors to include the methodology difference of this paper and [1], along with the experimental comparison. 
2. The formation of the problem(low dim system) and neural network structure are relatively simple. It would be interesting to see how the method applies in more complex system.
3. The major improvement of this paper is the theoretical proof of stability over the previous work. However, I’m confused by the derivation logic. See my question 3 and 4. 
questions: 1. In Assumption 1 and line 166, the distance of (x,u1) and (y,u2) is a bit ambiguous with undefined “-” operator. It’s better to denote (x,y) as the concatenated vector for clarification.
2. Can you provide the proof for theorem 5 from your reference [29]? 
3. Theorem 2 claims the existence of 1-hidden-layer neural network $\phi$ to approximate the unknown dynamics, based on universal approximation theory. However, this only proves the existence but not the actual learn  $\phi$ would satisfy such approximation accuracy. Similar for theorem 5. For instance, in line 503 of appendix, I’m wondering how to prove the actual $V_{\phi}$ satisfy the Lyapunov condition given theorem 5 only claims the existence?
4. I’m curious how to approximate M in line 167. If upper bound of $\lVert \frac{\partial V}{\partial x}\rVert $is approximated by sampling then this is not a guarantee. Same question applied to other Lipschitz constants.
limitations: This paper does not have potential negative societal impact.
review_title: null

final_score: 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.
review_content: summary: The paper addresses the challenging task of guaranteeing asymptotic stability of an unknown nonlinear system by simultaneously learning the unknown dynamics (via a neural network) and a valid Lyapunov function for the learned dynamics. They provide an extension of the method proposed by Chang et. al (ref. [6]) to unknown nonlinear systems.

The problem is fundamental in the sense that it bridges the gap between theoretical control theory and data-driven control by being able to guarantee strong stability properties for unknown and general nonlinear systems.

strengths_and_weaknesses: The strength of the paper is as follows:
1) To the best knowledge of mine, this is the first paper that attempts to provide stability guarantees for unknown nonlinear systems

The weakness of the paper is as follows:
1) Since the SMT solver is not scalable, the approach is restricted to low-dimensional problems and might not be suitable for real-world robotics applications

2) The convergence of the algorithm depicted in Figure 1 is not clear.

More details about the approach are presented under "Questions"
questions: I have the following issues with your approach

1) How do guarantee the existence of a feedback nonlinear controller that would steer the unknown nonlinear system to the origin? For instance, the recent work by Zinage et al. titled “Neural Koopman Lyapunov control” simultaneously learns a Koopman-based bilinear model and a valid Control Lyapunov Function (CLF) for the unknown nonlinear system and consequently guarantees the existence and computes a feedback controller by using the universal Sontag’s formula (provides necessary and sufficient conditions for asymptotic stability for controlled nonlinear systems) which is well studied in the control theory literature.

2) How do you ensure that your designed nonlinear controller would ensure forward invariance for the unknown nonlinear system? In other words, how do you ensure your controller will keep the trajectories within the ROA?

3) The SMT solver is not scalable and hence the computational time needed to compute a valid Lyapunov function increases exponentially as the dimension of the state increases. Consequently, this would restrict your approach to toy examples and therefore the applicability of your approach to real-world robotics problems like humanoids, manipulators, etc. becomes nontrivial.

4) One of the Lyapunov conditions is that V(0)=0. This is a “hard constraint”. However, this condition is added as a soft constraint in your loss function. Hence after the learning process is over, V(0) might not be “exactly” zero which violates one of the Lyapunov conditions thereby not making it to learn a valid Lyapunov function.

5) How is the value of beta chosen? It is mentioned that beta is kept relatively high so as to account for the approximation errors between the unknown nonlinear system and the learned system. I believe that if that is the case it might be sometimes difficult for the SMT solver to satisfy one of the Lyapunov conditions involving beta. It would be beneficial to add a table describing the influence of beta on the computational time required by the SMT solver to generate counterexamples.

6) How do you guarantee the learning process finally converges i.e it is possible to reach a state where there are no more counterexamples that satisfy the falsification constraint?

7) The proof of Theorem 4 is basically from the logic presented in Section 3.2 (Eqns. 8,9 and 10). I would suggest that you add this theorem before Eqns. 8, 9, and 10 and remove it from Appendix (page 14)

8) For some nonlinear systems, there does not exist any linear feedback controller that could stabilize the nonlinear system (however a nonlinear feedback controller exists). In view of that, the controller design in your paper is restricted to only a linear feedback controller (Lines 12-18 of Algorithm 1) which might not steer the nonlinear system in some cases.

9) Please elaborate on how Theorem 6 helps in the proof.

10) I think some important references are missing which are relevant with your work. For instance, the papers titled
“ Neural Lyapunov redesign”
“A ‘universal’ construction of artstein’s theorem on nonlinear stabilization”
“ Neural Koopman Lyapunov Control”


limitations: I would suggest adding a section to discuss the limitations of this approach. For instance, based on the following question
1) Does the learning framework finally converges?
2) SMT solver scalability?
3) Existence of linear feedback controllers?
4) Forward invariance when a linear controller is used?
review_title: null

Meta-review: metareview: The problem statement and the technical approach are interesting. Some concerns about the scalability of the approach remain; however, given the novelty of the approach, I am recommending that the paper be accepted in spite of these concerns. Please make sure to incorporate the reviewers' feedback into the final version. 
confidence: Certain
Decision: Accept