SEEV: Synthesis with Efficient Exact Verification for ReLU Neural Barrier Functions

We thank the reviewer for suggesting R1 and R2. The branch-and-bound methods for neural network verification perform branch and bound on non-linear units, either in the propagation of spatial data structures as mentioned in R1, or bound propagation as done in R2. In these works, being able to verify in the decision space of size potentially up to $2^n$ (where $n$ is the number of activation units) is done through analyzing and taking advantage of the intrinsic structure of neural networks, thus quickly pruning out large infeasible combinations to achieve verifiability. In our work, once we have identified at least one point that belongs to the border of region $\mathcal{D}$, we exploit the fact that the border region is connected and we quickly expand from this point to identify the entire border region, without the need to make decisions using branch and bound. In other words, we took advantage of the intrinsic structure of the control barrier function to quickly eliminate the need to search in regions that do not contain the border, as an analogy to how branch-and-bound methods in NN verification can prune out unnecessary search space in neuron space.

We also make the distinction that R1 and R2 are primarily concerned with verifying input and output relationships of neural networks, whereas the verification conditions in Proposition 1 involve nonlinear dynamical systems, which add another layer of complexity on top of NN verification problems.

Safe action can be derived from a control barrier function as a safety filter as described in [1] and [2]. In particular, one may solve the following optimization:

The solution to this optimization problem provides a control $u$ that minimally deviates from the nominal control $\pi_{nom}(x)$, while satisfying the descent condition defined by the control barrier function $B(x)$ in the constraint.

There is no limit on how to choose the control action filtered by the control barrier function, as a correct control barrier function forms a forward invariant set to ensure the safety of the system it describes.

[1] Ames, Aaron, et al. Control Barrier Functions: Theory and Applications. 17th European Control Conference, ECC 2019, Naples, Italy, June 25-28, 2019, 3420–3431.

[2] So, Oswin, et al. How to Train Your Neural Control Barrier Function: Learning Safety Filters for Complex Input-Constrained Systems. CoRR, abs/2310.15478.

We thank the reviewer for providing [1] and [2], and we will include a discussion about these works in the final submission. The reviewer is correct that verification-in-the-loop training is a known approach. The main contribution of this paper is to enhance the scalability of verification-in-the-loop training of NCBFs. We focus on a key bottleneck of existing verification-in-the-loop training methods, namely, the difficulty of performing verification and generating counterexamples in a computationally efficient manner. We make the following contributions in this direction: (i) algorithms for enumerating the boundary activation sets to be verified that leverage the topological properties of the safe region to reduce runtime; (ii) a hierarchical verification approach that first verifies tractable sufficient conditions and then checks exact conditions if no safety proofs or counterexamples can be found; and (iii) a novel regularizer that minimizes the number of activation sets at the boundary of the safe region, and thus incorporates efficient verification as one of the criteria for training the NCBF.

In Equation 8, the last two terms are widely used in the training of the NCBFs. The first term of Equation 8 encourages fewer linear hyperplanes along the boundary of the obtained NCBF. To do this, we need to penalize the dissimilarity of activation patterns in such regions. To make the computation of this dissimilarity differentiable with respect to the neural network's parameters, we introduced a modified sigmoid function, controlled by $k$, to perform the regularization. Figure 2 visualizes the effectiveness of this approach by showing the reduced variety of activation patterns of the trained neural network, and Table 1 quantitatively studies the number of boundary hyperplanes and the improved verification efficiency by employing this approach.

We further performed an ablation study on the hyperparameter $k$, which can be found in the supplemental PDF. According to this study, we note that the training performance is robust in the choice of $k$, as long as it is not too large to lead to gradient explosion during the backpropagation stage of training the neural network.

We will clarify Section 4 by adding an initial figure, as shown in the supplemental PDF, to describe the components of our approach. We will also add detailed descriptions of the algorithms (Appendix A.4) and the optimization problems (Appendices A.5 and A.6).

The reviewer is correct that it is difficult to directly compute exact solutions for the optimization problems for hyperplane and hinge verification, while conservative sufficient conditions may be more efficient but inexact. Our approach takes advantage of both methods by first attempting to verify safety using sufficient conditions. If the sufficient conditions are not satisfied, then we check safety using the exact conditions. In our evaluation of Spacecraft Rendezvous, we found that around 95% of the hinges can be verified with sufficient conditions, spending 5.9s (66% of hinge verification time), and the remaining 5% of hinges take 3.0s (34% of hinge verification time) when the sufficient conditions fail. Hence, in practice, our approach achieves exact verification with reduced computation time.

