Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation

Authors: hanjiang  hu
yujie  yang
tianhao  wei
changliu  liu
Venue: robot-learning_org_CoRL_2024_Conference
Published: 2024-06-06 03:36:00

Abstract: Control barrier functions (CBFs) are important in safety-critical systems and robot control applications. Neural networks have been used to parameterize and synthesize CBFs with bounded control input for complex systems. However, it is still challenging to verify pre-trained neural networks CBFs (neural CBFs) in an efficient symbolic manner. To this end, we propose a new efficient verification framework for ReLU-based neural CBFs through symbolic derivative bound propagation by combining the linearly bounded nonlinear dynamic system and the gradient bounds of neural CBFs. Specifically, with Heaviside step function form for derivatives of activation functions, we show that the symbolic bounds can be propagated through the inner product of neural CBF Jacobian and nonlinear system dynamics. Through extensive experiments on different robot dynamics, our results outperform the interval arithmetic-based baselines in verified rate and verification time along the CBF boundary, validating the effectiveness and efficiency of the proposed method with different model complexity. The code can be found at https://github.com/intelligent-control-lab/verify-neural-CBF.

Main paper: 
 introduction: 
 Safe control is of great importance in online decision making for robot learning through filtering out unsafe explorative actions [1, 2, 3, 4] , guaranteeing safety during sim-to-real transfer in a hierarchical manner [5] . As an effective tool of safe control, control barrier functions (CBFs) have been studied for years on both verification and synthesis [6, 7, 8, 9, 10] . A valid CBF guarantees safety by ensuring the function values non-positive for any states along the safe trajectory, implicitly enforcing the non-trivial forward invariance that feasible control inputs always exist to maintain the following non-positive energy values once the state is safe. To ensure forward invariance, polynomial-based CBFs have been proposed based on hand-crafted parametric functions [11, 12, 13] , which can be verified through algebraic geometry techniques like sum-of-squares (SOS) optimization [14, 15, 16] . However, polynomial-based CBFs cannot encode complicated safety constraints [17] , and the generic parameterization of non-conservative safe control for various nonlinear dynamics and nonconvex safety specifications is needed.Neural network parameterized CBFs (neural CBFs) have shown promising results due to their powerful expressiveness in modeling complex dynamics with bounded control inputs [18, 19, 20, 21, 22] . But it is challenging to guarantee that the learned neural CBF is valid because of its poor mathematical interpretability. One way to ensure the safety/stability of the dynamic system is to learn neural barrier/Lyapunov certificates [23, 24, 25, 26, 27, 28, 29] , but it may be too conservative and cause false negatives if the formal verification only relies on a specific control policy [17, 30] . Recent works to directly verify the forward invariance of learned neural CBFs are based on SMT-based counterexample falsification [31, 32] , mixed integer programming [33] , Lipschitz neural networks [34] , and CROWN-based linear bound propagation [35, 36, 37] . Although linear bound based verifi-8th Conference on Robot Learning (CoRL 2024), Munich, Germany. cation methods have shown promising scalability to larger neural networks [38, 39, 40] , the bounds do not have linear symbolic format when calculating the inner product of neural networks Jacobian and the nonlinear system dynamics [36] , which may be too loose and not efficient due to interval arithmetic.Therefore, we introduce an efficient incomplete verification framework for ReLU-based neural CBFs using the fully linear symbolic bound propagation w.r.t state by combining the gradient of CBFs and neural dynamics, as shown in Fig. 1 . By leveraging the fact that the derivative of ReLU activation function is the Heaviside step function, we show that linear symbolic bounds can be propagated through the inner product. Extensive experiments on various robot dynamic systems show that our method surpasses current state-of-the-art verification baselines in terms of verified rate and verification time along the CBF boundary. In summary, our contributions are listed below.• We propose a novel neural CBF verification framework using derivative bound propagation to efficiently establish symbolic bounds for verifying forward invariance.• We simplify the problem of propagating linear bounds through the inner product between neural CBF Jacobian and system dynamics.• Extensive experiments validate that our proposed method achieves a 20% higher verified rate with less total verification time to verify the boundary of neural CBFs compared to the baselines.2 Problem Formulation 
