Certified Training with Branch-and-Bound: A Case Study on Lyapunov-stable Neural Control

Clarification on branch-and-bound

Is the training dataset $\mathbb{D}$ a set of points or regions? What does it mean by $(\underline{x}, \overline{x})$in Line 269?

The training set is a set of regions, not points. Each $(\underline{x}, \overline{x})$ means a subregion (a bounding box). We defined them at the beginning of Section 3.2 around Line 218-Line 220 in our initial submission: “each example $(\underline{\mathbf{x}}^{(k)}, \overline{\mathbf{x}}^{(k)})~(1\leq k\leq n)$ is a subregion in $\mathcal{B}$, defined as a bounding box $\{\mathbf{x}: \mathbf{x}\in\mathbb{R}^{d},\,\underline{\mathbf{x}}^{(k)} \leq \mathbf{x} \leq \overline{\mathbf{x}}^{(k)}\}$ with boundary $\underline{\mathbf{x}}^{(k)}$ and $\overline{\mathbf{x}}^{(k)}$”.

Does the proposed approach need to verify that g(x)≤0 for every region?

Yes, the condition needs to be verified for the entire region-of-interest $\mathcal{B}$ (i.e., all the subregions). This requirement is necessary for the formal verification of Lyapunov stability and it is the same as that in previous works on Lyapunov stability (Wu et al., 2023; Yang et al., 2024).

If so, then how does this work scale to high-dimensional systems?

Lyapunov stability is a relatively strong guarantee and existing works on Lyapunov stability with formal guarantees have commonly focused on relatively low-dimensional systems so far (Chang et al., 2019; Wu et al., 2023; Yang et al., 2024), which we have mentioned as a limitation in the conclusion section.

In the conclusion section, we also mentioned that future works may consider training-time branch-and-bound on activation functions instead of input, in order to scale to high-dimensional systems. It is motivated by existing works on neural network verification methods which typically conduct branch-and-bound on activation functions for high-dimensional problems, because there is often sparsity in the active/inactive status of activation functions such as ReLU, which can be efficiently leveraged by verifiers so that branching on activation functions can be more efficient than branching on the large input. However, it remains an open problem to conduct certified training and train verifiable models by training-time branch-and-bound on activation functions, for Lyapunov stability in high-dimensional systems. We believe this is an important direction for future works.

We appreciate your constructive feedback and the detailed list of references. We wanted to provide an early response since we believe most weaknesses mentioned are due to misunderstandings and misconceptions. We have clarified why some previous work (Jin et al., 2020) did not actually achieve formal guarantees. We also clarified the difference between barrier functions and Lyapunov functions, and we have extended the discussion of the related work of our paper (see the updated PDF), cited the papers you mentioned, and discussed the key differences. We believe that none of these papers on barrier functions are valid baselines for empirical comparison, since our setting on Lyapunov stability is clearly different. We also provided a clarification on branch-and-bound.

Some previous works without formal verification

We thank the reviewer for raising this point for us to make our related work section more clear and comprehensive. But we would like to clarify that we believe it is the fact that several works we cited (Jin et al., 2020; Sun & Wu, 2021; Dawson et al., 2022; Liu et al., 2023), especially Jin et al., 2020 which the reviewer has mentioned, did not achieve formal guarantees, and our writing is not “in a misleading way”. It is clear that Sun & Wu, 2021; Dawson et al., 2022; Liu et al., 2023 did not consider formal verification. We will explain Jin et al., 2020 in more detail.

There have been extensive works on neural barrier function learning or barrier/policy joint learning $1,2,3$ . The authors misinterpret these works by claiming that they, including $2$ , "did not provide formal guarantees".

We believe we did not misinterpret them. We did not say $1, 3$ which are not about Lyapunov stability “did not provide formal guarantees”. Please refer to our response in the “Related works on other safety guarantees in control” section regarding related works on barrier functions which are different from Lyapunov functions for stability.

Now we will explain why Jin et al., 2020 ( $2$ in the review) did not achieve formal guarantees. The lack of formal guarantees in Jin et al., 2020 has also been confirmed by multiple previous works: Edwards et al., 2023; Abate et al., 2024; Yang et al., 2024 have all mentioned that Jin et al., 2020 is either unsound (regarding the certificates) or did not provide formal guarantees.