A comparison of the present paper with [15] is as follows. We note that our paper considers both the synthesis and verification of neural CBFs (NCBFs), while [15] only considered the verification problem. Moreover, while our approach verifies the exact conditions developed in [15], we greatly enhance scalability via the following novel technical contributions: (i) Instead of relying on off-the-shelf tools such as Linear Relaxation Based Perturbation Analysis (LiRPA) to enumerate the activation sets at the boundary of the safe region, we develop an enumeration algorithm that leverages the connectivity properties of the safe region to reduce runtime while maintaining the completeness of the enumeration; (ii) We propose a hierarchical verification approach in which novel tractable sufficient conditions are verified first, and the more complex exact conditions of [15] are only checked if the sufficient conditions fail; and (iii) We propose a new regularizer for training the NCBF that attempts to minimize the number of activation sets at the boundary, and hence minimizes the number of nonlinear programs that must be solved by the verifier. As shown in Table 1 of the paper, this regularizer reduced the number of boundary activation sets from 6,371 to 627 for a six-dimensional system (a reduction of over 90%). Our approach can be interpreted as introducing verification time as a criterion during NN training, and it could be of use in other NN applications.

Related to the comparison with [15], we emphasize that our approach is not conservative. It has the same exactness guarantees and is guaranteed to return the same value as [15]. While we utilize conservative over-approximations as a first step in the verification, the exact algorithms are used whenever the conservative over-approximations fail to return a conclusive result, i.e., either a proof of safety or a safety counterexample. We will revise the paper to make this point clear.

Thus, our paper utilizes over-approximations only as the first stage in the hierarchical pipeline to improve efficiency -- our verification checks easier problems and then solves harder problems if necessary. The final verification result is both sound and complete as the hinge enumeration and verification step solves the exact verification problem.

We will revise the paper to remove the overloaded notation $\mathbf{S}$. A collection of activation sets $\mathbf{S_1},\ldots,\mathbf{S_r}$ is complete if, for any $\mathbf{S}^{\prime} \notin \{\mathbf{S_1},\ldots,\mathbf{S_r}\}$, we have $\overline{\mathcal{X}}(\mathbf{S_1}) \cap \cdots \cap \overline{\mathcal{X}}(\mathbf{S_r}) \cap \overline{\mathcal{X}}(\mathbf{S}^{\prime}) = \emptyset$. We will add this definition to the statement of Proposition 1.

We clarify Problem 1 and Proposition 1 as follows. The set $\mathcal{D} = \{x: b(x) \geq 0\}$, where $b$ is the NCBF to be trained, while the set $\mathcal{C}$ is the given safety constraint. Proposition 1 ensures that $\mathcal{D}$ is positive invariant and $\mathcal{D}$ is contained in $\mathcal{C}$. This condition is weaker than the positive invariance of $\mathcal{C}$, since there may exist $x_0 \in \mathcal{C} \setminus \mathcal{D}$ such that $x(t) \notin \mathcal{C}$ for some $t \geq t_{0}$ when $x(t_0) = x_0$. Since $\mathcal{C}$ is given a priori, it is generally not possible to guarantee the positive invariance of $\mathcal{C}$. We will elaborate on this point in the text of the paper after Proposition 1.

