Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation
Authors: Hanjiang Hu
Yujie Yang
Tianhao Wei
Changliu Liu
Venue: CoRL 2024 (2024)
Keywords: Learning for control
control barrier function
formal verification
TL;DR: We propose a new neural CBF verification framework using symbolic derivative bound propagation to give tight and efficient bounds for verifying forward invariance.

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.

Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation
Hanjiang Hu Yujie Yang Tianhao Wei Changliu Liu
The Robotics Institute, Carnegie Mellon University han jaanjiang@@cm edu, cliu6Gandrew. cmu.
Control barrier functions (CBFs) are important in safety-critical sys- tems and robot control applications. Neural networks have been used to param- eterize 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 new efficient verification framework for ReLU-based neural CBFs through symbolic derivative bound propagation by combining the linearly bounded nonlinear dynamic sys- tem 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 dy- namics, 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: /ttp:////ttttbb com ittiiiieelilii otg.tho...o///atlllloeeetooooooo verify-neural-Coe
Abstract:
Keywords: Learning for control, control barrier function, formal verification
Introduction
Safe control 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 hi- erarchical manner [5]. As an effective tool of safe control, control barrier functions (CBFs) have been studied for years both verification and synthesis [6. 7, 8, 9, 10]. A valid CBF guaran- tees 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 in- variance, polynomial-basee
CBFs have been proposed based on hand-crafter parametric functions [11, 12, 13], which can be verified through algebraic geometry techniques like sum-of -oi---u--s-sssssss (SOS) optimization [14, 15, 16]. However, polynomial-based CBFs cannot encode complicated safety con- straints [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 pow- erful expressiveness in modeling complex dynamics with bounded control inputs [18, 19, 20, 21, 22]. But it challenging to guarantee that the learned neural CBF is valid because of its poor mathemat- ical interpretability. One way 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, 37J. Although linear bound based verifi-
8th Conference Robot Learning (CoRL. 2024), Munich, Germany.

---

f(x) g(Ou
$00
System denamics
Centrol spoc
Sec.
0,+00)
Grodiett
(x.u) + (x)
State spec
Output spec
(K)
Variicctioon goal:
Nauni CSF
mas ((X.
Figure 1: Overview of the verification pipeline with symbolic bound propagation, from input speci- fications boundary state and control to the output specification of the CBF condition.
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, introduce efficient incomplete verification framework for ReLU-based neural CBFs using the fully linear symbolic bound propagation w.r. state by combining the gradient of CBFs and neural dynamics, 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 prop- agated 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 verified rate and verification time along the CBF boundary. In summary, our contributions listed below.
We propose 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
2.1 Safe Control with Neural CBF
Given a control-affine system x = f(x) + g(x)u with state x E X' C R" and bounded con- trol input E 21 C Rm and user-specified safe set Xo C X, neural control barrier func- tion (neural CBFs) are defined as continuous and piecewise smooth functions á F" R with neural network parameterization. Generally, the neural CBF consists of feedforward lay- Vs R " + R": 1-,,i=11 1,2, I. after each linear feedforward layer. Therefore, the neural CBF is formulated as the compositional function d(x) = VL 0 - 1. yL-2 0 (x), where y R + R. and nig = n,, n2, = Furthermore, each feedforward layer is parame- terized with weight W, E ". xn.-: and bias b, E " as 2, = (z,-.) = W b,, where 2 1 T. the pre-activation output of y; and 7;-1 E m is the output of last activation layer 2,-1 Ji- (2.-)). A neural CBF parameterized with neural network 0 valid if the sublevel set X₂ = (x E X' (x(x)) 0} C Xo satisfies forward invariance, defined below. In the absence of ambiguity, we omit the subscript 0 and directly use the notation á to represent neural CBF.
R 1,2, ........ L,, associated with L ReLU activation functions
Definition 1. A set X forward invariant if for state x(0) E Xs at time 0, any following time > 0, there always exists control input u(t) U such that x(t) E X according to x f(x) + g())u.
By Nagumo theorem [41], the forward invariance holds if the following boundary condition holds.

---

Theorem (from [11, 6)). Given neural CBF Φ. if the following boundary condition over boundary
set Ox == {x E X' xxx) = 0} holds for the sublevel set X == {x
E X x(x) s 0),
VX E 0X, := fx X (xx) 0). Bu E U, s.t. x) (f(x) + g(x)u) S 0,
(1)
then the sublevel set Xx - xx E 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 signifieance verify that learned neural CBFs are valid.
2.2 Goal of Verifying Nerual CBF
Given a pre-trained neural CBF 6. our goal is to formally verify that it is valid in two aspects. One is to ensure that the sublevel set Xg == {x E X ((x) - 0} is a valid subset of the user-specified safe set Xo, and the other is to guarantee the forward invariance in Definition 1. Since the neural CBF can be bounded above by &c o C, C > 0 to shrink the forward invariance set into the user-specified safe set, without loss of generality, 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 a E R into Equation (1) and adopt the following equivalent condition in more general form with a 2 [ 17].
reasonably assume that X2 == {x X Φ(x) - 0} C X
Vx E 0.2 Bu E U, s.t. é(x, u) + aœ(x) Vx T (f(x) - g(x)u) + aΦ(x) S 0.
(2)
Rewriting the condition using minimax, the final verification goal in this work is to prove
max min o(x, u) + aạ(x)= = max min vxδ f(x) + VxΦ g(x)u + aΦ(x) S 0.
(3)
xEOXg well
xEOX, RE0Xs uel
3 Symbolic Derivative Bounds Propagation
In this section, we present a method using symbolic bound propagation to verify Equation (3). Since it is hard to precisely characterize the boundary x E OX, in Equation (3), we first relax it as the
union set of K hyper-rectangles to over-approximate all the roots of (xx) = 0 following [18, 17],
0.4 C AX, == KK_ - where (A) == (x()), (x)) = {x (k) S S x()) We
then mainly focus on the verification of max minuez o(x, u) + aΦ(x) (xx as an exchangeable
goal when referring Equation (3) with hyper-rectangle bounded input u U == [u. uj (u e
Rm Ius S u S ú} and each hyper-rectangle bounded state ( For simplicity, we omit the super-script (k) in the following context. Our method first finds 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 V 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 V in Section 3.3.
3.1 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 over hyper-rectangle 44 instead of traversing the vertices in literature [18, 36), we have the following proposition to efficiently give the equivalent expression of minueu Φ(x, u) with the optimal control input u, Proof can be found in Appendix A.I.
Proposition 1. When is within hyper-rectangle U [| {u E R. X, the minimum value of d(x, u) over U can be found explicitly as
S S u], given
min d(xx u) = vx T f(x) + ( g(x)]+ ut well
"g(()) u [
~(x; u. (x)),
(4)
3

---

where [+]+ max [), = min 0. and the optimal control input u. (x) argm ((x, u) lies among the vertices V(L) of hyper-rectangle U given state x.
Suppose the control-affing system h(x, u) f(x) + + u analytical and its second-order deriva- tive exists w.r.t. with the optimal control input u, E [u. uj from Equation (4), the linear lower and upper bounds w.r.t can be found based on 1-order Taylor models [42, 43, 44] follows,
4(x, u,) W x b. I h(x, u.) f(x) + g(x)u S W. b, h(xx, u.), (5) where W W. = hxx, up) and b.y b, are shown in Remark in Appendix A.2 through Lagrange remainder with bounded lg operator norm of Hessian matrix for each entry of 1((,, u.), following [45].
3.2 Bounding the Jacobian Neural CBF
Now consider the gradient of neural CBF ò : RR R. As shown in Section 2.1, neural CBFs alternatively consist of linear layers 2; ya (z W + b; and ReLU activation layers 2 (2;-), with input and output 2g x, 2. = <(x). For the gradients of Φ with respect to intermediate vectors - 2,, Vi 1,2,.... L, based on chain rule, we have
Oz.
V=_Φō V y4 2. Ø = W V o. Va. O2:
O V. o= = 0'((2) V
(6)
where + denotes element-wise Hadamard product for inputs with the same size. Based on the initial condition V ø 1, the recursive formula (6) will result in the gradient w.r.t the input manner. More specifically, with initial trivial linear bounds of Ox + W 1 S V V 2 & 0x + W7, the final gradient Vx can be linearly bounded as
v V in back--ropagateee
(xx) = Ax + - S V & (x) = Ax + d, where = = 0 and for j-th entry of VxO, (7)
L-1
L-1
[]]
min xEAX
W. ())
max xEAX
III
W. Di (Z)))
We remark that the bound above essentially equivalent the linear bounds [46] because the initial gradient of the last dense layer V2, 1 is not related input and each derivative of ReLU activation function o' o'(2, is
bounded Heaviside step function. Therefore, the input x in the pre-activation bound 2, will never appear in the bound propagation of Vxú, 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.
0
1
0
0011
Example 1. Consider 1D double--ntegrator
0
0
x
+
with
-0.1
S
0.1
1/2
and -1 < u S 1, given 2-layer neural CBF ((x)
[1
1]
ReLUU
x)
0..5,, based
1/2 -1
0
[2
on Equation (7), the linear bounds of Vx0(x) are Ox +
-1
S Vx S 0x +
Also, the
1
optimal control input from Equation (4) is uy = -1 when
[V2 1] x > and u, = when
[v2 -1 x1>> 0.
3.3
Verification with Symbolic Bound Propagation through Inner Product
By solving the inner minimization w.r.t control input u based on Proposition the equivalent veri- fication goal of max AN min é(x, u) ax(x) in Equation (3) is
d(x, u.) ad(x)= max XEAX,
max
VxΦ h(x, u.) + (œ(x) 0,
(8)
XEAX,
which contains the inner product bounded neural CBF Jacobian Vx in Equation (7) and linearly bounded system dynamics h(x, u.) in Equation (5). We define the problem of bound propagation through the inner product below.

---

Problem 1. Given two vector functions f1 fx(x), fz(x): : R" + R with linear symbolic bounds w.r.t imput x E RR, ie. W, S < & 1 W,x+ ba S (x) & W2x+by b2g the problem is to find the linear symbolic bounds for the inner product of fi fi(),, f2(x), iee find W Wpy Wp. bp
s.t. W x bp S (fi(x), f2(x) fi (x) - Wx bp.
In our setting of Equation (8), we have fi(x) = VxΦ, f2(x) = h(x, u.)) To the best of our knowledge, it is not trivial to solve the problem above. However, with the Jacobian of ReL.U-based e where A = A = 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 imput E U, given learned neural CBF o(x) with ReLU activation functions, suppose the boundary state set 0X4 is the union of K hyper-rectungles AX as 0x C A = ,
Ax((), then the goal in Equation (3) is achieved if as a sound upper bound Vx h(x, +xx(x, the following inequality holds for any x in each hyper-rectangle state set AX' E ANg.
a 1Txx, u+)]+ + ld [T(xx u.)l- + 1- )+ + +1a"1 1
[xx,, u. a((xx S
where [+]+ = max + ReI.U()): [+]_ = (0, +)
Rel.U(+*), and d, d and h(x, ue), L(xx, un) can be found through Equation (7) and Equation (5), respectively.
If hxx, u, Lxx,, u,) 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 AX, 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-boundt scheme [48. 36, 17]. the new optimal control input u' can be found for each new split branch AX" 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.
-0.1
0 0.1
Example 2. To verify Example 1 with a 0.5, initially with
-0.1
S
x
S
the verification condition in Theorem with approximated optimal control imput
u1
-1 is Iv2 1] ReLU
0
0
1
x
+
-1
0 [0 -1] -1]
0
0
1
x
[
+ 0.5 X
V2
([1 1] ReLU
x)
0.05)
O, which cannot be verified directly. Then we further split
V2
-1
0.1
0.1
0
specification into two new branches
$ x
and
S
x
and the verifica-
0.1
0
0.1 -e]
0
[0
1
tion condition of the first branch is
[V2
0] Rel.U(
0 0
x+
10
0
V2
+005x(10 -1] ReLU
x)
-0.05) S 0 with u. = 1. and the verification condition
2
-1
0
1
x - [ [-]= jo 0] RELU
[0 _ x
of the second branch is [V2
1]
ReLu
0
V2
1
0.5 x (10 -1]
x) - 0.05) < 0 with u. = 11 which can be verified or further
22 -1
split through off -he-- verification tools [46] such branch-and and-bound scheme.
4 Experiments
In this section, we aim to answer the following questions. Given pre-trained neural CBFs, how does our proposed verification method perform compared the existing verification baseline under different robot dynamics? In terms of tightness and scalability, how are our proposed method and the basclines influenced by different input specification sizes and model complexity? We answer the
5

---

(a)
(b)
(c)
(d)
Figure 2: Illustration of the verification results for Dubins using (a) NNCB-IBB CBP [28], (b) BBV
[36] and (c) ours. The obstacle is in gray. The state boundary of σ(x) = given orientation -4 over-approximated by boxes. Green boxes denote the results of "hold" while red ones denote the
results of "unknown" to verify é 0.5Ø 0, whose value is shown as heatmap in Fig. (d).
CBF training type Verification condition
Regular training
Adversarial training
0.1
a 0.5
a
1.0
a 0.1
a 0.5
1.0
BBV [36]
0.617
0.492
0.448
0.750
0.719
0.695
Dubins Car 3-dim state
NNCB-IBP [28]
0.446
0.437
0.425
0.623
0.601
0.577
Ours
0.700
0.729
0.706
0.778
0.730
0.732
BBV [36]
0.384
0.355
0.317
0.391
0.367
0.337
Point Robot 4-dim state
NNCB-IBP [28]
0.280
0.261
0.237
0.317
0.304
0.282
Ours
0.404
0.401
0.391
0,404
0.397
0.385
BBV [36]
0.314
0.319
0.290
0.352
0.335
0.313
Planar Quadrotor 6-dim state
NNCB-IBP [28]
0.301
0.279
0.249
0.216
0.205
0.168
Ours
0.354
0.382
0.341
0.359
0.404
0.475
Table 1: Comparison of Verified Rate with baselines on different dynamics models under different
neural CBF training settings.
first question in Section 4.2 through quantitative and qualitative comparison and answer the second one in Section 4.3 as the ablation study. Prior to that, we first introduce the experiment setup of robot dynamics and verification details.
4.1 Experimental Setup
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 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 non-convex environment
shown in Figure 2. To this end, the neural CBF is learned ensure forward invariance of the collision-free states. Similar to [17], for each robot dynamics, train the neural CBF based [14] as regular training and further adopt gradient-based adversarial training [37, 52] enhance the forward invariance under worst-case state [18]. As default models, we adopt 4-layer MLPs with ReLU with layer dimensions of (66,4,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 124,128,)4,1) ablation study of model complexity. More details can be found Appendix B.I.
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 be found through grid search as all the hyper-rectangles that contain zero roots of (²x) x) O following [35, 18). The default number of grids for each dimension is 20. By traversing all boundary hyper-rectangles, we report the ratio of recer-restangles that satisfy the verification condition Equation (3) as the evaluation metric Verified Rate. We choose two recent incomplete verification methods as the baselines, NNCB- IBP the -tn-httccastic 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 fair comparison, ours adopts the same maximum splitting iteration number in the Tranch-and-o bound scheme BBV. Also, following [53, 54, 14], we adopt efficient sampling-basee

---

0=1.11 regular training
0.5, regular training
1.0, regular training
Veirfled Rate
0.8
Velrfled Rate
Veirfied Rate
0.7
07
0.7
BBV
BBV
88
BBV
NNCB- IBP
NNCB-IBP
NNCB-IBP
Ours
Ours
Ours
0.4
Upper bound
04
Upper bound
Upper bound
10"
10
101
10"
10"
13"
Num. of boundary hyperrestangles
Num. of boundary hyperrectanglees
Numn of boundary hyperreetangles
a 0.1, adversarial training
a 0.5, adversarial training
a- 1.0, adversarial training
0.9
0.9
Vertfied Rate
0.5
Verified Rate
a.
0.7
0.7
0.7
0.6
BBV
0.6
BBV
BBV
NNCB-IBP
NNC3-IBP
NNCB-IBP
Ours
Ours
Ours
0.4
Upper bound
033
Upper bound
Upper bound
0.3
16"
16
10"
16
12'
10"
Num, of boundary hyper-rectangies
Num. of boundary hyper-rectangees
Num. of boundary heperrrsctangles
Figure 3: Verified Rate under different number of boundary hyper-rectangles under different grid sizes. The grid number per dimension for each figure (from left to right); 10, 20, 50, 100. The dashed line denotes the results of falsification by counterexample upper bounds.
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--ee loop training [36, 55), counterexample falsification [27, 40], etc.
4.2 Results Comparison
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 the muuchhandd-bunse scheme. With larger a in verification condition (3), the performance of the baseline method decays significantly due 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 qual- itative comparison with baselines in Figure 2. Given fixed orientation angle, the boundary of Φ(x) 0 is over-approximated 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 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).
4.3 Ablation Study
Different numbers of boundary hyper-rectangles under differrnt grid sizes. Since the bound- ary 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. can seen that the performance of both ours and baselines increases as the number of bound- ary hyper-rectangles goes up. but ours consistently presents higher Verified Rate than the basclines do. More specifically, with fewer boundary hyper-rectangles, our superiority over the baselines be- comes more significant even for branch-and-bound based BBV [36], validating the efficiency of our method. Although there is still margin with respect to the unsound upper bound, our performance can be further boosted through complete verification methods [48] for tighter bounds.
7

---

Verified rate Dubins Car
Regular training
Adversurial training
under different model sizes
Small
Default
Large
Small
Default
Large
BBV [36]
0.506
0.617
0.729
0.785
0.750
0.458
0.1
Ours
0.558
0.700
0.752
0.788
0.778
0.481
BBV [36]
0.365
0.492
0.635
0.781
0.719
0.411
0 0.5
Ours
0.562
0.729
0.688
0.792
0.730
0.444
BBV [36]
0.208
0.448
0.510
0.750
0.695
0.367
1.0
Ours
0.540
0.706
0.592
0.758
0.732
0.413
Table The influence of neural CBFs with different model sizes on branch-and-bound based verifi- cation baseline and ours with Dubins Car. The Small, Default and I Large denote 4-layer ReL.U-MIPP with layer output dimensions of (8,8,811). (16,64,16, 16,1,,,,1))). and 14,,128,64111 respectively.
Time comparison with small model size
Time comparison with default model size
Time comparison with big model sire
BBV
120
BBV
Verificaaion time (S)
Ours
Verefication time (c)
330-
Cur
Verrication time
12.5
250-
80
250-
7.5
60-
+
40.
1000
2.5
20-
50-
boundary hyperrectangles
boundary hyperrectangles
boundary hyperrestangles
Figure 4: Comparison of verification time using branch-and- to achieve 100% Verified Rate with different model complexity with regular training. The more hyper-rectangles the boundary set contains, the finer the state input specification will be.
Different complexity of neural CBF models. As shown in Table we investigate the verification performance under different sizes of neural CBFs under regular training and adversarial training. We can see that for regular training, 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 verify. Besides, ours can consistently give higher verified rates compared the baseline.
Verification time of branch-and-bound. For fair comparison of time consumption, allow forever until achieving 100% verified rate of 0.1 under Dubins Car
branch-and-boue bound 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 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 this case, ours cannot always beat BBV since the non-symbolic interval arithmetic more computationally efficient for single- input verification with 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.
5 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 net- works, 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 various robot dynamics show that method outper- forms 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.