The reviewer has mentioned page 6 in Jin et al., 2020 which appeared to discuss verification. However, while Jin et al., 2020 has theoretically aimed to achieve a verification and included a discussion on the verification, their theoretical explanation is based on an assumption that the model is Lipschitz continuous and a (sound) Lipschitz constant is available. In their actual implementation, they only empirically checked a finite number of samples, without actually computing the Lipschitz constant which their verification scheme depends on. Thus, they have not achieved a formal verification, especially computing sound and sufficiently tight Lipschitz constants is nontrivial and could be challenging in practice (Jordan et al., 2020; Shi et al., 2022). Specifically, in Page 6 in Jin et al., 2020, it is mentioned that “we only verify if $\\min\_{i=1,2,\\cdots} V\_{\\boldsymbol{\\omega}}(\\mathbf{x}^i\_{g})\\leq \\epsilon\_2$, where $\\epsilon\_2\>0$ is a small constant parameter that bounds the tolerable numerical error, and $\\mathbf{x}^i\_g$ are the points in the discretization of $\\mathcal{\\bar{X}}\_g$”. We have revised the paper to explain it.

Jin, Wanxin, Zhaoran Wang, Zhuoran Yang, and Shaoshuai Mou. "Neural certificates for safe control policies." arXiv preprint arXiv:2006.08465 (2020).

Edwards, A., Peruffo, A., & Abate, A. (2023). A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis. arxiv: 2309.06090

Abate, A., Bogomolov, S., Edwards, A., Potomkin, K., Soudjani, S., & Zuliani, P. (2024). Safe Reach Set Computation via Neural Barrier Certificates. arXiv preprint arXiv:2404.18813.

Yang, L., Dai, H., Shi, Z., Hsieh, C. J., Tedrake, R., & Zhang, H. Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation. In Forty-first International Conference on Machine Learning.

Jordan, M., & Dimakis, A. G. (2020). Exactly computing the local lipschitz constant of relu networks. Advances in Neural Information Processing Systems, 33, 7344-7353.

Shi, Z., Wang, Y., Zhang, H., Kolter, J. Z., & Hsieh, C. J. (2022). Efficiently computing local lipschitz constants of neural networks via bound propagation. Advances in Neural Information Processing Systems, 35, 2350-2364.

Related works on other safety guarantees in control

We thank the reviewer for suggesting a more comprehensive related work section. We acknowledge that we missed some previous works on control barrier functions, as we mostly focused on related works on Lyapunov stability which is the main focus of our entire paper.

However, we would like to clarify that Lyapunov functions and control barrier functions are different, and Lyapunov stability is a stronger guarantee than forward invariance guaranteed by control barrier functions. Lyapunov stability guarantees a convergence towards the equilibrium point, while forward invariance only guarantees that the system remains in the invariance set (without reaching an unsafe set) but it does not guarantee a convergence. Similar to previous works on the Lyapunov stability of neural controllers (such as Yang et al., 2024; Wu et al., 2023), we also mainly focused on the Lyapunov stability.

We do agree that control barrier functions are still relevant as they also aim for the safety of controllers. We have added a new paragraph (highlighted in blue in the updated PDF file) in our related work section to discuss related works on other (i.e., non-Lyapunov) safety properties of neural controllers, and we have cited all the new references suggested by the reviewer. We agree that $1$ cited in the review does contain formal verification by a SMT solver for control barrier functions (not Lyapunov functions).

The local/global robustness verification is not quite relevant to this work, and the discussion should be eliminated from the related work.

We mentioned local/global robustness, as there are a large body of works on certified training which was originally proposed for local robustness. Since we consider certified training for neural controllers in this paper, we believe it is necessary to discuss the background of certified training, as well as our motivation of introducing training-time branch-and-bound for certified training, due to the significantly different problem for control here in contrast to robustness.

ROA comparison

ROA considered in this work is also very relevant to the invariant set in control theory. Thus, this work is expected to compare with STOAs in this domain, e.g., $7$ .

As we have clarified above, Lyapunov stability and forward invariance are different and Lyapunov stability is a stronger guarantee, and thus we believe results on these two different types of safety guarantees are not comparable.

