On Choice of Loss Functions For Neural Control Barrier Certificates

Q6. Any intuition for Theorem 8? It's just math proofs there, and it's a bit hard for readers to digest.

A6. The intuition behind Assumption 7 and Theorem 8 lies in leveraging Lipschitz continuity to provide formal guarantees. Since neural networks are trained on a finite set of data points, it is crucial to establish out-of-sample performance guarantees to ensure overall correctness

Lipschitz continuity enables us to extend guarantees from a finite set of training data to the entire state set. Assumption 7 serves as a condition that facilitates this extension. Specifically, it ensures that if a sample point (used during training) satisfies the control barrier certificate conditions, then all points within a neighborhood centered at the sample point with radius $\frac{\epsilon}{2}$ also satisfy those conditions. This approach forms the theoretical foundation needed to bridge the gap between finite data and overall correctness across the entire state set.

Q7. The verification relies heavily on Lipschitz constants, the upper/lower bounds. From my experience, this Lipschitz bound is usually extremely loose, especially when the input region is not small. Did the authors encounter this issue?

A7. While the trivial upper bound of the Lipschitz constant is indeed loose, we employ the approach outlined in "Lipschitz Certificates for Layered Network Structures Driven by Averaged Activation Operators," SIAM Journal on Mathematics of Data Science, by Combettes and Pesquet, which provides considerably tighter bounds than the trivial upper bound.

We have included the Lipschitz constants of our control barrier certificates in Sections $5.2$ and $5.3$. For the inverted pendulum case study, we obtained $\mathcal{L}_B = 0.47$ and $\mathcal{L}_k = 2.3$ as the Lipschitz constants of the barrier certificate and its corresponding controller, respectively. For the double inverted pendulum case study, we obtained $\mathcal{L}_B = 0.17$ and $\mathcal{L}_k = 1.8$ for the barrier certificate and its corresponding controller, respectively.

Q8. What do sections 5.3 and 5.4 mean? Is it to pick an inverted pendulum as an illustration example?

A8. Yes, Sections 5.3 and 5.4 focus on the two most challenging case studies. Additional details about the other four systems are provided in the appendix.

Q9. The experiment settings in Section 5.2 miss many hyperparameters, the code only contains the pendulum examples.

A9. We did our best to include all hyperparameters (such as Lipschitz constants, $\epsilon$, and $\eta$) in their corresponding subsections. However, it is certainly possible that we may have missed some. Could the reviewer please specify which hyperparameters they believe were omitted?

We sincerely thank the reviewer for their detailed analysis and thoughtful feedback on our method. We appreciate the time and effort you have dedicated to reviewing our paper and will incorporate your suggestions to enhance its clarity and quality.

We kindly request that you re-evaluate our paper in light of the clarifications and additional insights we have provided.

Sincerely,

Authors

We are grateful for the reviewer’s constructive suggestions and provide our responses below.

Q1. The primary contribution is the replacement of the ReLU loss with Mean Squared Error (MSE) for smoother convergence in Neural Control Barrier Certificates (NCBCs). The novelty is low.

A1. While we agree that replacing the ReLU loss with MSE loss is one of the key contributions of this paper, we believe the work includes other significant novelties in obtaining neural control barrier certificates. For instance, a major contribution is the use of the implication (1):

$

(B(x) \leq \gamma) \implies (B(f(x, k(x))) \leq -\eta)

$

in place of the traditional inequality (2):

$

B(f(x, k(x))) - B(x) \leq -\eta

$

in the third condition of the barrier certificate. This approach is encoded in the neural barrier certificate with MSE loss while still providing formal guarantees.

We note that the implication (1) is significantly less conservative than the traditional inequality $B(f(x, k(x))) - B(x) \leq -\eta$. The latter requires the system’s evolution to be decreasing with respect to the barrier across the set $\mathcal{X} \setminus \mathcal{X}_u$ , even though some of these states might not be reachable from the initial set. In contrast, our implication relaxes the inequality in two key ways:

For non-reachable states satisfying $B(x) > \gamma$, the implication (1) holds trivially, and such states do not impact training. \item Even for reachable states, i.e., states satisfying $B(x)\leq \gamma$ , the implication (1) is a weaker condition than the traditional condition (2).

For more details on the implementation of this implication, we refer the reviewer to Assumption 7 (validity conditions) and Theorem 8.

Furthermore, we have rigorously demonstrated that using MSE loss instead of ReLU loss leads to several critical theoretical results regarding the convergence and stability of training.

Additionally, our extensive numerical experiments indicate that, when using MSE loss, both the barrier certificates and controllers exhibit smaller Lipschitz constants compared to those obtained with ReLU loss. This suggests that training with MSE is less data-intensive than training with ReLU loss.

Q2. Algorithm 1 is very confusing and not well-written. B3 = B? What is B3 and why?

A2. The term $B_3 = B$ is included to address the moving target problem, as mentioned in the paper. By fixing the weights of the barrier certificate while training the controller, we ensure that the target we aim to achieve does not "move." For more details on the moving target problem, we refer the reviewer to Mnih et al., "Human-level control through deep reinforcement learning," Nature, 2015. We will add more elaboration on the issue of the moving target problem in the revised version to clearly motivate the use of $B_3 = B$.

Q3. The presentation is poor.

A3. We have revised the draft and addressed comments from other reviewers to improve clarity. We would greatly appreciate it if the reviewer could provide more specific feedback on why the presentation is considered poor, so we can address these concerns more effectively in the revised version.