safe control with neural cbf: 
 Given a control-affine system ẋ = f (x) + g(x)u with state x ∈ X ⊂ R n and bounded control input u ∈ U ⊂ R m and user-specified safe set X 0 ⊆ X , neural control barrier function (neural CBFs) are defined as continuous and piecewise smooth functions ϕ : R n → R with neural network parameterization. Generally, the neural CBF consists of L feedforward layersy i : R ni-1 → R ni , i = 1, 2, . . . , L, associated with L -1 ReLU activation functions σ i : R ni → R ni , i = 1, 2, .. . , L -1 after each linear feedforward layer. Therefore, the neural CBF is formulated as the compositional function ϕ(x) = y L • σ L-1 • y L-1 • σ L-2 • y L-2 • • • • σ 1 • y 1 (x),wherey i : R ni-1 → R ni and n 0 = n, n L = 1. Furthermore, each feedforward layer y i is parame- terized with weight W i ∈ R ni×ni-1 and bias b i ∈ R ni as ẑi = y i (z i-1 ) = W i z i-1 + b i , where ẑi-1 ∈ R ni is the pre-activation output of y i and z i-1 ∈ R ni-1 is the output of last activation layer z i-1 = σ i-1 (ẑ i-1 ). A neural CBF parameterized with neural network θ is valid if the sublevel set X ϕ := {x ∈ X | ϕ θ (x)≤ 0} ⊆ X 0 satisfies forward invariance, as defined below. In the absence of ambiguity, we omit the subscript θ and directly use the notation ϕ to represent neural CBF.A set X ϕ is forward invariant if for state x(0) ∈ X ϕ at time t = 0, at any following time t > 0, there always exists control input u(t) ∈ U such that x(t) ∈ X ϕ according to ẋ = f (x) + g(x)u.By Nagumo theorem [41] , the forward invariance holds if the following boundary condition holds, Theorem 1 (from [11, 6] ). Given neural CBF ϕ, if the following boundary condition over boundary set∂X ϕ := {x ∈ X | ϕ(x) = 0} holds for the sublevel set X ϕ := {x ∈ X | ϕ(x) ≤ 0}, ∀x ∈ ∂X ϕ := {x ∈ X | ϕ(x) = 0}, ∃u ∈ U, s.t. φ(x, u) = ∇ x ϕ ⊤ (f (x) + g(x)u) ≤ 0, (1) then the sublevel set X ϕ = {x ∈ X | ϕ(x) ≤ 0} is forward invariant.Due to the universal representability of neural networks, neural CBFs have potential superiority in modeling complex forward invariant sets, showing that it is of great significance to verify that learned neural CBFs are valid.Given a pre-trained neural CBF ϕ, our goal is to formally verify that it is valid in two aspects. One is to ensure that the sublevel set X ϕ := {x ∈ X | ϕ(x) ≤ 0} is a valid subset of the user-specified safe set X 0 , and the other is to guarantee the forward invariance in Definition 1. Since the neural CBF can be bounded above by ϕ C = ϕ + C, C > 0 to shrink the forward invariance set into the user-specified safe set, without loss of generality, we reasonably assume that X ϕ := {x ∈ X | ϕ(x) ≤ 0} ⊆ X 0 holds, and mainly focus on the verification of boundary condition (1). More generally, for better local attractiveness of the boundary in the discrete-time CBF-based safe control when sequential states cross the boundary, we incorporate non-negative constant α ∈ R into Equation ( 1) and adopt the following equivalent condition in a more general form with α ≥ 0 [11, 17] ,EQUATIONRewriting the condition using minimax, the final verification goal in this work is to proveEQUATION3 Symbolic Derivative Bounds PropagationIn this section, we present a method using symbolic bound propagation to verify Equation (3). Since it is hard to precisely characterize the boundary x ∈ ∂X ϕ in Equation (3), we first relax it as the union set of K hyper-rectangles to over-approximate all the roots of ϕ(x) = 0 following [18, 17] ,∂X ϕ ⊂ ∆X ϕ := ∪ K k=1 ∆X (k) , where ∆X (k) := [x (k) , x (k) ] = {x | x (k) ≤ x ≤ x (k) }.We then mainly focus on the verification of max x∈∆X (k) min u∈U φ(x, u) + αϕ(x) as an exchangeable goal when referring Equation (3) with hyper-rectangle bounded input u ∈ U := [u, u] = {u ∈ R m | u ≤ u ≤ u} and each hyper-rectangle bounded state ∆X (k) . For simplicity, we omit the super-script (k) in the following context. Our method first finds a piece-wise linear symbolic upper bound for the minimax expression in Equation (3), then resorts to out-of-the-shelf neural network verification algorithms to generate the proof. We use three steps to obtain the symbolic upper bound as shown in Figure 1 . In Section 3.1, we first find the linear symbolic bounds for dynamic propagation in the inner minimization of Equation (3). We then characterize the linear bounds for ∇ x ϕ using gradient reachability analysis in Section 3.2. Lastly, we introduce a tight method to compute symbolic propagation through the inner product between the linear symbolic bounds for dynamic propagation and the linear bounds for ∇ x ϕ in Section 3.3. 