While a comparison with state-of-the-art is necessary, the scope should be restricted to works on Lyapunov stability. The existing state-of-the-art on learning Lyapunov-stable neural controllers is Yang et al., 2024 (ICML 2024) and we have already compared our results with those by Yang et al., 2024. Notably, in Yang et al., 2024 and earlier works on Lyapunov stability such as Wu et al., 2023, Dai et al., 2021, and Chang et al., 2019, they also do not compare with any forward invariant set baselines, since the setting is different.

We thank the reviewer for identifying our strengths and providing detailed and constructive feedback. We have revised our paper accordingly (with major changes highlighted in blue in the updated PDF), and we address the weakness points and questions below:

Branch-and-bound

Approach is based on branch-and-bound, which suffers from the curse of dimensionality and thus might not be applicable in high-dimensional systems... This limitation is mentioned in Sec. 5 but a discussion about the theoretical complexity and directions to overcome this limitation would be helpful.

We think a theoretical analysis for the complexity is still an open problem, as to our knowledge, even existing works on branch-and-bound for test-time verification do not have a theoretical complexity. Given the more complicated nature of training-time branch-and-bound which further involves the training dynamics of neural networks, we believe obtaining a theoretical complexity is highly challenging at this time and thus we have to leave it for future work.

In Section 5, we briefly mentioned directions on supporting high-dimensional systems, potentially by considering splits on activation functions instead of input states. It is motivated by existing works on neural network verification methods which typically conduct branch-and-bound on activation functions for high-dimensional problems, because there is often sparsity in the active/inactive status of activation functions such as ReLU, which can be efficiently leveraged by verifiers so that branching on activation functions can be more efficient than branching on the large input. However, it remains an open problem to conduct certified training and train verifiable models by training-time branch-and-bound on activation functions for high-dimensional systems. We believe this is an important direction for future works.

Using your dynamic splitting, are there certain areas that get splitted more often than other areas? How do these areas differ? E.g., are there more splits at V(x) = 0 or similar? Would be nice to get more insights there. Maybe one can visualize the splitted subsets using a heat map or similar to see in which area the most splits occured.

We thank the reviewer for suggesting a visualization for the branch-and-bound. We have added Appendix B for this visualization. As expected, more extensive splits tend to happen when at least one (sometimes all) of the input states is close to that of the equilibrium state, where Lyapunov function values are relatively small and the training tends to be more challenging.

Does the number of regions converge to some maximum or do they continuously get split during training?

For the relatively easy systems (e.g., inverted pendulum as shown in Table 3), the number of regions naturally converges to some maximum, when CROWN can verify all the regions and thus no more split is needed. If CROWN cannot verify all the regions yet, the number of regions can continue growing, but in our implementation, we early stop the training (when it is already sufficient to verify the model by a more extensive branch-and-bound at test time) or we stop splitting at some point as you mentioned.

If we do not stop splitting, as long as the training can succeed, technically the number of regions can still converge to some maximum ultimately. It is because the test-time branch-and-bound can verify all the models, and if the training-time branch-and-bound achieves a comparable level of splitting, compared to the test-time branch-and-bound, the number of regions can ultimately saturate.

However, we believe it is more reasonable to restrict the number of splits during the training (e.g., by stopping splitting at some point if the number of splits is already enough for successful training and verification), as training-time branch-and-bound is more costly than test-time branch-and-bound (many training epochs may be needed on the regions). It can potentially also make the model work better under a limited number of splits (if the number of splits is already sufficient) so that it may reduce the number of required splits at test time.

Why did you decide to stop splitting after 5000 training steps for the quadrotor benchmark?

We have discussed our motivation above. Below we compare the performance when the early stopping for the splitting is enabled v.s. disabled. The training could work under both settings which produces similar ROA, while early stopping the splitting achieves a slightly lower verification time cost at test time. The difference is overall small, so it is optional to stop the splitting early here. We did not early stop the splitting for other systems in our experiments because the training could finish in fewer than 5000 steps.

Branch-and-bound (cont.)

Would it be useful to merge some regions at some point again?