---

Acknowledgments
This work part supported by the National Science Foundation under Grant No. 2144489.
References
[1] R. Cheng, G. Orosz, R. M. Murray, and J. W. Burdick. End-to-end safe reinforcement learning through barrier functions for safety-critical continuous control tasks. In Proceedings of the AAAI conference on artificial intelligence, volume 33, pages 3387-3395, 2019.
[2] Ferlez, M. Elnaggar, Y. Shoukry, and C. Fleming. Shieldnn: A provably safe nn filter for unsafe nn controllers. arXiv preprint a1Xhv:2006.09564, 2020.
[3] W. Zhao, T. He, and C. Liu. Model-free safe control for zero-violation reinforcement learning. In 5th Annual Conference on Robot Learning. 2021.
[4] W. Zhao, He, and C. Liu. Probabilistic safeguard for reinforcement learning using safety index guided gaussian process models. In Learning for Dynamics and Control Conference, pages 783-796. PMLR, 2023.
[5] W. Zhao, T. He, R. Chen, T. Wei, and C. Liu. State-wise safe reinforcement learning: a survey. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, pages 6814 2814-6822, 2023.
[6] C. Liu and M. Tomizuka. Control safe set: Addressing safety in human-robot interactions. In Dynamic Systems and Control Conference, volume 46209, page V003T42A003. American Society of Mechanical Engineers, 2014.
[7] H. Dai and F. Permenter. Convex synthesis and verification of control-lyapunov and barrier functions with input constraints. In 2023 American Control Conference (ACC), pages 4116 4123. IEEE, 2023.
[8] X. Xu. W. Grizzle, P. Tabuada, and A. D. Ames. Correctness guarantees for the composition of lane keeping and adaptive cruise control. IEEE Transactions on Automation Science and Engineering, 15(3):1216-1229, 2017.
[9] J. Breeden and D. Panagou. High relative degree control barrier functions under input con- straints. In 2021 60th IEEE Conference on Decision and Control (CDC), pages 6119-6124. IEEE, 2021.
[10] Kang, Y. Chen, H. Yang, and M. Pavone. Verification and synthesis of robust control barrier functions: Multilevel polynomial optimization and semidefinite relaxation. In 2023 62nd IEEE Conference Decision and Control (CDC), pages 8215-8222 IEEE, 2023.
[11] A. D. Ames, S. Coogan, M. Egerstedt, G. Notomista, K. Sreenath, and P. Tabuada. Control barrier functions: Theory and applications. In 2019 18th European control conference (ECC), pages 3420-3431. IEEE, 2019.
[12] W. Xiao and C. Belta. Control barrier functions for systems with high relative degree. In 2019 IEEE 58th conference decision and control (CDC), pages 474-479. IEEE, 2019.
[13] S. Prajna, A. Jadbabaie, and G. J. Pappas. A framework for worst-case and stochastic safety verification using barrier certificates. JEEE Transactions on Automatic Control, 52(8):1415 1428, 2007.
[14] H. Zhao, X. Zeng. Chen, and Z. Liu. Synthesizing barrier certificates using neural net- works. In Proceedings of the 23rd international conference hybrid systems: Computation and control, pages 1-11, 2020.