linear symbolic bounds for dynamics propagation with optimal control inputs: 
 To simplify the verification goal in Equation (3) by solving the inner minimization of control input u over hyper-rectangle U, instead of traversing the vertices in literature [18, 36] , we have the following proposition to efficiently give the equivalent expression of min u∈U φ(x, u) with the optimal control input u v . Proof can be found in Appendix A.1. Proposition 1. When u is within a hyper-rectangle U = [u, u] = {u ∈ R m | u ≤ u ≤ u}, given x ∈ X , the minimum value of φ(x, u) over u ∈ U can be found explicitly as,EQUATIONwhere [ * ] + = max{0, * }, [ * ] -= min{0, * } and the optimal control input u v (x) = argmin u∈V (U ) φ(x, u) lies among the vertices V (U) of hyper-rectangle U given state x.Suppose the control-affine system h(x, u) = f (x)+g(x)u is analytical and its second-order derivative exists w.r.t. x, with the optimal control input u v ∈ [u, u] from Equation (4), the linear lower and upper bounds w.r.t x can be found based on 1-order Taylor models [42, 43, 44] as follows,EQUATIONwhereW v = W v = ∇ ⊤ x h(x, u v ) and b v , b v are shown in Remark 1 in Appendix A.2 through Lagrange remainder with bounded ℓ 2 operator norm of Hessian matrix for each entry of h(x, u v ), following [45] .Now we consider the gradient of neural CBF ϕ : R n → R. As shown in Section 2.1, neural CBFs alternatively consist of linear layers ẑi = y i (z i-1 ) = W i z i-1 + b i and ReLU activation layers z i-1 = σ i-1 (ẑ i-1 ) , with input and output as z 0 = x, ẑL = ϕ(x). For the gradients of ϕ with respect to intermediate vectors z i-1 , ẑi , ∀i = 1, 2, . . . , L, based on chain rule, we haveEQUATIONwhere ⊙ denotes element-wise Hadamard product for two inputs with the same size. Based on the initial condition ∇ ẑL ϕ = 1, the recursive formula (6) will result in the gradient w.r.t the input ∇ x ϕ = ∇ z0 ϕ in a back-propagation manner. More specifically, with initial trivial linear bounds of0x + W ⊤ L ≤ ∇ z L-1 ϕ ≤ 0x + W ⊤ L , the final gradient ∇ x ϕ can be linearly bounded as ∇(x) = Λx + d ≤ ∇ x ϕ ≤ ∇(x) = Λx + d, where Λ = Λ ≡ 0 and for j-th entry of ∇ x ϕ, (7) [d] j = min x∈∆X [ L-1 i=1 W ⊤ i Diag(σ ′ ( ẑi ))]W ⊤ L j , d j = max x∈∆X [ L-1 i=1 W ⊤ i Diag(σ ′ ( ẑi ))]W ⊤ L j .We remark that the bound above is essentially equivalent to the linear bounds in [46] because the initial gradient of the last dense layer ∇ ẑL ϕ = 1 is not related to input x and each derivative of ReLU activation function σ ′ (ẑ i ) is 0 -1 bounded Heaviside step function. Therefore, the input x in the pre-activation bound ẑi will never appear in the bound propagation of ∇ x ϕ, resulting in the weight term with respect to x always being 0. Equation ( 7) greatly simplifies linear bound propagation through the inner product, as shown in the next section. We give the following simple example to show the Jacobian and optimal control input.Example 1. Consider 1D double-integrator ẋ = 0 1 0 0 x + 0 1 u with -0.1 -0.1 ≤ x ≤ 0 0.1 and -1 ≤ u ≤ 1, given a 2-layer neural CBF ϕ(x) = [1 1] ReLU( √ 2 1 √ 2 -1 x) -0.05, based on Equation (7), the linear bounds of ∇ x ϕ(x) are 0x + 0 -1 ≤ ∇ x ϕ ≤ 0x + √ 2 1. Also, the optimal control input from Equation ( 4)is u v = -1 when √ 2 1 x > 0 and u v = 1 when √ 2 -1 x > 0.By solving the inner minimization w.r.t control input u based on Proposition 1, the equivalent verification goal of max x∈∆X ϕ min u∈U φ(x, u) + αϕ(x) in Equation ( 3) isEQUATIONwhich contains the inner product of bounded neural CBF Jacobian ∇ x ϕ in Equation ( 7) and linearly bounded system dynamics h(x, u v ) in Equation ( 5). We define the problem of bound propagation through the inner product below.Problem 1. Given two vector functionsf 1 (x), f 2 (x) : R n → R m with linear symbolic bounds w.r.t input x ∈ R n , i.e. W 1 x+b 1 ≤ f 1 (x) ≤ W 1 x+b 1 , W 2 x+b 2 ≤ f 2 (x) ≤ W 2 x+b 2 ,the problem is to find the linear symbolic bounds for the inner product off 1 (x), f 2 (x), i.e. find W p ,b p , W p ,b p s.t. W p x + b p ≤ ⟨f 1 (x), f 2 (x)⟩ = f ⊤ 1 (x)f 2 (x) ≤ W p x + b p .In our setting of Equation ( 8), we havef 1 (x) = ∇ x ϕ, f 2 (x) = h(x, u v ).To the best of our knowledge, it is not trivial to solve the problem above. However, with the Jacobian of ReLU-based ϕ where Λ = Λ ≡ 0 in Equation ( 7), the problem will be simplified and more straightforward to solve. We derive the following theorem as a sound upper bound of the left-hand side of Equation ( 8) to verify our goal in Equation ( 3). Proof can be found in Appendix A.2.Theorem 2. For any control-affine system h(x, u) = f (x) + g(x)u with bounded control input u ∈ U, given a learned neural CBF ϕ(x) with ReLU activation functions, suppose the boundary state set ∂X ϕ is the union of K hyper-rectangles ∆X as ∂X ϕ ⊂ ∆X ϕ := ∪ K k=1 ∆X (k) , then the goal in Equation (3) is achieved if as a sound upper bound of ∇ x ϕ ⊤ h(x, u v )+αϕ(x), the following inequality holds for any x in each hyper-rectangle state set ∆X ∈ ∆X ϕ ,[d ⊤ ] + [h(x, u v )] + + [d ⊤ ] + [h(x, u v )] -+ [d ⊤ ] -[h(x, u v )] + + [d ⊤ ] -[h(x, u v )] -+ αϕ(x) ≤ 0,where  and d, d and h(x, u v ), h(x, u v ) can be found through Equation (7) and Equation (5), respectively.[ * ] + = max{0, * } = ReLU( * ), [ * ] -= min{0, * } = -ReLU(- * ),If h(x, u v ), h(x, u v ) are concretized and non-symbolic, our result degrades to the interval arithmetic case [47, 36] , showing our symbolic bounds are more general and tighter. Note that for efficient implementation, given ∆X , the optimal control input u is approximated as fixed by Proposition 1.The symbolic upper bound of Theorem 2 can be viewed as the summation of new MLPs with ReLU activation functions, which can be verified through CROWN [38, 39] . Combining branch-and-bound scheme [48, 36, 17] , the new optimal control input u ′ can be found for each new split branch ∆X ′ for the recursive verification. Based on Example 1, we continue to find the corresponding symbolic upper bound of Theorem 2 with branch-and-bound below.Example 2. To verify Example 1 with α = 0.5, initially with -0.1 -0.1 ≤ x ≤ 0 0.1 , the verification condition in Theorem 2 with approximated optimal control inputu v = -1 is √ 2 1 ReLU( 0 1 0 0 x + 0 -1 ) -[0 -1] ReLU(- 0 1 0 0 x - 0 -1 ) + 0.5 × ([1 1] ReLU( √ 2 1 √ 2 -1x) -0.05) ≤ 0, which cannot be verified directly. Then we further split xspecification into two new branches -0.1 -0.1 ≤ x ≤ 0 0 and -0.1 0 ≤ x ≤ 0 0.1, and the verifica-tion condition of the first branch is √ 2 0 ReLU( 0 1 0 0 x+ 0 1 )-[0 -1] ReLU(- 0 1 0 0 x- 0 1 )+0.5×([0 -1] ReLU( √ 2 1 √ 2 -1 x)-0.05) ≤ 0 with u v = 1, and the verification condition of the second branch is √ 2 1 ReLU( 0 1 0 0 x + 0 -1 ) -[0 0] ReLU(- 0 1 0 0 x - 0 -1 ) + 0.5 × ([0 -1] ReLU( √ 2 1 √ 2 -1 x) -0.05) ≤ 0 with u v = -1, which can be verified or further split through off-the-shelf verification tools [46] following such branch-and-bound scheme. 