Thanks for the great suggestion. We agree that it can be potentially useful to merge regions -- we may track the branch-and-bound tree during the training, and for two subregions coming from a bigger parent region, if both of them can be verified, we may merge them into the parent region again. In our future work, we plan to investigate the scalability and new techniques to handle higher-dimensional systems, and we will try to implement this merging strategy to see if it can help for harder systems.

Is it sensible to test each dimension before deciding where to split? This might increase the training time (especially if higher-dimensional systems are considered). Would another heuristic make more sence, e.g., sensitivity?

Testing each dimension is a relatively simple approach and it can indeed be more costly if more branching is needed especially for higher-dimensional systems. We would agree that future works may design a smart and efficient heuristic when trying to support higher-dimensional systems.

Sec. 3.3: The initial splits appear a bit random: Would it not be better to start off with the entire region of interest and only refine into subsets where necessary?

We used an initial split instead of starting with a single region, in order to have enough initial regions to fill $1\sim 2$ batches according to the batch size, so that the batch size can remain stable during the training. If we start with a single region, then the actual batch size would be very small and unstable in the beginning (starting from from batch size=1), which we think may not be good for the optimizer, as existing deep learning works typically have a fixed batch size. We have revised our paper and added an explanation.

Applicability to other safety properties

Convergence to a single point within the region of interest is not well motivated (see question below).

Is it sensible to assume a single equilibrium state x*? How is x* determined as x* has to be known to evaluate the equations given sin Sec. 3.4? The authors could discuss the implications of this assumption and how the method needs to be adapted for multiple x*.

It is a typical setting in Lyapunov asymptotic stability. We followed previous works (Wu et al., 2023; Yang et al., 2024) to consider dynamical systems with a single equilibrium state $x^*$. These systems are already known to have a single equilibrium state (all at 0 here), according to previous works or textbooks (mentioned in Section 4.1), and thus we treat it as a prior knowledge. We have revised our paper and added a sentence in Section 3.1 to clarify that.

Would your approach also work for more equilibrium states

According to textbook Murray et al., 2017 (Section 4.1 in the book), if there are multiple equilibrium points, we will need to study the Lyapunov asymptotic stability w.r.t. each equilibrium point individually. And then our method can be applied for each equilibrium point independently.

Murray, R. M., Li, Z., & Sastry, S. S. (2017). A mathematical introduction to robotic manipulation. CRC press.

The paper only considers the safety property of stability, i.e., the actor should steer to some (predefined?) equilibrium state (see question below for other safety properties that could be discussed). if the system does not converge but should not violate a safety property where the actor should stay outside of some unsafe region after some point in time?

Our new training framework is generally formulated in Section 3.2 and Section 3.3, with a specific instantiation and focus for Lyapunov asymptotic stability in Section 3.4. We believe that our framework also has the potential for broader applications including other safety properties in control, such as reachability or forward invariance to ensure that a controller can stay outside of some unsafe region, or systems with disturbance, as you mentioned. These are interesting future directions.

Many previous works focus on a particular kind of safety property -- e.g., Dai et al. 2021, Wu et al. 2023, Yang et al. 2024 all focused on Lyapunov asymptotic stability. Thus we believe it is reasonable for us to also focus on Lyapunov asymptotic stability in this paper.

Random seeds

The results in Sec. 4 are only single-dimensional: Over how many seeds are the runs averaged? Please provide stand deviations where applicable, e.g., the area of ROA.

We followed the previous work Yang et al., 2024 to use a single seed, and thus standard deviations were not originally applicable. Additionally, we have extended our experiments to use 5 different random seeds on the 2D quadrotor systems as shown below. Our method has relatively stable performance while significantly outperforming Yang et al., 2024.

High-dimensional systems

Additionally, we would like to see more examples involving high-dimensional systems to demonstrate the efficiency of the proposed method.

As acknowledged in our conclusion section, existing works and our work so far are all limited to relatively low-dimensional systems, for the problem of Lyapunov (asymptotic) stability which is a relatively strong guarantee.

In the conclusion section, we also mentioned that future works may consider training-time branch-and-bound on activation functions instead of input, in order to scale to high-dimensional systems. It is motivated by existing works on neural network verification methods which typically conduct branch-and-bound on activation functions for high-dimensional problems, because there is often sparsity in the active/inactive status of activation functions such as ReLU, which can be efficiently leveraged by verifiers so that branching on activation functions can be more efficient than branching on the large input. However, it remains an open problem to conduct certified training and train verifiable models by training-time branch-and-bound on activation functions, for Lyapunov stability in high-dimensional systems. We believe this is an important direction for future works.

