Exact Verification of ReLU Neural Control Barrier Functions

Summary

This paper studies the exact conditions under which a learned CBF $b$ with ReLU activations yields the positive invariance property. Even though the set of inputs for which the CBF is non-differentiable has measure zero, the paper shows by example that safety can be still violated. This is because the slope of $b(x)$ can be discontinuous at the boundary $b(x) = 0$. To address this, the paper derives a theoretical result (Proposition 1) that provides a necessary and sufficient condition for a valid ReLU CBF. Based on this central result, the paper presents a verification algorithm that consists of state space discretization and search, activation set enumeration, and solving nonlinear programs. The experiments show faster safety verification for low-dimensional systems than SMT-based approaches.

Strengths

* ReLU is a popular activation function that is often used for constructing feedforward neural networks. The paper addresses the important theoretical problem of verifying learned CBFs with ReLU activations. * The paper provides a novel, central theoretical result (Proposition 1) that gives necessary and sufficient conditions for a given ReLU neural CBF to be valid. * As shown in Section 5, the proposed verification algorithm yields more efficient run-time than SMT-based approaches.

Weaknesses

* From a practical point of view, an engineer or a researcher can always choose a differentiable activation function to design a neural CBF, such as tanh or softplus. Then, the CBF remains differentiable. This leads to a motivational question of why we should use ReLU activations for modeling CBFs in the first place. Specifically, the proposed approach seems to possess several disadvantages compared to learning differentiable CBFs and verifying them. 1) The verification algorithm involves state-space discretization and activation set enumeration, both of which have inherent poor scalability with respect to the state-space dimensionality and the size of the neural network, respectively. In particular, the enumeration seems to suffer a lot as the network becomes complex, as observed in Table 2. 2) The online optimization problem for control (i.e. equation 10) requires solving possibly multiple quadratic programs, adding complexity to the standard CBF-QP. * The presentation can be improved so that mathematical descriptions are easier to follow. Especially, it is recommended that the paper 1) clearly define dimensionality of every vector and matrix-valued variables introduced in the paper, such as $W_i$, $W_{ij}$. 2) Define clearly any non-trivial variables in the main statement of mathematical results. For instance, the definition of $\bar{W}_0$ and $\bar{r}_0$ should be provided in the main statement of Lemma 1, not in the proofs in the appendix.

Questions

* What are the theoretical and practical advantages of using ReLU activations over differentiable activations (as done in [1], for example) for modeling neural CBFs? * Shouldn't the last formula in the proof of Lemma 1 use $W_{Lj}$, not $W_{ij}$? [1] Dawson, Charles, Zengyi Qin, Sicun Gao, and Chuchu Fan. "Safe nonlinear control using robust neural lyapunov-barrier functions." In Conference on Robot Learning, pp. 1724-1735. PMLR, 2022.

Rating

6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, 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

2 fair

Contribution

2 fair

Limitations

* The most concerning limitation is the scalability of the verification method. Even if the state space has a low-dimensionality, the usage of more layers or neurons can lead to combinatorial explosion of the runtime complexity.

Summary

Neural control barrier functions offer wider expressive power but do not satisfy the continuously differentiable assumption with ReLU activation functions. In this paper, the authors propose a method to verify that a neural ReLU CBF is a valid CBF and is hence capable of rendering a set forward-invariant. This method derives its foundations by extending the conditions of Nagumo’s theorem. These observations provide a set of necessary and sufficient conditions for verification. Algorithmically, these conditions are verified by a combination of linear relaxation to do a coarse analysis followed by interval bound propagation to fine-tune the regions of violation. Then, two non-linear programs are used to check for the CBF conditions. The final verification engine runs faster than existing SMT methods and works correctly on three benchmarks: Darboux, Obstacle avoidance and Spacecraft.

Strengths

The theoretical conditions for verification and the proposed algorithm are novel, principled, creative and non-trivial. Previous works typically gloss over the points of non-differentiability in energy functions such as CLF/CBF. Hence, I believe this is an important contribution which can be extended further in future work.

Weaknesses