experiments: 
 In this section, we aim to answer the following questions. Given pre-trained neural CBFs, how does our proposed verification method perform compared to the existing verification baseline under different robot dynamics? In terms of tightness and scalability, how are our proposed method and the baselines influenced by different input specification sizes and model complexity? We answer the Robot dynamics and neural CBF training We conduct experiments using three different robot dynamics, Point Robot [49, 36] with state dimension of 4, Dubins Car [50] with state dimension of 3 and Planar Quadrotor [51] with state dimension of 6. Following [36] , for any random trajectories with bounded control input and state, the robots should avoid obstacles in a non-convex environment as shown in Figure 2 . To this end, the neural CBF is learned to ensure forward invariance of the collision-free states. Similar to [17] , for each robot dynamics, we train the neural CBF based on [14] as regular training and further adopt gradient-based adversarial training [37, 52] to enhance the forward invariance under worst-case state [18] . As default models, we adopt 4-layer MLPs with ReLU with layer dimensions of (16,64,16,1) to model neural CBFs, and further investigate small model with layer dimensions of (8,8,8,1) and large models with layer dimensions of (64, 128, 64, 1) in ablation study of model complexity. More details can be found in Appendix B.1.Verification details and evaluation metric. Given the pre-trained neural CBF, the goal is to verify the forward invariance in Equation (3) over the boundary states, which can be found through grid search as all the hyper-rectangles that contain zero roots of ϕ(x) = 0 following [35, 18] . The default number of grids for each dimension is 20. By traversing all boundary hyper-rectangles, we report the ratio of hyper-rectangles that satisfy the verification condition of Equation (3) as the evaluation metric Verified Rate. We choose two recent incomplete verification methods as the baselines, NNCB-IBP in the non-stochastic continuous version adapted from [28] and BBV [36] , which are both based on interval arithmetic through CROWN bounds [38, 39] and the latter adopts branch-and-bound scheme. For a fair comparison, ours adopts the same maximum splitting iteration number in the branch-and-bound scheme as BBV. Also, following [53, 54, 14] , we adopt efficient sampling-based counterexample falsification to obtain an (unsound) upper bound for the verified rate [37] . We remark that since we purely focus on verification given pre-trained CBFs in this work, we do not fully explore CBF training potential and the performance of Verified Rate can be further improved by combining verification-in-the-loop training [36, 55] , counterexample falsification [27, 40] , etc.Quantitative results. From Table 1 , we can see that under different robot dynamics, ours performs better than the baselines, although the verification becomes more challenging to scale up for higher state dimensions. Specifically, ours and BBV [36] have better performance compared to NNCB-IBP [28] due to the branch-and-bound scheme. With larger α in verification condition (3), the performance of the baseline method decays significantly due to larger over-approximation errors by interval arithmetic, while ours is tighter and keeps relatively higher Verified Rate. The advantage of our method over baselines is larger for neural CBFs with regular training than for neural CBFs with adversarial training, showing adversarial training can enforce the forward invariance to hold.Qualitative results. In this section, we visualize the verification results of Dubins Car for qualitative comparison with baselines in Figure 2 . Given a fixed orientation angle, the boundary of ϕ(x) = 0 is over-approximated as position boxes as input specifications. It can be seen that it is more challenging for both baselines [28, 36] in Figure 2 (a,b) to verify the boxes that face the car head, which are intuitively more likely to result in collision. However, due to the tighter bounds of our symbolic propagation during verification, ours can verify all the boundary boxes, which is consistent with the heatmap visualization of the boundary condition values in Equation (2).Different numbers of boundary hyper-rectangles under different grid sizes. Since the boundary hyper-rectangles are found through grid search with fixed grid size, the finer the grids are, the more boundary hyper-rectangles will be. As shown in Figure 3 , we evaluate the performance with different fine-grained boundaries from 10, 20, 50, and 100 grids for each dimension, respectively. It can be seen that the performance of both ours and baselines increases as the number of boundary hyper-rectangles goes up, but ours consistently presents higher Verified Rate than the baselines do. More specifically, with fewer boundary hyper-rectangles, our superiority over the baselines becomes more significant even for branch-and-bound based BBV [36] , validating the efficiency of our method. Although there is still a margin with respect to the unsound upper bound, our performance can be further boosted through complete verification methods [48] for tighter bounds. Different complexity of neural CBF models. As shown in Table 2 , we investigate the verification performance under different sizes of neural CBFs under regular training and adversarial training. We can see that for regular training, as models become larger, the verified rate will mostly increase due to better overall performance, especially for the baseline BBV [36] . However, since even small models can be effectively robustified and obtain good overall performance through adversarial training, the verified rate tends to decrease as model complexity increases because larger models are more difficult to verify. Besides, , ours can consistently give higher verified rates compared to the baseline.Verification time of branch-and-bound. For a fair comparison of time consumption, we allow branch-and-bound to run forever until achieving 100% verified rate of α = 0.1 under Dubins Car with regular training . From Figure 4 , we can see that with small model size, the total time along the boundary is mainly dominated by the number of boundary hyper-rectangle inputs, and ours performs faster on small NNs. However, with a large model size, the total time is mainly dominated by the single-input verification time and the more hyper-rectangles along the boundary, the finer the input spec will be and the faster the single-input verification will be . In this case, ours cannot always beat BBV since the non-symbolic interval arithmetic is more computationally efficient for singleinput verification with a larger model size. In between, the default model size tells us that the total verification time for ours has the bottleneck of the number of hyper-rectangles, while the baseline has the bottleneck of single-input verification time. 