Background of Lyapunov stability and difference with Yang et al., 2024

Due to the limited length of the article, the discussion of related work should be appropriately integrated into the introduction. It is necessary to introduce the relevant theories and background on system stability and Lyapunov functions. The paper focuses on the work of Yang et al.; we suggest that the authors provide a brief explanation to highlight the differences between their method and the new approach presented in this paper.

We thank the reviewer for suggesting an explanation on the background of Lyapunov asymptotic stability, which we agree is important. We have revised our introduction section to include an explanation (highlighted in blue in the updated PDF), as:

"It involves finding a Lyapunov function which intuitively characterizes the energy of input states, where the global minima of Lyapunov function is at an equilibrium point. If it can be guaranteed that for any state within a region-of-attraction (ROA), the controller always makes the system evolve towards states with lower Lyapunov function values, then it implies that starting from any state within the ROA, the controller can always make the system converge towards the equilibrium point and thus the stability can be guaranteed."

We have also highlighted the difference compared to previous works in the revised introduction section, as:

"To do this, we optimize for verified bounds on subregions of inputs instead of only violations on concrete counterexample data points, and thus our approach differs significantly compared to Wu et al. (2023); Yang et al. (2024)."

We thank the reviewer for constructive feedback and we have revised our paper accordingly (see our updated PDF, with changes highlighted in blue). We believe there was some misunderstanding regarding the soundness of our method (the models produced by our method have actually been formally verified) and we have provided clarification below. We also explained our comparison with baselines and extended our comparison to include an earlier baseline. We also explained the common limitation of existing works in the dimension of systems and provided directions for future works. Finally, we also added an early discussion on the background of Lyapunov asymptotic stability in the introduction section.

Soundness guarantees

We would like to clarify that our method produces models with formal soundness guarantees.

As mentioned in the “Implementation” paragraph in Section 4.1, after the models are trained, we use α,β-CROWN, a formal complete verifier, to verify the Lyapunov condition with ROA for our models. This evaluation with formal verification follows Yang et al., 2024 and thus it has provided the soundness for our work. All the models can be successfully verified as shown in Table 2 and Table 3. We have also revised our paper (near the end of Section 3.2) to clarify that a formal verifier is employed at test time to ensure soundness.

Although a Lyapunov function is obtained through learning, there may be some errors. Does the learned Lyapunov function truly satisfy the stability conditions? Could the authors provide an explanation for this?

As explained above, the conditions have been formally verified at test time by α,β-CROWN.

These methods not only provide formal correctness guarantees (in contrast to the simulation testing used in this paper)

We would like to clarify that our paper does not use “simulation testing”. Instead, we use formal verification by α,β-CROWN at test time, and thus our method achieves formal guarantees.

Generally, the consistency between experimental results and theoretical foundations provides assurance for the validity of the method. I do not understand why the method's efficiency is indicated solely based on empirical evidence, especially since these experiments are limited and conducted in low dimensions.

The performance of neural network-based approaches typically need to be demonstrated by experiments. Although there are formal soundness guarantees in our evaluation after models are trained, it is hard to theoretically guarantee what solution the training process can find, just like most other deep learning works, due to the complicated nature of the training process. This is consistent with previous works such as Dai et al., 2021, Wu et al., 2023, Yang et al., 2024 -- none of them could provide any guarantee on the convergence of training, but the Lyapunov conditions can be formally verified at test time after models are trained in the experiments.

The empirical advantage of our proposed method is also supported by our motivations -- since we use verified bounds at test time for verification, we propose to optimize verified bounds during training by certified training, and a training-time branch-and-bound is proposed to enhance the training given that the properties need to satisfy on the entire region-of-interest which is a relatively large region.

Comparison with baselines

The experimental section of this paper provides only limited comparisons with the related work of Yang et al., 2024, making it difficult to assess the reliability of the experimental results. The authors should also compare their method with other approaches to highlight the contributions of this work.