---

[15] M. Schneeberger, F. Dörfler, and S. Mastellone. Sos construction of compatible control lya- punov and barrier functions. JFAC-PuperSOnl..ne, 16(2):14488-104444 2023.
[16] A. Clark. Verification and synthesis of control barrier functions. In 2021 60th IEEE Conference on Decision and Control (CDC), pages 6105-6112 12. IEEE, 2021.
[17] H. Zhang, W. Junlin, V. Yevgeniy, and Clark. Exact verification of reL. neural control barrier functions. In Advances neural information processing systems, 2023.
[18] S. Liu, C. Liu, and J. Dolan. Safe control under input limits with neural control barrier func- tions. In Conference on Robot Learning, pages 1970-1980. PMLR, 2023.
[19] O. So, Z. Serlin, M. Mann, Gonzales, K. Rutledge, N. Roy, and C. Fan. How train your neural control barrier function: Learning safety filters for complex input-constrained systems. arXiv preprint mrXi:2231.15578, 2023.
[20] V. Zinage, R. Chandra, and Bakolas. Neural differentiable integral control barrier functions for unknown nonlinear systems with input constraints. arXiv preprint arXiv:2312.07345, 2023.
[21] C. Dawson, Z. Qin, S. Gao, and C. Fan. Safe nonlinear control using robust neural Iyapunov- barrier functions. In Conference on Robot Learning, pages 1724-1735 PMLR, 2022.
[22] B. Dai, P. Krishnamurthy, and F. Khorrami. Learning a better control barrier function. In 2022 IEEE 61st Conference on Decision and Control (CDC), pages 945-950. IEEE, 2022.
[23] N. Boffi, S. Tu, N. Matni, J.-J. Slotine, and V. Sindhwani. Learning stability certificates from data. In Conference Robot Learning, pages 1341-1350. PMLR, 2021.
[24] C. Dawson, S. Gao, and C. Fan. Safe control with learned certificates: A survey of neural Iyapunov, barrier, and contraction methods for robotics and control. IEEE Transactions on Robotics, 2023.
[25] W. Xiao, T.H. Wang, R. Hasani, M. Chahine, A. Amini, X. Li, and D. Rus. Barriernet: Differentiable control barrier functions for learning of safe robot control. IEEE Transactions on Robotics, 2023.
[26] L. Lindemann, H. Hu, A. Robey, H. Zhang, D. Dimarogonas, S. Tu, and N. Matni. Learning hybrid control barrier functions from data. In Conference on Robot Learning, pages 1351- 1370. PMLR, 2021.
[27] Y.-C. Chang, N. Roohi, and S. Gao. Neural lyapunov control. Advances in neural information processing systems, 32, 2019.
[28] R. Mazouz, K. Muvvala, A. Ratheesh Babu, Laurenti, and M. Lahijanian. Safety guaran- tees for neural network dynamic systems via stochastic barrier functions. Advances in Neural Information Processing Systems, 35:9672-9666 96866 2022.
[29] Y. Yang, H. Hu, T. Wei, E. Li, and C. Liu. Scalable synthesis of formally verified neural value function for hamilton-jacobi reachability analysis. arXiv preprint arXiv:2407.20532, 2024.
[30] Y. Yang, Z. Zheng, S. F. Li, M. Tomizuka, and C. Liu. The feasibility of constrained reinforce- ment learning algorithms: A tutorial study. arXiv preprint arXiv:2404. N00:64404..0064, 2024.
[31] S. Gao, S. Kong, and E. M. Clarke. dreal: An smt solver for nonlinear theories over the reals.
In International conference on automated deduction, pages 208-214. Springer, 2013.
[32] A. Peruffo, D. Ahmed, and A. Abate. Automated and formal synthesis of neural barrier cer- tificates for dynamical models. In International conference tools and algorithms for the construction and analysis of systems, pages 370-388. Springer, 2021.
10