1) The presentation needs to be improved and there are several minor mistakes which put off the reader. Line 243 - missing reference, Line 181 - mistake in the definition of complete collection, Line 439 - What definition of distance is used in the definition of tangent cone?, Multiple typos in Lemma 5 in appendix 2) If the set of non-differentiable points has measure zero, it will not actually affect the practical safety filtering application as the system can shoot through those points. 3) For the experiments section, it would be interesting to also plot the points of non-differentiability in figure 2. The current result comparing to improperly trained CBF is rather expected. Showing the enhancement of safety verification/safety filtering by virtue of considering non-differentiable points will enhance the contribution.

Questions

1) In proposition 1, equation (11), is the set difference explicitly needed given that the collection of sets $\{ S_1, \dots, S_r \}$ is defined as complete. 2) What is the meaning of equation (15) in line 186? Why can that not just be written as $\mathcal{D} \subset \mathcal{C}$ ? 3) For the procedure discussed in figure 1, I did not find a lot of background material in the appendix on exactly how IBP is used to enumerate activated sets and which linear program is used for pruning. I recommend a discussion on this in greater detail in the Appendix similar to Section 7.7 for the non-linear program. This is the phase that is seen to be time-consuming from Table 2 and needs to be justified.

Rating

6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.

Confidence

4: You are confident in your assessment, but not absolutely certain. It is unlikely, but not impossible, that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work.

Soundness

3 good

Presentation

2 fair

Contribution

3 good

Limitations

The societal impact of this work is likely positive. Limitations on the scalability of the approach to higher dimensional systems and deeper networks is discussed.

Summary

The authors consider the problem of synthesising control barrier functions parametrised as ReLU neural networks for non-linear deterministic dynamical systems. The authors first extend standard approaches for synthesising control barrier functions to the case where the barrier function is non-differentiable in a zero-measure set. Then, they encode the synthesis of a neural control barrier function as a nonlinear optimisation problem and illustrate the effectiveness of the approach on three benchmarks

Strengths

- The theory is sound and the extension of standard results for synthesizing control barrier functions to non-differentiable barriers is surely of interest - Paper is overall well written and the problem considered of interest

Weaknesses

- The main weakness is the scalability of the approach wrt the complexity of the neural barrier function. While I acknowledge that the algorithm is superior in terms of scalability than SMT based approaches, still experimental results are limited to neural networks of 1 hidden layer and 20 neurons at most - Some of the statements in the related works are not precise. In fact, the authors claim that it is not possible to use convex programming to synthesize/verify neural barrier functions. This is not accurate, in fact recent approaches rely on piecewise linear uncertain relaxations of neural networks to encode the problem of verifying neural barrier functions using linear programming [Mathiesen, Frederik Baymler, et al. "Safety certification for stochastic systems via neural barrier functions." IEEE Control Systems Letters 7 (2022): 973-978.] or SDP [Mazouz, Rayan, et al. "Safety guarantees for neural network dynamic systems via stochastic barrier functions." Advances in Neural Information Processing Systems 35 (2022): 9672-9686.]. Of course, the resulting approach will be more conservative compared to the one proposed by the authors, but more scalable. Also, please expand the discussion of why approaches employed to synthesize neural Lyapunov functions, e.g. [Abate, Alessandro, et al. "Formal synthesis of Lyapunov neural networks." IEEE Control Systems Letters 5.3 (2020): 773-778], cannot be employed in the setting of this paper - To demonstrate the importance of using neural control barrier functions, I believe that in the experiments there should be at least one experiment where the authors compare with the standard approaches commonly employed to synthesise control barrier functions, e.g. parametrising them as a SoS polynomial. This should serve to empirically demonstrate the advantages in being able to make use of the flexibility of neural networks in the context of barrier functions.

Questions

Please, see Weaknesses Section and in addition consider the following points: - Equation (7) and (8) quantifies over pairs $(i, j)$ of the set $\mathbf{T}(x) \cap \mathbf{S}$. However, $\mathbf{T}(x)$ is the set of unstable neurons produced by input $x$, hence it is unclear what pairs the quantification is referring to. Is it any two unstable neurons in the set $\mathbf{T}(x) \cap \mathbf{S}$? - Set $\bar{\mathcal{X}}(\mathbf{S})$ is defined both inside Lemma 1 and right after the Lemma. Please, be consistent