conclusion: 
 In this work, we propose an efficient verification framework for neural CBFs using symbolic bound propagation, which combines the linearly bounded nonlinear dynamic system and the linear bounds of neural CBFs Jacobian. By utilizing bounded derivatives of activation functions in neural networks, we demonstrate that linear symbolic bounds can be propagated through the inner product of the neural CBF gradient and nonlinear system dynamics, fully keeping the symbolic bound for better tightness. Extensive experiments on various robot dynamics show that our method outperforms interval arithmetic based baselines in terms of verified rate and verification time along the CBF boundary with different model complexity. These results validate the tightness and efficiency of our proposed method. 
 
 Appendix: A.1 Proof of Proposition 1Lemma 1 (Interval Arithmetic, restated from Section 4.1 in [47] .). For any matrix multiplication A • x : R n → R m , if x is entry-wisely bounded as x ≤ x ≤ x, i.e. , x i ≤ x i ≤ x i , ∀i = 1 . . . n, the following inequalities hold for each entry of Ax,EQUATIONwhere[•] + := max{0, •}, [•] -:= min{0, •}.Proof. For the lower bound[A] + x + [A] -x, consider the j-th entry of [Ax] j = n i=1 A j,i x i . With the entry-wise bounds x i ≤ x i ≤ x i , ∀i = 1 . . . n, if A j,i ≥ 0, it holds that A j,i x i ≤ A j,i x i ; similarly, if A j,i < 0, it holds that A j,i x i ≤ A j,i x i . Writing it compactly, we have [A j,i ] + x i + [A j,i ] -x i = max{0, A j,i }x i + min{0, A j,i }x i ≤ A j,i x i. By summing the inequality above over i = 1, . . . , n, it holds that[[A] + x] j + [[A] -x] j = n i=1 [A j,i ] + x i + n i=1 [A j,i ] -x i ≤ [Ax] j = n i=1 A j,i x i , which indicates [A] + x + [A] -x ≤ Ax holds for each entry j. Similarly, the upper bound Ax ≤ [A] -x + [A] +x can be derived in the same way, concluding the proof the interval arithmetic.EQUATIONwhere [ * ] + = max{0, * }, [ * ] -= min{0, * } and the optimal control input u v (x) = argmin u∈V (U ) φ(x, u) lies among the vertices V (U) of hyper-rectangle U given state x.Proof. Based on the chain rule, it holds thatφ(x, u) = ∇ x ϕ ⊤ ẋ = ∇ x ϕ ⊤ f (x) + ∇ x ϕ ⊤ g(x)u.With u ≤ u ≤ u, based on Lemma 1, it holds that[∇ x ϕ ⊤ g(x)] + u + [∇ x ϕ ⊤ g(x)] -u ≤ ∇ x ϕ ⊤ g(x)u.Besides, consider the verticesV (U) := {u v | [u v ] i ∈ {u i , u i }, ∀i = 1, .. . , m}, we can find the equivalent expression for the lower bounds,[∇ x ϕ ⊤ g(x)] + u + [∇ x ϕ ⊤ g(x)] -u = ∇ x ϕ ⊤ g(x)u v (x),where[u v (x)] i = u i if [∇ x ϕ ⊤ g(x)] i ≥ 0 and [u v (x)] i = u i if [∇ x ϕ ⊤ g(x)] i < 0, showing that there exists u v ∈ V (U) s.t. the lower bound [∇ x ϕ ⊤ g(x)] + u + [∇ x ϕ ⊤ g(x)] -u can be achieved equivalently, which concludes that proof.A.2 Proof of Theorem 2 Theorem 3. (restated of Theorem 2.) For any control-affine system h(x, u) = f (x) + g(x)u with bounded control input u ∈ U, given a learned neural CBF ϕ(x) with ReLU activation functions, suppose the boundary state set ∂X ϕ is the union of K hyper-rectangles ∆X as ∂X ϕ ⊂ ∆X ϕ := ∪ K k=1 ∆X (k) , then the following inequality max x∈∂X ϕ min u∈U φ(x, u) + αϕ(x) ≤ 0 is satisfied if as a sound upper bound of ∇ x ϕ ⊤ h(x, u v ) + αϕ(x), the following inequality holds for any x in each hyper-rectangle state set ∆X ∈ ∆X ϕ , Proof. Based on Proposition 2, we have the following inequality hold for any ∆X ∈ ∆X ϕ ,[d ⊤ ] + [h(x, u v )] + + [d ⊤ ] + [h(x, u v )] -+ [d ⊤ ] -[h(x, u v )] + + [d ⊤ ] -[h(x, u v )] -+ αϕ(x) ≤ 0,EQUATIONwhere u v is an approximated constant vertex of optimal control input u v (x) for a sound upper bound of φ(x, u v (x)) over x ∈ ∆X . Now with the bounded dynamics h(x, u v ) ≤ h(x, u v ) ≤ h(x, u v ), by Lemma 1, for any x ∈ ∆X we haveφ(x, u v ) + αϕ(x) = ∇ ⊤ x ϕh(x, u v ) + αϕ(x) ≤ [∇ ⊤ x ϕ] -h(x, u v ) + [∇ ⊤ x ϕ] + h(x, u v ) + αϕ(x).Besides, with the bounded gradient d ≤ ∇ x ϕ ≤ d, the following inequalities hold[d] + ≤ [∇ x ϕ] + ≤ [d] + , [d] -≤ [∇ x ϕ] -≤ [d] -.Then applying Lemma 1 for [∇ ⊤x ϕ] -h(x, u v ) and [∇ ⊤x ϕ] + h(x, u v ), we further have the following inequality hold for any x ∈ ∆X ,φ(x, u v ) ≤ [d ⊤ ] + [h(x, u v )] + + [d ⊤ ] + [h(x, u v )] -+ [d ⊤ ] -[h(x, u v )] + + [d ⊤ ] -[h(x, u v )] -.Therefore, if for any x in each hyper-rectangle state set ∆X ∈ ∆X ϕ , it holds that[d ⊤ ] + [h(x, u v )] + + [d ⊤ ] + [h(x, u v )] -+ [d ⊤ ] -[h(x, u v )] + + [d ⊤ ] -[h(x, u v )] -+ αϕ(x) ≤ 0,and then we have φ(x, u v ) + αϕ(x) ≤ 0 for any x ∈ ∆X . Combining Equation ( 11), we havemax x∈∆X min u∈U φ(x, u) + αϕ(x) ≤ max x∈∆X φ(x, u v ) + αϕ(x) ≤ 0, ∀∆X ∈ ∆X ϕ .Since the exact boundary of ϕ(x) = 0 is the subset of all ∆X , i.e. , ∂X ϕ ⊂ ∆X ϕ := ∪ K k=1 ∆X (k) , it holds that Remark 1 (Linearly bounded dynamics.). We remark that although the linear bounds of dynamics h(x, u v ), h(x, u v ) can be found through 1-order Taylor models [42, 43, 44] in practice, we can give a generally valid lower and upper bounds by assuming bounded ℓ 2 operator norm of Hessian matrix following [45] . For the control-affine system with fixed control input u 0 , ẋ = h(x, u 0 ) with bounded state x ≤ x ≤ x, suppose the ℓ 2 operator norm of Hessian matrix of i-th entry of h(x, u 0 ) is bounded as ∥∇ 2x h (i) (x, u 0 )∥ 2 ≤ M (i) , then at x 0 ∈ [x, x] the following linear bounds can be found ash(x, u 0 ) = W 0 x + b 0 ≤ h(x, u 0 ) ≤ W 0 x + b 0 = h(x, u 0 ) where W 0 = W 0 = ∇ ⊤ x h(x 0 , u 0 ), b (i) 0 = h (i) (x 0 , u 0 ) -∇ ⊤ x h (i) (x 0 , u 0 )x 0 - 1 2 ∥x -x∥ 2 2 M (i) , for i-th entry of b 0 , b (i) 0 = h (i) (x 0 , u 0 ) -∇ ⊤ x h (i) (x 0 , u 0 )x 0 + 1 2 ∥x -x∥ 2 2 M (i) , for i-th entry of b 0 .Specifically, if the control-affine system is linear and time-invariant, i.e. , f (x) = Ax and g(x) = B with constant A, B, where the lower and upper bounds will trivially beW 0 = W 0 = A, b 0 = b 0 = Bu 0 .In this work, symbolic bounds are bounds that are linearly related to the input specification, compared to the concretized bounds where the input dependencies are thrown away. Besides, if a sound but incomplete verifier returns a result of not-hold, maybe the statement will actually hold, but the current verifier is too loose to verify that. In contrast, if sound and complete verifiers return not-hold results, there must exist counterexamples that violate the statement. This motivates us to develop tighter sound and incomplete verification with symbolic bounds. Verification procedure. The first step of verifying neural CBFs is to find the hyper-rectangles to over-approximate the boundary, i.e. , find the superset of all the roots ϕ(x) = 0. Assuming the hyper-rectangles are small enough such that the CBF is continuous and monotonic for each dimension of the state, we check all the gridded hyper-rectangles to find if all the vertices give positive or negative CBF values. Based on the mean value theorem and the assumption above, the roots exist in the hyper-rectangles whose vertices give CBF values with opposite signs. Once the hyper-rectangles are obtained along the boundary, we verify the forward invariance condition based on off-the-shelf neural network verification toolboxes [56, 57, 58, 59 ]. More specifically, given the state specification, we first approximate the optimal control input using one vertex and then find the linear bounds based on TaylorModels.jl [43] . Then with the Jacobian bounds [46] , the condition in Theorem 3 is found to verify if it is no larger than 0. If it does not hold, we adopt branch-andbound by half-splitting the state specification along each dimension, and conduct the breath-first search to verify Theorem 3 recursively until reaching maximum iteration of 1000. By maintaining all verified sub-specifications, we approximate the optimal control input for other vertex traversals to verify if the union set of all verified sub-specifications equals the whole state specification. All the baselines are conducted in a similar way but with concretized bounds instead of the symbolic one in Theorem 3. We remark that although the procedure may not be the most efficient due to approximating optimal control input, the verification result is sound and the scalability is satisfactory for current robot dynamics. It is marked as future work to make the procedure more efficient for robot dynamics with higher dimensions.Comparison with different α in the verification condition. As shown in Figure 5 , we compare our results and the branch-and-bound based baseline BBV [36] with different α in the verification condition with different grid numbers per dimension. The upper bound indicates how challenging the verification will be with different α. It can be seen that with larger α, the performance of BBV decreases more than ours due to larger over-approximation errors. The reason why our results can get better when α goes up lies in that the approximation errors of gradient bounds through ReLU [46] become less dominant and the symbolic property becomes more significant. Besides, with more fine-grained state specifications, the influence of α becomes less because of fewer approximation errors of both interval arithmetic and ReLU gradient. Adversarial training can also help boost the verification performance of BBV when the grid size is large, while it can hurt our performance with small grid sizes due to more training noise during projected gradient descent.Influence of Branch-and-Bound (BaB) on the proposed method. Here we conduct an experiment as an ablation study to show the influence of branch-and-bound in the proposed method. As shown in Table 3 , we can find that without branch-and-bound, the performance is significantly reduced, especially with fewer boundary hyper-rectangles (larger sizes of grids), showing that branchand-bound scheme is essential to the proposed method to alleviate the extra approximation error caused by finding gradient bounds through ReLU [46] .Visulizaton of branch-and-bound scheme. From Figure 6 , we can see that after each splitting for the previous unknown specifications, branches will be doubled and the branch-and-bound follows breadth-first search. With fewer split branches, it can be seen that the coarse specifications cannot be verified for both base BBV [36] and ours. However, with more splitting, ours can successfully verify all branches after 5 splits while BBV can only verify some of the finer specifications, leaving lots of unknown branches to be further split due to looser bounds and larger over-approximation.The visualization shows that even though with the same approximated optimal control input u v , ours can give tighter bounds for neural CBF verification with much fewer split times, resulting in a higher verified rate and shorter verification time.Comparison with symbolic interval analysis based method. Since ReluVal [60] is also based on symbolic bounds and adopts iterative interval refinement, we fairly compare it with CROWN-based baseline BBV [36] and ours with branch-and-bound in [36] and ours with symbolic interval analysis based method ReluVal [60] under different model sizes.bounds when the lower bound of symbolic pre-activation upper bound is less than 0. Therefore, CROWN-like symbolic bounds are generally tighter than ReluVal [48] .One limitation of this work is that it requires an analytical control-affine dynamic model and is not directly applicable to work with (non-control-affine) neural network dynamic models [61, 62, 45] . Besides, it is challenging to efficiently verify neural CBF with high dimensions (> 10) of state due to the exponential growth of the number of boundary boxes. Since the scalability also highly depends on the property of the neural CBF, e.g., unstable neuron patterns, local Lipschitiz, etc. Future work can involve robust or certified training techniques [63, 64, 65, 66] , to enhance the scalability of verification, e.g., new loss from verification conditions, reducing the number of unstable neurons, etc. Future work could also incorporate the linear bounds into verification-in-the-loop training for verified neural CBFs in real-world applications. 