---

[33] Q. Zhao, X. Chen, Z. Zhao, Y. Zhang, E. Tang, and X. Li. Verifying neural network controlled systems using neural networks. Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control, pages 1-11, 2022.
[34] M. Tayal, H. Zhang, P. Jagtap, A. Clark, and S. Kolathaya. Learning formally verified control barrier function in stochastic environment. arXiv preprint arXiv:2403.19332 2024.
[35] F. B. Mathiesen, S. C. Calvert, and L., Laurenti. Safety certification for stochastic systems via neural barrier functions. IEEE Control Systems Letters, 7:973-978, 2022.
[36] X. Wang, L. Knoedler, F. B. Mathiesen, and J. Alonso-Mora. Simultaneous synthesis and verification of neural control barrier functions through branch-and-bound verification-in-the- loop training. arXiv preprint arXiv:2311.10438, 2023.
[37] Chen, Molu, and M. Fazlyab. Verification-aided learning of neural network barrier func- tions with termination guarantees. arXiv preprint arXiv:2403.07308 2024.
[38] H. Zhang, T.-W. Weng, P.-Y. Chen, C.-J. Hsieh, and L. Daniel. Efficient neural network robust- ness certification with general activation functions. Advances in neural information processing systems, 31, 2018.
[39] K. Xu, Z. Shi, H. Zhang, Wang. K.-W. Chang, M. Huang, B. Kailkhura, X. Lin, and C.-J. Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. Advances Neural Information Processing Systems, 13:1129-1141, 2020.
[40] L. Yang, Dai, Z. Shi, C.-J. Hsich, Tedrake, and H. Zhang. Lyapunov neural control for state and output feedback: A novel formulation for efficient synthesis and verification. arXiv preprint arXiv:2404.07956, 2024.
[41] F. Blanchini, S. Miani, et al. Ser-theoretic methods in control, volume 78. Springer, 2008.
[42] K. Makino. Rigorous analysis of nonlinear motion in particle accelerators. Michigan State University, 1998.
[43] M. M. Joldes. Rigorous polynomial approximations and applications. PhD thesis, Ecole normale supérieure de lyon-ENS LYON, 2011.
[44] M. Streeter and J. V. Dillon. Automatically bounding the taylor remainder series: Tighter bounds and new applications. urXiv preprini arXiv:2212.11449, 2022.
[45] H. Hu, J. Lan, and C. Liu. Real-time safe control of neural network dynamic models with sound approximation. In 6th Annual Learning for Dynamics & Control Conference. PMLR, 2024.
[46] Z. Shi, Y. Wang, H. Zhang, Z. Kolter, and C.-J. Hsieh. Efficiently computing local lips- chitz constants of neural networks via bound propagation. Advances in Neural Information Processing Systems, 1-2350-23644 2022.
[47] C. Liu, T. Arnon, C. Lazarus, C. Strong, C. Barrett, M. J. Kochenderfer, al. Algorithms for verifying deep neural networks. Foundations and Trends@ in Optimization, 4(3-4):244 404, 2021.
[48] S. Wang, H. Zhang, K. Xu, X. Lin, S. Jana, C.-J. Hsich, and Z. Kolter. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. Advances in Neural Information Processing Systems, 34:29909-29921, 2021.
[49] V. G. Rao and D. S. Bernstein. Naive control of the double integrator. IEEE Control Systems Magazine, 21(5):86-97, 2001.