Rating

6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, 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

2 fair

Limitations

Please, see Weaknesses Section

Summary

In this paper, the authors present a new strategy for verifying neural control barrier functions (NCBFs) to ensure safe control of nonlinear systems. Specifically, the authors address the challenge posed by NCBFs when ReLU activation functions are employed. This renders existing verification strategies inapplicable due to the non-differentiability of resulting NCBFs. The authors tackle this issue by introducing conditions for a ReLU NCBF to satisfy \emph{positive invariance}, which forms the basis for constructing safe control policies. The proposed verification algorithm enumerates \emph{activation sets} and individually verifies their positive invariance defined based on the positivity of the activation outputs. The paper demonstrates the effectiveness of the proposed approach by comparing it with Satisfiability Modulo Theory (SMT) based methods across three control problems.

Strengths

- The paper contributes to the field by introducing a new verification algorithm and control strategies that apply to NCBFs using ReLU activation functions. Existing verification approaches are not directly applicable, and the authors address this limitation by introducing a new characterization of active sets and a corresponding verification algorithm. This approach has the potential to broaden the application domain of neural control barrier functions. - The paper appears to be technically sound.

Weaknesses

- While the comparison with SMT-based methods is informative, it would be beneficial to include a more comprehensive performance evaluation of ReLU NCBFs against classical NCBFs with differentiable activations, such as sigmoid. Assessing factors like NCBF training time, verification time, and the expressive capabilities of the resulting NCBFs in real-world control problems would add depth to the analysis. If ReLU NCBFs consistently outperform sigmoid NCBFs, the proposed verification strategy's utility would be significantly enhanced. - The authors could provide a thorough analysis of the time complexity of the proposed verification strategy. As the algorithm discretizes the state space into hyper-cubes and calculates corresponding bounds of $b(x)$ individually, it is important to understand how the complexity scales in high-dimensional problems. Also, the authors should provide experiments on more complex, potentially higher-dimensional control problems. - (Minor) the manuscript contains several typos that require careful proofreading.

Questions

N/A

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

The authors should consider the possibility of clearly outlining the limitations of their study and potential negative societal impacts. After the rebuttal phase (the same as the post-rebuttal comments): I thank the authors for their response and conducting the additional experiments. The majority of the concerns raised in my initial evaluation have been effectively attended to. While I acknowledge the efforts undertaken by the authors to conduct an additional round of experiments, I still have reservations about how well the proposed algorithm would work for problems with high dimensions. The additional experiments provided are still confined to low-dimensional scenarios. I recommend that the authors explore this aspect in their future research endeavors.

Summary

The paper proposes a technique to verify the safety of NCBF-based control policies. Usually, the verification depends on the CBF to be continuously differentiable. This is not the case for NNs, however using NCBFs is beneficial as it allows to encode more complex safety constraints. Their approach identifies the piecewise linear segments of the NCBF. The number of segments is reduced by only focusing on those at the boundary of the safe region. The remaining linear segments are overapproximized and verified using nonlinear programs. The authors compare their proposed technique with SOTA SMT based methods and demonstrate that they are able to verify NCBFs that previously resulted in a timeout.

Strengths

The paper propose a new original technique to prove the safety of NCBFs. The authors do a good job of motivating their new approach by demonstrating the shortcoming of techniques that expect $b$ to be continuously differentiable. The paper is mostly clear in its explanation and formulas, and gives intuitive explanations for many of them. In their experimental evaluation, they use one benchmark to compare their performance against two other SOTA techniques, and demonstrate that they are able to verify instances that would otherwise lead to a timeout. This indicates the significance of their proposed technique, should the results carry over to other benchmarks.

Weaknesses

The equations in the paper get increasingly complicated to follow, even with the provided explanations. Especially Lemma 4 is hard to follow. In the experimental evaluation, the paper would strongly benefit from exploring more benchmarks. The comparison to SOTA techniques dReal and Z3 is limited to one benchmark, with two more benchmarks that do not include a comparison to those tools. Also, a comparison to an approach based on neural-network-verification (e.g. "A Hybrid Partitioning Strategy for Backward Reachability of Neural Feedback Loops" by Nicholas Rober, Michael Everett, Songan Zhang, and Jonathan P. How) would help to demonstrate that the proposed technique can solve previously hard problems.