Decision: Strengths: Overall the paper is well-written (but some very long sentences could do with rewrites). The symbolic derivative bounds propagation for verifying ReLU-activated MLP-based CBFs for control-affine systems is a novel contribution. Tighter bounds than the existing interval arithmetic-based method, resulting in increased verified rates as compared to the baselines. 

Weaknesses: There is some concern about the scalability of the method and the claimed verification time improvement. The method also appears to be specific to ReLU-activated MLPs. The reviews provide detailed questions for rebuttal.

----------

As part of the rebuttal, I'd like to commend the authors on clarifying their contributions. I think the strengths of the paper outweigh its weaknesses.

Reviews: review: title: title: The proposed method is incremental and scales poorly with the dimension of the state space limiting its applicability to actual robotic systems.
paper_summary: paper_summary: Given a pre-trained neural network, the paper proposes a symbolic bound propagation method to verify that the neural network is a Control Barrier Function. The paper proposes
main_review: main_review: Clarity:
--------
The writing style of the paper needs to be improved. Several sentences are incredibly long, which makes it hard to follow. 

Originality:
------------
The paper uses symbolic interval analysis to propagate bounds over the Jacobian of the neural network. Symbolic Interval Analysis has been heavily studied for formal verification of NNs. See for example:

[*] Wang, Shiqi, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. "Formal security analysis of neural networks using symbolic intervals." In 27th USENIX Security Symposium (USENIX Security 18), pp. 1599-1614. 2018.
This paper uses a similar concept but on the Jacobian of the NN instead of the NN itself.