The synthesis of a safe control policy for a given NCBF $b$ is discussed in [15] and is omitted from our paper due to space constraints. When $x(t)$ is in the interior of an activation region $\overline{\mathcal{X}}(\mathbf{S})$, the gradient $\frac{\partial b}{\partial x}$ is well-defined and any control input $u \in \mathcal{U}$ satisfying $\frac{\partial b}{\partial x}(f(x(t))+g(x(t))u) \geq -\alpha(b(x(t))$ for some strictly increasing function $\alpha: \mathbb{R} \rightarrow \mathbb{R}$ with $\alpha(0) = 0$ will ensure safety. If $x(t)$ lies at the intersection of multiple activation regions $\overline{\mathcal{X}}(\mathbf{S_1}),\ldots,\overline{\mathcal{X}}(\mathbf{S_r})$, any control $u \in \mathcal{U}$ that satisfies $\overline{W}(\mathbf{S_i})^{T}(f(x(t))+g(x(t))u) \geq -\alpha(b(x))$ for some $i \in \{1,\ldots,r\}$ will ensure safety. We have added a description of how to choose the control policy to the appendix.

The reviewer is correct that our result involves multiple parameters, including the regularizer coefficients $\lambda_B$, $\lambda_f$, and $\lambda_c$, as well as the parameter $k$ used by the regularizer $L_{B}$. We have included ablation studies of these parameters in the supplemental PDF.

We thank the reviewer for the feedback regarding the paper presentation. We will improve the readability of the paper by adding an overview figure to Section 4, as shown in the supplemental PDF, and improving the clarity of the notations in the paper. Furthermore, we will move the definitions of the regularizers $\mathcal{L}_f$ and $\mathcal{L}_c$ to Section 3 of the paper. Although we will leave the optimization problem formulations (14)--(22) in the appendix due to space constraints, we will provide additional explanations (including derivations of Lipschitz-based relaxations) for each formulation.

The reviewer correctly points out that our approach, although falls back to expensive SMT/non-linear programs, greatly outperforms the algorithms directing employing them. Our hierarchical pipeline performs cheap sufficient condition checking to quickly reduce the need for solving expensive non-linear problems.

As for the question regarding the cost of solving nonlinear programs during enumeration, we first apologize for a confusion - there is a typo in the section title of A.5, which is supposed to be written "A.5 Linear Programs for Enumeration". The enumeration relies solely on linear programs. BoundaryLP in Eq. (14) is used to determine if S is on a boundary activation set. USLP in Eq. (15) checks if the neighboring hyperplane may contain the zero-level set, while HingeLP in Eq. (16) assesses whether the intersection of hyperplanes may contain the zero-level set. These linear programs can all be solved quickly. To further answer the reviewer's question about the cost of solving nonlinear programs during verification, we extend the discussion to "A.6 Nonlinear Programs for Verification". The hierarchical verification involves nonlinear programs for sufficient conditions in Eqs. (20) and (21), and exact conditions in Eqs. (19) and (22). Among these, Eq. (22) is the most challenging. However, the difficulty in solving Eq. (22) does not hinder the overall efficiency of the verification process due to the hierarchical design. In the Spacecraft Rendezvous case study, we observed that only 5% of hinge verifications are solved by Eq. (22), taking 3.0 seconds (34% of the hinge verification time).

We thank the reviewer for the suggestion of scaling up the approach using alpha-beta-CROWN and other NN verification tools. We first note that the referred paper [1] focuses on synthesizing a Lyapunov function, which is different from our contribution in efficient synthesis and verification of neural control barrier function. We will make sure to add the reference to it in the final version. We further note that, in the prior work [15] used as the baseline for our evaluation, NN verification tools such as Linear Relaxation Based Perturbation Analysis (LiRPA) were used to enumerate activation sets at the boundary. Our proposed approach significantly reduces the runtime of this enumeration stage compared to this baseline. For example, in the obstacle avoidance case, [15] used 169.5s for enumeration, while our method used 20.6s. Moreover, unlike many of the existing NN verification works (including the recent work suggested by the reviewer), we consider a continuous-time problem setting. In continuous-time, the verification problem reduces to proving that, for any x with $b_{\theta}(x) = 0$, there exists control $u$ satisfying $\frac{\partial b_{\theta}}{\partial x}(f(x)+g(x)u) \geq 0.$ Hence, verifying safety in continuous time requires joint consideration of the reachable set of $b_{\theta}(x)$ as well as the gradient $\frac{\partial b_{\theta}}{\partial x}$, rendering many of the SOTA NN verification tools not directly applicable. We believe that generalizing such tools to our problem setting is a promising direction for future work and has the potential to further improve the scalability of the verification.

We plan to include a limitation paragraph in the final version of the paper that contains the points raised by the reviewer, including scalability to higher-dimensional systems and more complex NNs as well as generalization to non-ReLU activation functions.

[1] Yang, Lujie, et al. Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation for Efficient Synthesis and Verification. CoRR, abs/2404.07956.