Questions

Main question: Why can't one use regular verification of safety properties of neural networks? If $D$ is convex (or can be split into a reasonable number of convex subsets), then one could verify that no input in $D$ is mapped to an output outside of $D$. When $f$, $g$ and $\\mu$ in Equation 1 are known, that equation could most probably be encoded as a NNs, so all common tools (compare e.g. VNN-COMP 2022 or 2023) should be able to verify this (or time out). You state the main benefit of your approach is that it does not depend on the specific choice of $\\mu$ (line 288). However, I do not know if this is often a requirement. If $\\mu$ changes, the verification using a technique that depends on $\\mu$ could be repeated. Did you do an experimental comparison of your approach with a NN-Verification-Tool-based approach to see how costly this would be? Other questions: 1) In the text above Proposition 1, is $\\overline{X}(S_1) \\cap \\ldots \\cap \\overline{X}(S_r) \\cap S'$ well-defined? $\\overline{X}(S)$ is a set of inputs $x$, but $S'$ is a set of neurons. Should this be $\\overline{X}(S')$? 2) In Equation 11, is the term to the right of $ \\textbackslash $ obsolete? If $\\{S_1, \ldots, S_r\\}$ is complete, then no input that activates all of $\\{S_1, \ldots, S_r\\}$ also activates any other $S'$ (based on the text above Proposition 1). So what is removed by the term right of $ \\textbackslash $ ? 3) What's the significance of the three different lines in Figure 2? They represent different "set boundaries", bu I do not know what that visualization achieves compared to one with just set boundary 0 Minor: What is the missing reference in line 243? Minor note: Line 268: "with in" -> "within"

Rating

6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, 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 authors do not provide a list of limitations or potential negative societal impact. However, the potential negative societal impact is probably small, as this technique is developed to increase the provable safety of NCBFs. So the potential negative societal impact is identical to that of any AI-based technology. The paper would benefit from a description of the limitations of their proposed approach.

Acknowledgement

Thank you for your convincing response. The additional experiments are interesting in that the ReLU activation results in faster learning and verification than other commonly-used functions, such as tanh. This indeed motivates the use for ReLU activations for NCBFs. Based on Table 2 and 3 in the new PDF, it seems that the proposed algorithm has better scalability than existing methods, which is an encouraging result. Thank you also for clarifying the condition under which the worst-case solve time for QP occurs.

Read author response

I have read the author's response to my comments. The response is convincing. Further, additional supplementary experiments have been provided to show that ReLU activations are more beneficial and can potentially give a larger RoA. These results are encouraging. The only concern that remains for me are the tractable relaxations for verification that have recently come to my knowledge through the other reviewers.

Response to Rebuttal

I thank the authors for the rebuttal and the additional experiments, which clarified some of my doubt and the contributions. Consequently, I increase my score to weak accept. - We will also add a sentence to the second paragraph of the related work that reads “Piecewise linear approximations of ReLU neural networks have been used to develop tractable safety verification algorithms using linear and SOS programming. This approach leads to sound and incomplete verification algorithms, whereas the present paper proposes exact verification algorithms. Moreover, these existing works apply to discrete-time systems with a priori given controllers. I would put the emphasis especially on the fact that you focus on exact verification algorithms, while these relaxations will only produce sound and incomplete results and they have only be applied for discrete-time systems. In fact, controller synthesis for these alternative approaches has been considered, see e.g., Section 5 in [Mazouz, Rayan, et al. "Safety guarantees for neural network dynamic systems via stochastic barrier functions." Advances in Neural Information Processing Systems 35 (2022): 9672-9686.]

Response to rebuttal

I thank the authors for their response and conducting the additional experiments. The majority of the concerns raised in my initial evaluation have been effectively attended to. While I acknowledge the efforts undertaken by the authors to conduct an additional round of experiments, I still have reservations about how well the proposed algorithm would work for problems with high dimensions. The additional experiments provided are still confined to low-dimensional scenarios. I recommend that the authors explore this aspect in their future research endeavors.