Strengths:
------------
- The evaluation section shows the proposed method achieves better results than other methods.

Weaknesses:
--------------
- A major weakness of the proposed method is the need to partition the space of states and control actions, limiting the proposed framework's scalability.

- The paper claims that one of the main contributions is to solve the "quadratic operator of the inner product." But this problem has never been clearly defined. Each section forward points to the next one, but a clear definition of the problem is never well articulated.

Some technical questions need to be addressed. The "Questions For Rebuttal" below details these questions.
questions: questions: (1) What is the difference between $\phi$ and $\phi_\theta$ (it seems the paper is using interchangeably without any mention of that)? 

(2) In Section 2.2, the paper states that one of its objectives is to ensure that the sublevel set of $\phi$ is a valid subset of the user-specific safe set. Later in the same paragraph, the paper abandons this objective by assuming that one can modify the pre-trained NN (by adding a constant C) to achieve such a goal. The paper should explain how to find such a constant C since it affects the overall time for verifying the CBF. Was the time taken to find C accounted for in the experiments?

(3) In Section 3.2, the paper states that "Equation (7) avoids intractable linear bound propagation through the quadratic operator of the inner product." It is not clear why linear bound propagation is intractable. Off-the-shelf tools are capable of propagating linear bounds over a whole set of nonlinearities in polynomial time. A proof showing that linear bound propagation is intractable is needed.