---

[50] J. Reeds and L. Shepp. Optimal paths for a car that goes both forwards and backwards. Pacific journal of mathematics, 145(2):367-393, 1990.
[51] G. Wu and K. Sreenath. Safety-critical control of planar quadrotor. In 2016 American control conference (ACC), pages 2252-2258. IEEE, 2016.
[52] A. Madry, A. Makelov, Schmidt, D. Tsipras, and Vladu. Towards deep learning models resistant adversarial attacks. arXiv preprint arXiv:1706. 06083, 2017.
[53] A. Abate, D. Ahmed, A. Edwards, M. Giacobbe, and A. Peruffo. Fossil: a software tool for the formal synthesis of Iyapunov functions and barrier certificates using neural networks. In Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control, pages 1-11. 2021.
[54] H. Dai, B. Landry, L. Yang, M. Pavone, and R. Tedrake. Lyapunov-stable neural-network control. arXiv preprint arXiv:2109. 14/52, 2021.
[55] Y. Wang, C. Huang. Z. Wang. Z. Wang, and Q. Zhu. Design-wiile-verify: correct-by- construction control learning with verification in the loop. In Proceedings of the 59th ACM/IEEE Design Automation Conference, pages 925-933,2022
[56] Neuralverification... https: http://////g/aaaooo//////////aaa j1, 2021.
[57] Modelverifiiation...
httpe://ggaabbccca//nnllllggoooo
Mode_Verification. j1, 2024.
[58] a-B-crown. 2022.
[59] Wei, L. Marzari, K. Yun, H. Hu, P. Niu, X. Luo, and C. Liu. Modelverification. jl: comprehensive toolbox for formally verifying deep neural networks. arXiv preprint arXiv:2407.01639, 2024.
[60] S. Wang, Pei, Whitehouse, J. Yang, and Jana. Formal security analysis of neural networks using symbolic intervals. In 27th USENIX Security Symposium (USENIX Security 18), pages 1599-1614, 2018.
[61] T. Wei and C. Liu. Safe control with neural network dynamic models. In Learning for Dynam- ics and Control Conference, pages 739-750. PMLR, 2022.
[62] 7. Liu, G. Zhou, J. He, T. Marcucci, I.. Fei-Fei, J. Wu, and Y. Li. Model-based control with sparse neural dynamics. In seirth-e Conference on Neural Information Processing Sys- tems, 2023.
[63] H. Zhang, H. Chen, C. Xiao, S. Gowal, R. Stanforth, B. Li, D. Boning, and C.-J. Hsieh. Towards stable and efficient training of verifiably robust neural networks. arXiv preprint 19X.::9906.06166 2019.
[64] Z. Shi, Y. Wang, H. Zhang, J. Yi, and C.-J. Hsieh. Fast certified robust training with short warmup. Advances in Neural Information Processing Systems, 34:18335-18349, 2021.
[65] M. N. Müller, F. Eckert, M. Fischer, and M. Vechev. Certified training: Small boxes are all you need, arXiv preprint arXiv:2210.04877 2022.
[66] T. Wei, Z. Wang, P. Niu, A. Abuduweili, W. Zhao, C. Hutchison, E. Sample, and C. Liu. Im- prove certified training with signal-to-noise ratio loss to decrease neuron variance and increase neuron stability. Transactions on Machine Learning Research, 2024.
12