Yang et al., 2024 is the previous state-of-the-art work on this problem and thus we mainly compared our work with Yang et al., 2024 to demonstrate our performance. There are a limited number of learning-based approaches on the same problem setting. Additionally, we have revised our paper to also include applicable results for Wu et al. 2023 in Table 2. Wu et al. 2023 underperforms Yang et al., 2024 with much smaller ROA and is only applicable on some of the systems (e.g., Wu et al., 2023 cannot correctly scale to systems with 6 input states such as the 2D quadrotor system, as discussed in Yang et al., 2024). Our method also achieves much larger ROA compared to Wu et al., 2023.

We thank the reviewer for constructive feedback. We have clarified our contributions compared to previous works, where we highlight our novel contributions on training, not verification. We have extended our related work section to include all the references you mentioned. We also added additional results on varying the activation function and random initialization. Finally, we provided some additional explanation and fixed a typo.

Comparison with previous works

The setting and Lyapunov synthesis condition is exactly the same as $1$ . The only difference is that the certification uses BaB framework instead of adversarial robustness, which makes the contribution not too significant, since BaB framework for neural network verification is also pretty common (e.g., $7,8$ ), especially for RELU network.

We would like to clarify that our main contribution is on the first certified training framework for Lyapunov-stable control, where our training framework is enhanced with training-time branch-and-bound. Although our problem setting follows Yang et al., 2024, our focus is on the training framework which we believe is novel. Our contributions on the training framework are also significantly different compared to Bunel et al., 2020, Wang et al., 2021 which are for verifying trained models. Importantly, our method could enable the training of more verification-friendly models to obtain stronger guarantees (such as larger ROA in this paper), which previous works such as Bunel et al., 2020, Wang et al., 2021 could not do. Our contributions are thus crucial for training/building verifiable models in mission-critical applications, not just verifying/testing existing models.

It would be great to see some variations using different reachability tools other than α−β CROWN, such as in Sherlock $2$ , nnenum $3$ , etc. Also it would be interesting to compare the current setup with some existing NNCS (Neural Network Control System) verification tools, such as NNV $4$ , Polar-Express $5$ , CORA $6$ , etc.

We have extended our related work section to cover all the references you mentioned.

Verification for Lyapunov-stable neural control has been benchmarked in the recent 5th International Verification of Neural Networks Competition (VNN-COMP'24) (https://sites.google.com/view/vnn2024). Models were developed by Yang et al., 2024 and built into a benchmark called LSNC (short for Lyapunov-stable neuron control). The results have been reported at https://docs.google.com/presentation/d/1RvZWeAdTfRC3bNtCqt84O6IIPoJBnF4jnsEvhTTxsPE/edit#slide=id.g279a3ebee4e_5_383 (publicly available, linked at https://sites.google.com/view/vnn2024).

The competition has participants including α−β-CROWN, NNV, nnenum, and CORA which you have mentioned. Among those participants, only α−β-CROWN could support the LSNC benchmark. In total, there were only two teams of participants supporting the LSNC benchmark (α−β-CROWN and PyRAT), with α−β-CROWN significantly outperforming PyRAT (α−β-CROWN successfully verified all, while PyRAT only verified 15 out of 40 subregions). Therefore, VNN-COMP’24 has already shown the difference of those verifiers in terms of verifying trained models. Since our focus is on training, not verification, we believe it is reasonable for us to adopt the state-of-the-art verifier on this problem (i.e., α−β-CROWN) for verification at test time. Additionally, we would also like to clarify that Lyapunov (asymptotic) stability (with a guarantee on convergence towards the equilibrium under an infinite time horizon) is different from reachability (with finite time) handled by some tools such as Sherlock, Polar-Express, etc.

We thank the reviewer for acknowledging our rebuttal. We agree that this is a promising direction and we will continue investigating the certified training with training-time branch-and-bound direction and its broader applications in our future research. However, we believe that we have already addresssed the weakness points raised in the initial review. We do acknowledge that this work has limitations which, however, are common limitations which exist in other papers recently published in similar venues (the focus on Lyapunov stability and the limitation to relatively low-dimensional systems are common in previous works including Wu et al., 2023 in NeurIPS 2023 and Yang et al., 2024 in ICML 2024). Therefore, we would like to gentlely request the reviewer to reconsider your rating. Thanks.