Q4. the algorithm relies heavily on Lipschitz constants (isn't that loose?)

A4. If one chooses not to use Lipschitz continuity, the only alternative, to the best of our knowledge, is to employ SMT solvers or MILP optimization to provide formal guarantees. However, these methods require an exact mathematical model of the system and suffer from exponential complexity as the number of neurons in the neural network increases. This challenge is particularly significant for over-parameterized networks, which we use in our experiments due to their desirable universal approximation capabilities. We refer the reviewer to Hornik’s work, “Approximation Capabilities of Multilayer Feedforward Networks," Neural Networks, 1991. As demonstrated in our experiments, SMT solvers fail to provide solutions within a reasonable time frame when applied to over-parameterized networks.

While the trivial upper bound of the Lipschitz constant is indeed loose, we employ the approach outlined in "Lipschitz Certificates for Layered Network Structures Driven by Averaged Activation Operators," SIAM Journal on Mathematics of Data Science, by Combettes and Pesquet. This approach provides considerably tighter bounds than the trivial upper bound.

Q5. the attached code only includes the pendulum examples.

A5. We have included all case studies in the final submission.

I have read the authors' response.

We appreciate the reviewer’s constructive suggestions, which have helped improve our paper. We have included all experiments in the attached code.

If you have any further questions or concerns, please feel free to reach out.

Q6. Also, these systems are small enough that there are analytically-determined barrier functions for at least some of them. How do the computational results compare?

A6. We agree with the reviewer that some of our case studies involve relatively small systems. However, these examples were adopted from the literature to allow for direct comparisons. To further demonstrate the advantages of our algorithm, we introduced a new system—the double inverted pendulum—where all previous methods fail to find a control barrier certificate, even when assuming access to the exact mathematical model of the system.

Q7. Finally, how is eta chosen, and is it decreased over the course of training?

A7. Regarding $\eta$, it is a design parameter; however, based on our experiments, it does not play a critical role in training since any admissible $\eta$ provides sufficient conditions for safety. The value of $\eta$ depends on several factors, including the system, the geometry of the initial and unsafe regions, the distance between these sets, and the parameters of the neural networks. Generally, larger values of $\eta$ make it easier to satisfy conditions (14)-(15) with a larger quantization parameter for data collection.

Our algorithm computes $\eta$ at each iteration, and training concludes once it meets the admissibility criteria, specifically the validity conditions outlined in Assumption 7.

We sincerely thank the reviewer for their detailed analysis and thoughtful feedback on our method. We appreciate the time and effort you have dedicated to reviewing our paper and will incorporate your suggestions to enhance its clarity and quality.

We kindly request that you re-evaluate our paper in light of the clarifications and additional insights we have provided.

Sincerely,

Authors

We are grateful for the reviewer’s constructive suggestions and provide our responses below.

Q1. The gridding of the state space into Lipschitz-constant-dependent neighborhoods of training points is a potential downside of this approach -- it seems that it could limit the scalability and remove some of the benefits of using a barrier function. Could the authors include discussion (beyond the examples shown) of how the training scales with the dimension of the dynamic system, as the number of training points is exponential in this dimension.

A1. We acknowledge the reviewer’s observation that sample complexity is exponential. However, computational complexity is a common challenge for data-driven methods that provide formal guarantees, and this issue is not unique to our approach. To further illustrate this point, here are some examples:

Ansaripour et al., "Learning provably stabilizing neural controllers for discrete-time stochastic systems," ATVA 2023.

Mathiesen et al., "Safety Certification for Stochastic Systems via Neural Barrier Functions," LCSS 2022.

Ehlers, "Formal verification of piece-wise linear feed-forward neural network," ATVA 2017.

Elboher et al., "An abstraction-based framework for neural network verification," CAV 2020.

Katz et al., "Reluplex: An efficient SMT solver for verifying deep neural networks," CAV 2017.

Chang et al., "Neural Lyapunov Control," NeurIPS 2019.

Zhao et al.,"Synthesizing barrier certificates using neural networks," HSCC 2020.

Zhang et al., "Exact Verification of ReLU Neural Control Barrier Functions," NeurIPS 2024.

Even assuming the availability of the system's model, we attempted prior methods using Sum of Squares (SOS) optimization techniques but were unsuccessful in finding polynomials (up to degree 15) for the double inverted pendulum case study, ultimately leading us to abandon increasing the degree of the polynomials further.

That said, we believe our proposed method remains more efficient than many model-based techniques, as evidenced by our experimental results.

Q2. The presentation of the paper is quite poor. First, the paper presents results using a discrete time control system, whereas the original work on which CBCs (Prajna) are based is presented for continuous systems. This should be clarified and that the results carry over directly should be confirmed. Second, the ReLU(.,.) and MSE(.,.) functions are not defined. In Alg 1 L_{MSE} references L_i functions in equations (7)-(9) that do not exist. Lipschitz continuity of neural networks is not defined. There are small typos throughout the paper.

A2. The reviewer is correct. We have added a citation to the following paper, which defines control barrier certificates for discrete-time systems (setting $k=1$):

Anand et al., “K-inductive barrier certificates for stochastic systems,” HSCC 2022.

Furthermore, we have addressed the reviewer’s concerns by providing clear definitions for the ReLU and MSE functions, correcting references in Algorithm 1, and resolving minor typographical errors throughout the paper.

Q3. There is not much physical intuition given in the paper: why are the inverted pendula examples harder to verify?

A3. Both examples are nonlinear systems that must ensure safety around their unstable equilibrium points.

Q4. Why is the inverted pendulum example not symmetric wrt theta and thetadot?

A4. We have adopted the inverted pendulum from the following state-of-the-art papers:

Edwards et al., "Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models," HSCC 2024.

Anand and Zamani, "Formally Verified Neural Network Control Barrier Certificates for Unknown Systems," IFAC 2023.

Chang et al., "Neural Lyapunov Control," NeurIPS 2019.

The model of the double inverted pendulum was derived using the Euler-Lagrange equations, as outlined in the Appendix A.1 of "Course Notes for MIT 6.832" by Tedrake.

Q5. What is the dependence on the network architecture, and how were the specific architectures used in the examples chosen?

A5. The universal approximation capability of a neural network relies on it being over-parameterized, i.e., sufficiently deep and wide. We refer the reviewer to Hornik’s work, "Approximation Capabilities of Multilayer Feedforward Networks," Neural Networks, 1991. Based on this, we chose an architecture with 4 hidden layers, each containing 200 neurons heuristically.

With the rebuttal deadline approaching today, we kindly remind the reviewer to review our response to your comments.

If any clarifications or additional details are needed to assist with your review, please feel free to let us know.

Thank you for your time and valuable feedback.

We are grateful for the reviewer’s constructive suggestions and provide our responses below.

Q1. Are the authors using the spectral norm bounds for Lipschitz constants and then derive certificates based on that? Have the authors considered more advanced methods for Lipschitz continuity?

A1. We would like to point out that our method is concerned with safety, and not stability.

Since we estimate the Lipschitz constant of two neural networks at each iteration during training, an efficient method for estimating it is crucial. We agree that there are other approaches in the literature that provide tighter bounds on the Lipschitz constant compared to Combettes and Pesquet, such as Fazlyab et al.,"Efficient and accurate estimation of Lipschitz constants for deep neural networks," NeurIPS 2019 and Pauli et al.,"Novel quadratic constraints for extending LipSDP beyond slope-restricted activation," ICLR 2024. However, these methods are computationally expensive. In fact, our numerical experiments suggest that approximately $99\\%$ of the training time is spent on calculating the Lipschitz constant, with only $1\\%$ dedicated to actual training.

Instead, we compute an upper bound of the Lipschitz constant using the spectral norm. For details, we refer the reviewer to "Lipschitz certificates for layered network structures driven by averaged activation operators," SIAM Journal on Mathematics of Data Science, by Combettes and Pesquet. The spectral norm approach offers a good trade-off: it provides a much tighter bound than the trivial upper bound while remaining efficient to compute.

We performed an a posteriori comparison between the spectral norm approach and the method proposed by Fazlyab et al. Our results show that the spectral norm approach is an order of magnitude faster than Fazlyab et al., while the upper bound it provides is only $40\\%$ to $50\\%$ larger than the upper bound obtained by Fazlyab. This finding aligns with the results reported in Fazlyab et al., particularly in Figure 2a.

Q2. Can the authors justify whether the MSE loss or the Lipschitz continuity lead to the improvements? Maybe some baselines that use advanced Lipschitz continuity properties without using MSE loss can be added for comparison?

A2. Justification for using MSE loss:

We would like to highlight that using MSE leads to several theoretical and numerical advantages.

As it is show in the literature, MSE loss has guarantees of convergence and optimality, see Cheridito et al.,"A proof of convergence for gradient descent in the training of artificial neural networks for constant target functions," Journal of Complexity, 2022.

Our extensive numerical experiments indicate that, when using MSE loss, both the barrier certificates and controllers exhibit smaller Lipschitz constants compared to those obtained with ReLU loss. This suggests that training with MSE is less data-intensive than training with ReLU loss, which is advantageous when scaling to larger problems.

Justification for using Lipschitz continuity:

If one chooses not to use Lipschitz continuity, the only alternative, to the best of our knowledge, is to employ SMT solvers or MILP optimization to provide formal guarantees. However, these methods require an exact mathematical model of the system and suffer from exponential complexity as the number of neurons in the neural network increases. This challenge is particularly significant for over-parameterized networks, which we use in our experiments due to their desirable universal approximation capabilities. We refer the reviewer to Hornik’s work, “Approximation Capabilities of Multilayer Feedforward Networks," Neural Networks, 1991. As demonstrated in our experiments, SMT solvers fail to provide solutions within a reasonable time frame when applied to over-parameterized networks.

Furthermore, Anand and Zamani in “Formally Verified Neural Network Control Barrier Certificates for Unknown Systems," IFAC 2023, utilize the approach proposed by Pauli et al., “Training Robust Neural Networks Using Lipschitz Bounds," LCSS 2021. We have compared our method to theirs, and as shown in Table 1 of our paper, our method demonstrates clear superiority in performance.

We sincerely thank the reviewer for their detailed analysis and thoughtful feedback on our method. We appreciate the time and effort you have dedicated to reviewing our paper and will incorporate your suggestions to enhance its clarity and quality.

We kindly request that you re-evaluate our paper in light of the clarifications and additional insights we have provided.

Sincerely,

Authors

With the rebuttal deadline approaching today, we kindly remind the reviewer to review our response to your comments.

If any clarifications or additional details are needed to assist with your review, please feel free to let us know.

Thank you for your time and valuable feedback.

Q6. Using spectral normalization to enforce the Lipschitz of B and k is quite conservative. Have you tried using more sophisticated Lipschitz parameterizations (see below)?

Pracht 2022: Almost-Orthogonal Layers for Efficient General-Purpose Lipschitz Networks Wang 2023: Direct Parameterization of Lipschitz-Bounded Deep Networks

A6. We do not utilize spectral normalization, nor do we enforce any constraints on the neural networks (other than small $l_1$ regularization).

Since we estimate the Lipschitz constant of the two neural networks at each iteration during training, an efficient method for this estimation is crucial. Existing methods, such as those proposed by Wang et al., are either computationally expensive or too restrictive. Furthermore, the method introduced by Pracht et al. is only applicable to linear neural networks.

We acknowledge that other approaches in the literature provide tighter bounds on the Lipschitz constant compared to Combettes and Pesquet, such as Fazlyab et al., "Efficient and accurate estimation of Lipschitz constants for deep neural networks," NeurIPS 2019, and Pauli et al., "Novel quadratic constraints for extending LipSDP beyond slope-restricted activation," ICLR 2024. However, these methods are computationally expensive. In fact, our numerical experiments indicate that approximately $99\\%$ of the training time is spent calculating the Lipschitz constant, with only$1\\%$ dedicated to actual training.

Instead, we compute an upper bound of the Lipschitz constant using the spectral norm. For details, we refer the reviewer to "Lipschitz certificates for layered network structures driven by averaged activation operators," SIAM Journal on Mathematics of Data Science, by Combettes and Pesquet. The spectral norm approach offers a good trade-off: it provides a much tighter bound than the trivial upper bound while remaining efficient to compute.

We performed an a posteriori comparison between the spectral norm approach and the method proposed by Fazlyab et al. Our results show that the spectral norm approach is an order of magnitude faster than Fazlyab et al., while the upper bound it provides is only $40\\%$ to $50\\%$ larger than the upper bound obtained by Fazlyab. This finding aligns with the results reported in Fazlyab et al., particularly in Figure 2a.

We sincerely thank the reviewer for their detailed analysis and thoughtful feedback on our method. We appreciate the time and effort you have dedicated to reviewing our paper and will incorporate your suggestions to enhance its clarity and quality.

We kindly request that you re-evaluate our paper in light of the clarifications and additional insights we have provided.

Sincerely,

Authors

Q4. I don’t totally understand the motivation of the MSE loss. The ReLU-type loss is meant to mimic a constraint and be active only when the constraint e.g. B(x) <= -\eta is not satisfied. However, it seems that MSE loss tends to push B(x) towards the boundary of the safe level set so that B(x) = -eta. It’s not clear how this will affect the overall landscape of the learned barrier function or why this is desirable besides smoothness of the loss. Typically a smooth performance objective is included in the loss anyways, which would end up competing adversarially with your CBC MSE loss.

A4. We observed that the MSE loss primarily pushes the initial set of states to $-\eta$ and the unsafe set to $\eta$, as these values are directly incorporated into the loss function.

We would like to emphasize that using MSE loss provides several theoretical and numerical advantages:

Convergence and Optimality Guarantees: As shown in the literature, MSE loss has established guarantees of convergence and optimality. For instance, Cheridito et al., in"A Proof of Convergence for Gradient Descent in the Training of Artificial Neural Networks for Constant Target Functions," Journal of Complexity, 2022, highlight its robustness in achieving these guarantees.

Numerical Benefits: Our extensive numerical experiments indicate that the barrier certificates and controllers trained using MSE loss exhibit smaller Lipschitz constants compared to those trained with ReLU loss. This suggests that training with MSE loss is less data-intensive, which is advantageous when scaling to larger problems.

Q5. The control problem formulation is kind of strange to me. Algorithm 1 certainly trains a controller to avoid the unsafe region, but what is the controller trying to achieve otherwise? Shouldn’t there be some performance objective such as stability to a fixed point or reaching a terminal set? The setting in the paper would make more sense to me if we are already given a controller and want to learn a barrier function B to certify its behavior rather than learning one from scratch. If a performance objective is added to the algorithm, it might be hard to trade-off that additional loss with your MSE which is always going to be non-zero if B is a continuous function.

A5. Our experiments show that while training a controller for safety, the system equipped with it tends to reach a fixed point, as demonstrated in our results. Performance objectives can be incorporated into the loss function; however, overly restrictive metrics may prevent convergence.

Moreover, achieving a zero loss is not necessary to establish formal guarantees, as we have outlined in our paper.

We are grateful for the reviewer’s constructive suggestions and provide our responses below.

Q1. The paper’s formulation and technical results are similar to that of Nejati 2023

A1. While the problem statements in our paper and Nejati (2023) share similarities, particularly in providing data-driven guarantees, there are significant differences in our approaches. Unlike Nejati (2023), which focuses solely on verification and does not employ neural networks, our method is designed for synthesis. Specifically, we leverage neural networks to represent control barrier functions and their corresponding controllers. Nejati (2023) relies on a fixed template for barrier functions and formulates the problem using a scenario convex program, resulting in probabilistic guarantees. In contrast, our framework ensures 100% correctness of the control barrier functions and their associated controllers, representing a fundamentally different approach.

Q2. The validity of the algorithm depends on obtaining valid upper-bounds for the Lipschitz constants L_x and L_u. This seems to be non-trivial unless they are known analytically.

A2. We agree with the reviewer that obtaining the Lipschitz constants is non-trivial. However, as mentioned in the paper, sampling-based techniques can be employed to estimate these constants, which is a well-studied field. Established methods include:

Strongin et al.,"Acceleration of global search by implementing dual estimates for Lipschitz constant," NUMTA 2019.

Novara et al., "Direct feedback control design for nonlinear systems," Automatica 2013.

Calliess et al., "Lazily adapted constant kinky inference for nonparametric regression and model-reference adaptive control," Automatica 2020.

Calliess, "Lipschitz optimisation for Lipschitz interpolation," ACC 2017.

González et al., "Batch Bayesian optimization via local penalization," Artificial intelligence and statistics, 2016.

Q3. The author’s claim that their method is more scalable to higher-dimensions. I will agree that it is scalable wrt to the network size, however I think there are significant scalability issues in state and control dimension in requiring an epsilon-net (Eq (6) on the state-space and and requiring sample-based estimates for Lipschitz constants $L_x$ and $L_u$. Often-times large networks aren’t required for direct state-feedback of 6-dimensional problems and more appropriate for perception-based controllers not currently supported by this framework.

A3. We agree with the reviewer’s point regarding the exponential sample complexity in requiring an $\epsilon$-net. As mentioned in the conclusion, our future work focuses on addressing this challenge by leveraging system properties such as monotonicity, mixed monotonicity, and compositionality techniques. It is important to note that sample complexity is a common challenge in methods providing formal guarantees and is not unique to our approach. To further illustrate this, here are some examples:

Ansaripour et al., "Learning provably stabilizing neural controllers for discrete-time stochastic systems," ATVA 2023.

Mathiesen et al., "Safety Certification for Stochastic Systems via Neural Barrier Functions," LCSS 2022.

Ehlers, "Formal verification of piece-wise linear feed-forward neural network," ATVA 2017.

Elboher et al., "An abstraction-based framework for neural network verification," CAV 2020.

Katz et al., "Reluplex: An efficient SMT solver for verifying deep neural networks," CAV 2017.

Chang et al., "Neural Lyapunov Control," NeurIPS 2019.

Zhao et al.,"Synthesizing barrier certificates using neural networks," HSCC 2020.

Zhang et al., "Exact Verification of ReLU Neural Control Barrier Functions," NeurIPS 2024.

Even assuming the availability of the system's model, we attempted prior methods using Sum of Squares (SOS) optimization techniques but were unsuccessful in finding polynomials (up to degree 15) for the double inverted pendulum case study, ultimately leading us to abandon increasing the degree of the polynomials further.

That said, we believe our proposed method is still more efficient than many model-based techniques, as demonstrated in our experiments.