---

A Proofs
A.1 Proof of Proposition 1
Lemma 1 (Interval Arithmetic, restated from Section 4.1 in [47].). For any matrix multiplication
A x In + IRm",, if is entry-wisely bounded as x S x S x, X, S X2 S x, 1i n, the following inequalities hold for each entry of Ax,
[A]+X x + [ x < Ax < [A] X + [A]+X
(9)
where [+++ == m0, (0, -. 1- == min (0,
Proof. For the lower bound [A]+x + [A]-x, consider the j-th entry of [Ax]; = Ei= A With the entry-wise bounds x; S x; S Xx, Vi = I... n, A 2 0, holds that J S A similarly, if Aj < O, it holds that A S A Writing compactly, we have
[A + | x; = max {0, A 5 + min (0, },, S ,, By summing the inequality above over = 1..... n. holds that
[ + [[A]_|], E'Aul + EAA (Ax), Σ A
i=1
Ax holds for each entry j. Similarly, the upper bound Ax S [A]-x X + [A]+X x can be derived in the same way, concluding the proof the interval arithmetic.
which indicates [A]+x + [A]_x
Proposition 2. (restated of Proposition 1) When u is within hyper-rectangle U = Iu, u| {u E
Rm u 5 u ū}, given X E X. the minimum value of o(xx u) over u E U can be found explicitly
as,
min o(xx u) = vxOl f(x) + V g(x)l+u+ x [(x]--== ò(x, (x)), well
(10)
where [+]+ max [+]-]
0) and the optimal control input u. u.(x)
argmin (1) ă(x, u) lies among the vertices V(4) of hyper-rectangle U given state x.
Proof.
Based on the chain rule, it holds that
o(x, u) VxΦ x= VxO f(x) VxΦ Vx g()u..
With < u S T. based on Lemma 1, it holds that
[v 9(x) [1))++= (vx0 9(x)
V VxΦ g(x)u
Besides, consider the vertices V(4)= {u, [un]i {u, u. vi I,..., m). we can find the equivalent expression for the lower bounds.
[VxØ x( (Vx g(x)) u v g(x)u,
where [x)]; u, if x g(x)); 2 and (x)], u, if [V g(x)]e < showing that
there exists u, V (24) s.I. the lower bound [ + V g(x)) 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 E U, given a learned neural CBF 6(x) with ReLU activation functions, suppose the boundary state set OXg is the union of K hyper-rectangles AX as OX, A.2 Ax(0), then the following inequality maxxsax, minueu á(x, 1) + ax((x) S is satisfied if as a sound upper bound of V h((x, u.) + the following inequality holds for any x in each hyperr-retangle state set AX E A.G.
+ a 1- [h(x, u. )+ + + /xxx, uz)] + aΦ(x) SO, O, where [+]+ max(0, }} ReLU(*), [+]_ (i, -ReLU(-*), and d, d and h(x, u.), 1(x,, uv) are the lower and upper bounds of x and h(x, uv), respectively.
d 1+ [T(x, u.)]+ + [d 1+ Tu(x uo))
13

---

Proof. Based on Proposition 2, we have the following inequality hold for any AA E Ados
min é(x, u) (x max xEAX
O(x, (x)) + ax(x) S max o(x, un) + aσ((x, (11)
xEAx well
xE
where uy is an approximated constant vertex of optimal control imput ux) for sound upper bound of ((xx (x)) over A... Now with the bounded dynamics h(x, un) S h(x, u.) S 1i(x, uz),
by Lemma for any E AA' we have
é(x, u.) + aØ(x) = V @h(x. u.) + a - [V u.) V h u.)) + ax(x).
Besides, with the bounded gradient v V Σ d. the following inequalities hold
d S [V x
S [ - dd_.
Then applying Lemma for [V h(x u.) and [V h (x, u.), we further have the following inequality hold for any AX.
o(x, u.) s a 1+ [h(x, )+ + d 1+ [x(, u.) + | 1-[ u+)l+ + [d'1- [h(x, u=)l
Therefore, if for any x in each hyper-rectangle state set AX' E A&2 it holds that
d [T(x, ]+ + [d ++ [h(x, u 1- + | [4x, u. + |d | [xx, u,)] + aΦ(x) S 0, and then we have o(x, u.) + (x) < 0 for any x E AX. Combining Equation (11), we have
max min (x, u) + ax((x)= s max o(x, u.) + aΦ(x) 5, E AXg. XEAX uell
xEAX
Since the exact boundary of (xx) is the subset of all AX, i.e. OX2 C A& == U / A holds that
max min o(x, u) ax(x)= < xEBX, well
max max min o(x, u) + aσ(x) s 50,
ANEAN XEAX ueld
which concludes the proof.
Remark (Linearly bounded dynamics.). We remark that although the linear bounds of dynamics l(x,, uo), h(x, u.) can be found through 1-order Taylor models [42, 43, 44] in practice, we can give generally valid lower and upper bounds by assuming bounded & operator norm of Hessian matrix following [45]. For the control-affine system with fixed control input ug x h(x,, uo) with bounded state S X, suppose the &g operator norm Hessian matrix of i-th entry of h(x, uo) is bounded as | h ( (x, un]ll2 S M6),, then at xo E [x.x] the following linear bounds can be found as
1(x, Uo) = W + bo I 1(x,, up) S WoX + by = -T(xx, uo) where W W. = V h(xo, uo),
by
(8)
(1() (xo, Uo) V (X0, uo)xo デ | (1 for
i-t i-th entry of by
( 11 uo)
V un)x0
-1 x12 for i-th entry of bo.
D
Specifically, if the control-affine system is linear and time innarinnariant,, i.e. f(x) = Ax and g(x) = =B with constant A, B, where the lower and upper bounds will trivially be Wo = Wo A, b, =
Dy = Bu,.
B Experiments
In this work, symbolic bounds are bounds that are linearly related to the input specification, com- pared to the concretized bounds where the input dependencies are thrown away. Besides, if a sound but incomplete verifier returns 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 to develop tighter sound and incomplete verification with symbolic bounds.
14

---

grids per dimension
grids per dimension
grids per dimension
1,0
1.0
1.0
0.8
0.8
Velrted Rate
Veinted Rate
0.6
Velrfed
0.8
0.4
0.4
BBV
BBV
BBV
0.2
Ours
0.2
Ours
Ours
Upper bound
Upper bound
Upper bound
oi
0.6
1.0
verification condition
verification condition
verification condition
grids per dimension
grids per dimension
grids per dimension
1.0
1.0
1.0
0.8
0.8
Veirted Rate
Veirfeed Rate
Velrfed
0.8
0.4
BBV
BBV
BBV
0.2
Ours
0.2
Ours
Ours
Upper
Upper bound
Upper bound
08
0.6
0.2
1.6
in verification condRtan
verification condition
verification condition
Figure 5: Verified rate with different in the neural CBF verification condition using different grid sizes (different number of boundary hyper-rectangles) for Dubins Car.
B.1 Experiment Environments and Dynamics
All the robot dynamic models are based on the open-sourced package RobotZoo.jl, where Point Robot is modified based on DoubleIntegrator (D=2) with zero gravity, Dubins Car is mod- ified based on DubinsCar with radius=0. 175, and Planar Quadrotor modified based on PlanarQuadrotor with mass=1. 0kg, gravity=9. 81m/s² and tip-to-tip distance=0.cr 3m. Moreover, for the state space. all robots move on 2D plane within (0,4m) (0, (hori- zontal for Point Robot and Dubins Car but vertical for Planar Quadrotor) with a static rect- angle obstacle located at the center coordinate (2m, 1m) with sizes of 1m*2m. More specif- ically, the states of Dubins Car are 2D positions and orientation angle within the 3-dim hyper-rectangle (0,4) * (0,4)) (0,z) and the unsafe states are within 3-dim hyper-rectangle (1.5,2.5) 55, (0, (0, x). The states of Point Robot are 2D positions and 2D velocities within the 4-dim hepernle (0, (0, (0,,4)(( (-1,,,,,))))) 1)*(-1, 1) and the unsafe states are within 4- dim hyper-rectangle (1.5,2.5) (0, 2), ()*(11, 1). The states of Planar Quadrotor are 2D positions, orientation angle. 2D velocities and angular velocity within the 6-dim hyper-rectangle (0,4) (0, 4) * (-0.1, (-1,1)))1 (-1, 1) and the unsafe states within 6-dim hyper-rectangle (1.5,2.55 inputs, Dubins Car adopts speed and angular speed within the 2D rectangle (-1,1))(-1,1), Point Robot adopts 2D accelerations as control input within the 2D rectangle (-1,1)+(-1,1) Planar Quadrotor adopts the thrust forces exerted by the two motors as control input within the 2D rectan- gle (4, 6) (4,6) to overcome its gravity and move on the vertical plane.
1)*((1, 1). For the control
B.2 Implementation Details
Data collection. As shown in the main text, we adopt supervised learning train the neural CBFs. The data is collected from random trajectories from the safe state space and control input space through the dynamics. To empirically ensure the forward invariance, we discard the second half states and control inputs to avoid the unsafe region of attraction, and only collect the other states and control inputs with the safe labels. To collect unsafe data, we collect random states from the unsafe state space with a similar amount of safe data for balance. To more detailed, the time of random trajectory is 10s with the time step of 0.1s and the states in the last 5s are omitted. Also, the trajectories that are less than 5s (e.g. when the robot collides with obstacles goes beyond the feasible states) are discarded as well. By repeatedly initializing random states and collecting
15

---

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 Number of grids per dimension
10
20
50
100
Ours w/o BaB
0.329
0.437
0.875
0.953
Regular training
Ours w/ BaB
0.507
0.729
0.926
0.963
Ours w/o BaB 0.247
0.592
0.837
0.910
Adversarial training
Ours w/ BaB
0.519
0.730
0.899
0.941
Table 3: The ablation study of the and-bound (BaB) in our proposed method under different grid densities with a 0.5 for Dubins Car.
trajectories with random control inputs through dynamies, we collect 2.5M total pairs of state and control input with 1.4M safe ones for Point Robot, 4.5M total pairs with 2.5M safe ones for Dubins Car and 1.2M total pairs with 0.7M safe ones for Planar Quadrotor as dataset. Then, we randomly choose 10k data as validation set and use the rest for model training for each robotic dynamics.
Model training. During the model training, we adopt the empirical mean of the positive model predictions as the safe set loss [17] and use the projected gradient descent to find the best-case control input to construct the forward invariance condition loss. To enhance the training efficiency, we only consider the training data along the empirical boundary of [Ø(x) < 0.1 for forward invariance condition loss with a 0. For adversarial training. we adopt project gradient descent over an adjacent cube of each state data to maximize the forward invariance loss, then the gradient descent is based on the worst-case projected states. The size of the adjacent cube in the adversarial training is 1/20 of each dimension. All the models are trained with Adam for 20 epochs with an initial learning rate of 0.01 and a decay rate of 0.2 every 4 epochs. The neural CBFs for Planar Quadrotor are trained with the weight decay 0.001.
Verification procedure. The first step of verifying neural CBFs is to find the hyper-rectangles
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.ji [43]. Then with the Jacobian bounds [46], the condition in Theorem 3 is found to verify if it is no larger than O. If it does not hold, we adopt branch-and- bound 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 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.
B.3 Additional Results and Analysis
Comparison with different a in the verification condition. As shown in Figure 5, we compare our results and the branch-and-bound based baseline BBV [36] with different a 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 a, the performance of BBV decreases more than ours due to larger over-approximation errors. The reason why results get
16

---

Results after 1st rtänn
ppittinng
splitting
sp Itting
splitting
1.00 1m
Fortes
&
Hoetas
Pooton
Results after 1st sp rtting
splitingg
sp ltting
1400
4:00
Yauton
1.07
Figure 6: Visualization of branch-and- bound for both baseline BBV [36] (first row) and ours (second row) for Dubins Car with regular-training CBF and u, [1, 1]. For each branch after splitting, the green boxes indicate verified specifications while the red ones indicate unknown specifications.
better when goes up lies in that the approximation errors 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 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 Branch-and and--Bund (BaB) on the proposed method. Here we conduct an experi- ment as an ablation study to show the influence of branch-and-boune in the proposed method. As shown in Table we can find that without wranch-and-bounde the performance is significantly re- duced, especially with fewer boundary hyper-rectangles (larger sizes of grids), showing that branch- and-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-hound scheme. From Figure 6, we can see that after each splitting for the previous unknown specifications, branches will be doubled and the branch-and-bowd follows breadth-fire search. With fewer split branches. 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 splits while BBV only verify some of the finer specifications, leaving lots of unknown branches to be further split due to looser bounds and larger over-approxination. The visualization shows that even though with the same approximated optimal control input u,, 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 Relu Val [60] also based on symbolic bounds and adopts iterative interval refinement, we fairly compare it with CROWN-based baseline BBV [36] and with branch-and-boune in Table 4. The experiment is conducted under Dubins Car dynamics with the same amount of maximum split times (1000) of BFS and 10 grids per dimension for input specs. From the result table, we can see that ours still has the best performance. With the default size (16,64.1611 model, ReluVal performs better than BBV and keeps on par with ours, showing that symbolic ReluVal bounds work well with relatively small model complexity. However, with a larger model size (64, 12,,6288, 1) and more unstable ReLU neurons, the bounds of Relu Val become looser, and ReluVal is more likely to perform worse than CROWN-based methods. The main reason lies in different symbolic bounds for crossing- -erso zero unstable ReLU layers. Ours and BBV adopt fully linear symbolic bounds as CROWN does, while Relu Val only adopts symbolic
17

---

Verfication condition
0.1
0.5
1.0
Model size
Default
Large
Default
Large
Default
Large
BRV [36]
0.450
0.564
0.371
0.486
0.357
0.329
ValuVal [60]
0.471
0.557
0.507
0.479
0.536
0.450
Ours
0.486
0.593
0.507
0.564
0.536
0.486
Table 4: Comparison between CROWN-bate baseline BBV [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 O. Therefore, CROWN-like symbolic bounds are generally tighter than ReluVal [48].
C Limitation
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-aftine) 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 involve robust certified training techniques [63, 64, 65, 66), to enhance the scalability of verification, c.g., new loss from verification conditions, reducing the number of unstable neurons, etc. Future work could also incorporate the linear bounds into verification -nnoon-ii-ttee -ee-iii--ttt-oot tho-loop training for verified neural CBFs in real-world applications.
18


Reviews:
[{"review_id": "KNBB1AjUYC", "reviewer": "Reviewer_sbF7", "summary": "", "questions": "", "limitations": "", "rating": 2, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": 2, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "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", "summary_of_recommendation": "The proposed method is incremental and scales poorly to robots with high-dimensional state spaces.", "technical_quality": 2, "clarity_of_presentation": 3, "potential_impact": 2, "robotics_focus": 2, "quality_of_limitations": 2, "questions_for_rebuttal": "(1) What is the difference between $\\phi$ and $\\phi_\\theta$ (it seems the paper is using interchangeably without any mention of that)? \n\n(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?\n\n(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.\n\n(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?", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "0QBmKS9kQ8", "reviewer": "Reviewer_KbLk", "summary": "", "questions": "", "limitations": "", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": 4, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "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.", "summary_of_recommendation": "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.", "technical_quality": 5, "clarity_of_presentation": 5, "potential_impact": 4, "robotics_focus": 3, "quality_of_limitations": 3, "questions_for_rebuttal": "1.\tPlease explain the meaning of “symbolic”  and  “incomplete verification” somewhere in the manuscript (for readers who are not in the field of verification)\n2.\tPlease explain how to compute $\\dot \\phi(x)$ (to compute the control signal) when $\\phi(x)$ uses a ReLU function.\n3.\tIn the paragraph right below Theorem 2, it mentions “the optimal control input u is approximated…”. Where does the approximation come from?", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "57uyRnB73l", "reviewer": "Reviewer_mp6J", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": 3, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "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.", "summary_of_recommendation": "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.", "technical_quality": 3, "clarity_of_presentation": 5, "potential_impact": 3, "robotics_focus": 3, "quality_of_limitations": 2, "questions_for_rebuttal": "- The reviewer believes it should be clarified in the abstract that the proposed method is specific to ReLU-activated MLPs.\n - It is not clear how the optimization over the state space in Equation (7) and in Example 1 is achieved.\n - 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?\n - What factors influence the magnitude of the overapproximation errors during the bound computation?\n - It is unclear to the reviewer how the $\\textit{approximated}$ control input is computed, e.g., in Example 2. \n - 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?", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: 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.
Decision: Accept