(4) Just after Theorem (2), the paper compares the obtained bound to "concretized and non-symbolic." But what about "symbolic interval analysis" like those used in [*] above?
limitations: limitations: 2
review_summary: review_summary: The proposed method is incremental and scales poorly to robots with high-dimensional state spaces.
title: title: This paper is well-written and organized, clearly presenting an efficient verification approach for verifying neural control barrier functions with promising performance demonstrated on various robot systems.
paper_summary: paper_summary: This paper addresses the challenges of verifying control barrier functions (CBFs) parameterized by neural networks (neural CBFs) in safety-critical systems and robot control applications. The authors introduce a novel verification framework that leverages symbolic derivative bound propagation. This method combines the properties of linearly bounded nonlinear dynamic systems with the gradient bounds of neural CBFs, utilizing the Heaviside step function for the derivatives of activation functions. The proposed approach propagates symbolic bounds through the inner product of the neural CBF Jacobian and nonlinear system dynamics. Extensive experiments on various robot dynamics demonstrate that this method outperforms interval arithmetic-based baselines in terms of verified rate and verification time, showcasing its effectiveness and efficiency across different model complexities.
main_review: main_review: This paper is well-written and organized. It clearly presents all relevant information and the reasoning and technical steps behind the development of the verification approach for verifying neural control barrier functions. The efficacy of the proposed approach is validated by extensive experiments.

Strengths:
- Well-written and to the point.
- Mathematically Sound: The basis for the framework (linear bounds for dynamics, bounding Jacobian of neural CBF, bound propagation through inner product) is adequately introduced, laying out a clear foundation for the verification algorithm.
- The numerical examples are constructive for understanding the technical approaches
- Extensive experiments validate the efficacy of the proposed approach 

Weaknesses:
- To compute the control signal from the QP program associated with the CBF $\phi(x)$, $\dot \phi(x)$ is required. However, it is unclear how $\dot \phi(x)$ can be computed, considering that $\phi(x)$ uses the ReLU activation function, which is not differentiable.
questions: questions: 1.	Please explain the meaning of “symbolic”  and  “incomplete verification” somewhere in the manuscript (for readers who are not in the field of verification)
2.	Please explain how to compute $\dot \phi(x)$ (to compute the control signal) when $\phi(x)$ uses a ReLU function.
3.	In the paragraph right below Theorem 2, it mentions “the optimal control input u is approximated…”. Where does the approximation come from?
limitations: limitations: 3
review_summary: review_summary: The paper is well-written and organized. The symbolic bound propagation based verification approach seems very promising due to the tightness of the bounds achieved through clearly explained steps.
title: title: Official Review by Reviewer mp6J
paper_summary: paper_summary: Efficient and accurate verification of learning-based control barrier functions (CBFs) remains an important and difficult challenge. The authors propose a novel verification method for ReLU-activated multilayer perceptron (MLP) networks based on symbolic derivative bounds propagation. In experiments on different systems and model complexities, the authors demonstrate that their method achieves superior verified rate and verification time as compared to state-of-the-art baselines.
main_review: main_review: $\textbf{Quality and Clarity:}$ The paper is well-written and clear to the reviewer, except for a few minor grammar mistakes/typos scattered throughout. The reviewer especially appreciates the concise technical background provided in Section 2. The technical content in Section 3 is also well-presented.

$\textbf{Originality:}$ The original contribution of the paper is the formulation of the symbolic derivative bounds propagation for verifying ReLU-activated MLP-based CBFs for control-affine systems. The contribution is novel as far as the reviewer understands it.

$\textbf{Significance:}$ The proposed approach provides tighter bounds than the existing interval arithmetic based method, resulting in increased verified rates as compared to the baselines. The reviewer believes this is a significant achievement. The authors also claim shorter verification times with their method, although the reviewer is not fully convinced on this point (elaboration in $\textbf{Weaknesses}$).

$\textbf{Strengths:}$ The authors provide a helpful example in Section 3 to clarify their approach. They also show that their bounds formulation contains the interval arithmetic case and thus yields only tighter bounds. This advantage is convincingly demonstrated in their experiments. The parameters along which the experiments vary are well-chosen.

$\textbf{Weaknesses:}$
 - The reviewer is not convinced of the claimed verification time improvement, since it seems to vary depending on the nature of the underlying safety solution, the model size, and the grid size. It would be helpful for the authors to provide an analysis on the conditions that result in better/worse verification time.
 - The proposed method is specific to ReLU-activated MLPs. However, other neural network architectures, e.g., physics-informed neural networks (PINNs) with sinusoidal activations, have also become popular for modeling safety functions and their gradients. 
 - The method does not scale well with the state dimension.
questions: questions: - The reviewer believes it should be clarified in the abstract that the proposed method is specific to ReLU-activated MLPs.
 - It is not clear how the optimization over the state space in Equation (7) and in Example 1 is achieved.
 - What is the significance of $\alpha$, and how does the choice of $\alpha$ affect the proposed method? Is it fair to use $\alpha \neq 0$ during experiment comparisons?
 - What factors influence the magnitude of the overapproximation errors during the bound computation?
 - It is unclear to the reviewer how the $\textit{approximated}$ control input is computed, e.g., in Example 2. 
 - What advantages do CBF-based approaches have over reachability-based approaches (which are guaranteed to yield provably optimal safety functions) for tractable low-dimensional systems, especially since the proposed verification approach scales intractable with the state dimension?
limitations: limitations: 2
review_summary: review_summary: The reviewer recommends that the paper is accepted. The paper presents a modest but tangible improvement to existing interval arithmetic based verification methods. The reviewer believes that the proposed symbolic derivative bounds propagation is highly relevant and a good baseline for future work to improve upon.