Exact Verification of ReLU Neural Control Barrier Functions
Authors: Hongchao Zhang
Junlin Wu
Yevgeniy Vorobeychik
Andrew Clark
Venue: NeurIPS 2023 poster (2023)
Keywords: Safety
Neural Barrier Function
Verification

Abstract: Control Barrier Functions (CBFs) are a popular approach for safe control of nonlinear systems. In CBF-based control, the desired safety properties of the system are mapped to nonnegativity of a CBF, and the control input is chosen to ensure that the CBF remains nonnegative for all time. Recently, machine learning methods that represent CBFs as neural networks (neural control barrier functions, or NCBFs) have shown great promise due to the universal representability of neural networks. However, verifying that a learned CBF guarantees safety remains a challenging research problem. This paper presents novel exact conditions and algorithms for verifying safety of feedforward NCBFs with ReLU activation functions. The key challenge in doing so is that, due to the piecewise linearity of the ReLU function, the NCBF will be nondifferentiable at certain points, thus invalidating traditional safety verification methods that assume a smooth barrier function. We resolve this issue by leveraging a generalization of Nagumo's theorem for proving invariance of sets with nonsmooth boundaries to derive necessary and sufficient conditions for safety. Based on this condition, we propose an algorithm for safety verification of NCBFs that first decomposes the NCBF into piecewise linear segments and then solves a nonlinear program to verify safety of each segment as well as the intersections of the linear segments. We  mitigate the complexity by only considering the boundary of the safe region and by pruning  the segments with Interval Bound Propagation (IBP) and linear relaxation. We evaluate our approach through numerical studies with comparison to state-of-the-art SMT-based methods. Our code is available at https://github.com/HongchaoZhang-HZ/exactverif-reluncbf-nips23.

Exact Verification of ReLU Neural Control Barrier Functions
Hongchao Zhang
Junlin Wu
Electrical & Systems Engineering
Computer Science & Engincering Washington University in St. Louis
Washington University in St. Louis
St. Louis, MO 63130
St. Louis, MO 63130 junlin, wu@wustl. edu
hongchao@vustl.cm edu
Yevgeniy Vorobeychik
Andrew Clark
Computer Science & Engineering Washington University in St. Louis
Electrical & Systems Engineering
Washington University in St. Louis
St. Louis, MO 63130
St. Louis, MO 63130
yvorobeychikewustt.. edu
andresclarkk@wustl. edu
Abstract
Control Barrier Functions (CBFs) are popular approach for safe control of nonlinear systems. In CBF-based control, the desired safety properties of the system are mapped nonnegativity of CBF, and the control input is chosen the CBF remains nonnegative for all time. Recently, machine learning methods that represent CBFs neural networks (neural control barrier functions, NCBFs) have shown great promise due to the universal representability of neural networks. However, verifying that a learned CBF guarantees safety remains a challenging research problem. This paper presents novel exact conditions and algorithms for verifying safety of feedforward NCBFs with ReLU activation functions. The key challenge in doing so is that, due to the piecewise linearity of the ReLU function, the NCBF will be nondifferentiable at certain points, thus invalidating traditional safety verification methods that assume a smooth barrier function. We resolve this issue by leveraging a generalization Nagumo's ' theorem proving invariance of sets with nonsmooth boundaries to derive necessary and sufficient conditions for safety. Based on this condition, we propose an algorithm for safety verification of NCBF's that first decomposes the NCBF into piecewise linear segments and then solves nonlinear program to verify safety each segment as well as the intersections of the linear segments. We mitigate the complexity by only considering the boundary of the safe region and by pruning the segments with Interval Bound Propagation (IBP) and linear relaxation. We evaluate approach through numerical studies with comparison to state-of-the-an art SMT-based methods. Our code is available at at|htpps; //github. com/ wwt.:occccccceeeeeeeee /ww///ooonnhhgnggggee.ee HZ/ eeeeeeecterifff.ooo reluccbrrrerrffro wwtamnffffipsee -nips23
that
Introduction
Safety is a critical property for autonomous systems, including unmanned ground, acrial, and space vehicles [1] and robotic manipulators 22. The importance of safety has motivated extensive research into verification and synthesis of safe control strategies [ 4 S 6, 77]. Control barrier function (CBF)-based algorithms [8] ensure safety by constructing a CBF that is nonnegative if the system is safe and synthesizing control policy that ensures that the CBF is nonnegative for all time. Control barrier functions provide high degree of flexibility, since any control policy that satisfies the control barrier function constraint is provably safe, and have been demonstrated in applications including
37th Conference on Neural Information Processing Systems (NcurIPS 2023).

---

robotic manipulation [9]. vehicle cruise control [0] and space exploration [.]. Recently, CBFs that are parametrized by neural networks (neural control barrier functions or NCBFs) L3 [4
have been proposed. This novel class of NCBFs is promising due to the universal representability of neural networks (enabling the encoding of complex safety constraints) and the efficiency of learning algorithms, with a comparison in Section A.15 exemplifying numerical difference. However, safety verification of NCBF-based control remains a challenging research problem.
In this paper, we consider the problem of verifying safety of NCBI--based control for nonlinear continuous- time systems. We focus on NCBFs represented by feedforward neural networks with ReLU activation due to their fast convergence in training shown in Section A.16 and widespread use in the safe control literature [12 B.. The key challenge for this class of NCBFs is that most methodologies for safety verification are based on proving that the derivative of the barrier function nonnegative at the boundary of the safe region, and hence the barrier function remains nonnegative for all time. Since the ReLU activation function is not continuously differentiable, this approach inapplicable. We resolve this challenge and derive exact safety conditions for ReLU NCBFs by leveraging a generalization of Nagumo's 's theorem for proving invariance of sets with nonsmooth boundaries. Based on these conditions, we propose a new class of NCBF-based control policies that do not require the control policy and NCBF to be jointly trained, thus improving flexibility and tunability of the controller design. Our safety conditions also incorporate linear constraints on the control input, which may arise due to limits on actuation.
We propose an algorithm to verify that an NCBF satisfies our derived safety conditions, implying that any control policy that is constrained by the NCBF will be safe. Our approach first decomposes the NCBF into piecewise linear segments. In order to mitigate the complexity of this stage, we show that it suffices to consider linear segments at the boundary of the safe region, and further over-approximate the segments using Interval Bound Propagation and linear relaxation. After decomposing the NCBF, we verify safety by solving a set of nonlinear programs, which check the safety criteria on each linear segment as well as at intersections of the segments. We evaluate our approach through numerical studies, in which we verify NCBFs with our proposed approach and compare to state-of-the-art Satisfiability Modulo Theory (SMT) based methods.
Related Work Energy-based methods have been proposed to guarantee safety by ensuring that a particular energy function remains nonnegative. Barrier certificates for safe control were first proposed in 15. More recently, CBFs have emerged as promising approaches to safe control, due to their compatibility with a wide variety of control laws [8] 16 17
12 Sum-of-squares (SOS) optimization and other techniques derived from algebraic geometry have been widely used for safety [7]. However, SOS-based approaches for
verification of polynomial barrier functions [15 8 polynomial CBFs cannot be applied directly to NCBF verification, since activation functions used in neural networks are not polynomial and may be non-differentiable.
18
19
Neural barrier certificate (20 21 22 23 and NCBFs [12 13 [4] have been proposed to describe complex safety constraints that cannot be encoded polynomials. Current work, including SaT-based methods [24] 21 [5] and mixed integer programs (26.. verify safety by constructing a nominal control policy and proving that it satisfies the NCBF constraints. However, as we show in Section [5] the reliance on a particular control policy may lead to false negatives during safety verification. Another related body of work deals with the problem of verifying neural networks including SMT [27).
output reachable set verification (28) polynomial approximations of the barrier function [29], verify
input/output relationships (30, 32 and ReLU neural networks focused verification [33 34].
These methods, however, are not directly applicable to the problem of NCBF verification, which requires joint consideration of the neural network and the underlying nonlinear system dynamics. Methods based on input/output relationship can verify by encode dynamics and control policy with neural networks. However, with approximating error introduced, these methods are not directly applicable for exact verification. Piecewise linear approximations of ReLU neural networks have been used to develop tractable safety verification algorithms using linear 335 and SOS programming (36. These approaches leads to sound and incomplete verification algorithms and have only be applied for discrete-time systems, whereas the present paper proposes exact verification algorithms for continuous-time systems.
Organization The remainder of the paper is organized as follows. Section gives the system model and background on neural networks and notation. Section 3 presents the problem formulation and
2

---

exact conditions for safety. D our approach to verifying that an NCBF satisfies the safety conditions. Section ceatioonScontionnn contains simulation results. Section 6 concludes the paper.
2 Model and Preliminaries
In this section, we first present the system model and definition of safety, We then give background and notations of feedforward neural networks.
2.1 System Model and Safety Definition
We consider a continuous-time nonlinear control-aftine system with state z(t) E X C R", control input u(t) U C RT" and dynamics
(()) (((())))(((())((())
where f: : R- + I2" and g IR + Ruxm are known functions. A control policy is a function IR +4 that maps state control input
Safety of dynamical systems requires r(t) remain in a given region C, which we denote as the safe region. We assume the safe region is given by C = {x : h(x) 2 0} C X, for some function h: X' + R. Safety is related the property of positive invariance, which we define follows.
Definition 1. A set D C I is positive invariant under dynamics 4 and control policy μ x0) D and u(t = ((x(tt) Vt 2 imply that z(t) E 'D for all 2 O.
We define a control policy μs be safe if there is set D such that (i) D and (ii) D is positive invariant under dynamics ① and control policy Jr.
One approach to designing safe control policies is to choose function b: IR" R. denoted as Control Barrier Function (CBF), and let = {x: : b(x) 2 0}. In the case where b continuously differentiable, the following result be used to guarantee positive invariance of D.
Theorem
( Suppose that is CBF, b(x())) 2 O. and u(t) satisfies
ab (f(z) + g(x)u) 2 abb(z))
dx
for all t, where a R R. is a strictly increasing function with a()) 0. Then the set b(x) 2 0} is positive invariant.
{o
Theorem Timplies that, if b a CBF, then adding 2 as constraint on control at each time step suffices to guarantee safety.
Recently, Neural Control Barrier Functions (NCBFs), in which the function b is encoded by a neural network, have been proposed [12, 13 14] The advantage of NCBFs arises from the universal representability of neural networks, which allows them realize wide variety of safety constraints.
2.2 Neural Network Background and Notation
We give notations to describe a neural network (NN) with layers and Mf neurons in the i-th layer. We let the input to the NN be denoted x, the output at the j-th neuron of the i-th layer be denoted 2ij. and the output of the network be denoted y. We let z; denote the vector of neuron outputs at the i-th layer. The outputs computed as
2ij {{
o oW + +Tg), o (W 2-1
i=1 iE 12
- z7 + +
(3)
where a : RR + R is the activation function. The input to the function is the pre-activation input to the neuron, and is given by W7,-+ - F1 for the j-th neuron at the first layer and W () zj-1 + for the j-th neuron at the i-th hidden layer. Wi has dimensionality n X for = 1 and M;-1 x 1 for i > 1. W; is an n x M; matrix. this paper, we assume that a the ReLU function (z) = max (0, The output of the network is given by y Ω zz. + w. where Ω Rdd and 1 E R. The j-th neuron the i-th layer is activated by particular input x its pre-activation input nonnegative, inactivated if the pre-activation input is nonpositive, and unstable if the pre-activation input is zero.
3

---

A set of neurons S = (Si..... S,), with S; C (l...., M;) denoting a subset of neurons at the i-th layer, activated by z if all of the neurons inactivated by z. A set of neurons T = (Tı,.... TT.) with T; S (1....,M, M,} is unstable by if all of the neurons in T are unstable by æ.
are activated by x and all the neurons not in are
For given set S, if S is activated by z, then the pre-activation input to each neuron and the overall output of the network are afline in x, with the affine mapping determined by S as follows. For the first layer, we define
W (5)(S) = = W1y jE Si Ti5(S) - mij. j E S1 else
else
so that the output of the j-th neuron the first layer W (S) +i)( We recursively define Wiy(S) (S) and Fiy(S) by letting (S) be a matrix with columns W (S)....... W. W.M, (S) and
Wey (S)( = {
W WS) jE S
Fiy(S) = { w + Tijs j E S
(5)
0, where (S) is the vector with elements r:j (S). = ,,..., M,
0,
else
else
define W(S) - (S) and (''r, + vb. Based on these notations, when an input J activates the set S, 2ij = W, (s)(
(S) and = W(S) + r(S).
Lemma Let (S) denote the set of inputs x that activate a particular set of neurons S, and let WS(S) be equal to the identity matrix, and ty to be zero vector. Then
P(S) = n n
(o: W W. W..1(S)) +1-11 rij 2 20
jES,
(a: W W (W-1(S)) +---1) + ray S 00) (6)
JæS.
A proof can be found in the supplementary material. Note that in (6) a particular input x could belong to multiple activation regions (().. This is because if the j-th neuron at the i-th layer is unstable, then both (S,,..,, S, U ( Sr.) and (Si, (Si,..., S: (i).... Sr.) can be regarded as activated by x. We let S(x) & (S x E X((S) and let T(x) denote the set of unstable neurons produced by input z. Given collection of activation sets S,...., Sp, we let
Ü.$) S:
(Ns)
V=1
1=1
The set .(S is equal to the set of neurons that must be unstable in order for an input x to belong to (()))) n... (((.)..
3 Problem Formulation and Safety Conditions
In this section, first formally define the problem, and then give necessary and sufficient conditions for verifying NCBFs.
3.1 Problem Formulation
We consider feedforward neural network (NN) b: X + R with ReLU activation function. Since b not continuously differentiable due to the piecewise linearity the ReLU function, the guarantees of Theorem I cannot be applied directly. Our overall goal will be to derive analogous conditions to 2 for UTNCFF and then ensure that any control policy μ that satisfies the conditions will be
safe with D {x b(x) 2 0}.
Problem 1. Given a nonlinear continuous-time system D. a neural network function b + R, set of admissible control inputs 21 = (u Au < <) for given matrix A E Rpxm and vector E TR. and a safe set {x h(x)) 2 0}, determine whether (i) C C and (ii) there exists a control policy such that D is positive invariant under dynamics and control policy p.

---

3.2 Exact Conditions for Safety
When a CBF b(x) is continuously differentiable, ensuring that 2 is satisfied is equivalent to verifying that there is no satisfying b(z) dz
Øb and tx f(x) < 0 [77. When is represented by a ReLU neural network. however, b will not be differentiable when the input x leads to neurons having zero pre-activation input, i.e., when T(x) * 0. Although the set of a with T(x) A has measure zero, such points can nonetheless cause safety violations as illustrated by the following example.
Øb g(z)
Example: Let sxt) E ? and suppose the dynamies of given by
2 (t)
21 + -11 + 5.2
+ -f(x) - 5 2, g(x) )
(1))) (11
22 (t) =
Suppose that U R the safe region C= fo : i + x 99, and the candidate CBF is given by b(x) - |x|||- This CBF can be realized by a neural network with single layer (L = 1) with four neurons (M1- 4), weights W11 (1 W1 rij = 0 for ,,, S2 -1 for j - 1..... 4, and & = 1. We observe that D = {x: b(x) 2
(-1 (-10)² W13 13 = (0 1)" W14 (0 1)
0} S C. Furthermore, whenever 0b
(1 - (-11), (-1 - -))] each of which satisfies @ gxxx + O. On the other hand, the set D is not positive invariant. If x0)
8a exists, we have db dr
then xz) (0) < 1 implies that (0) > O, and indeed, T2 will continue to increase until xxl) $ D. More details about this example can be found in Section A.17
Fundamentally, this safety violation occurs because at x = (0 1)²,, we have b(x) = 0. T(x) = {(), (1, (i.e., the preactivation input to the first and second neurons in the hidden layer is zero), creating a discontinuity in the slope of 6(z). For in the neighborhood of (0 1)""." the value of
2h dz (x') will be either 1 or 1. Since there is no single control input that satisfies 2 for both
values of 8b
oz 9(x', it is impossible to ensure safety of the system in the neighborhood of (0 1)²
The following lemma addresses this issue by giving exact and general conditions for NCBF with ReLU activation function to satisfy positive invariance. We let ÖD denote the boundary of the set D.
Lemma 2. The set D is positive invariant under control policy p. if and only if. for all x E OD, there exist S E Six) such that
(S))
2
v(i,) E T(
W (S(,, (f())((())) (()) 20
5o T(a))
(8)
(9)
The proof is based on the generalized Nagumo's Theorem 37 and novel characterization of the Clarke tangent cone to @D, and can be found in the supplementary material due to space constraints. Intuitively, conditions (7) () can be interpreted as follows. Condition (9) is similar to (2) when the gradient is given by (S), i.e., when is in the interior of the activation region defined by S. Eq.
(7) {8) can be interpreted as choosing the control input to ensure that x remains in the activation
region of S (i.e., {())..
Lemma can be used to construct NCBF-based safe control policies, analogous to control policies based on continuously differentiable CBFs. Formally, given a nominal control policy Unoms each time t, we can choose utt) by solving the optimization problem
minseS(ar..
||u Pnom (2t)
s.t.
( + ((x)(())) 2 -a(b(x))
(10)
u E U,
where a satisfies the same conditions as in Theorem
1 This problem can be solved by decomposing (10) into [S(xr) quadratic programs (one for each S) and then selecting the value of u that minimizes the objective function across all of the QPs. In particular, if ((x) is singleton, then the constraints on (IO) reduce to Eq.
We then give equivalent condition for b(x) to be an NCBF, As preliminary, say that collection of activation sets Si...., S, is complete if for any S' & (Si...., S,),, we have X(S)) n
... ...,X((s)) (((S)) 0.
5

---

Proposition 1. The function b is a valid CBF itf the following two properties hold:
(i) For all activation sets St..... and
......... S, with (Si...., complete and any satisfying b(x)
{}(()))
(11)
there exist E (1,....r) and u E U such that
(S),(S,) ((x)u) 2 0 v(.j) E T(S).....S.)nS..
(12)
(f( +
00
v(i.) E T(S.....,,..))) \
(13)
(14)
(ii) For all activation sets S, we have
(X (D) -C
(15)
The proof can be found in the supplementary material. We refer to any æ that fails to meet least one of conditions (i) and (ii) of Proposition safety counterexample.
Enumerate
S, = [110 1
Sg
[1 110 ..
100
[111 00
[11
0.]
Prume
(1/
S, [101
S, [111
00]
For each coll containing multiple 8'E
Gridily the state space and find cells that cross C-level eet
For each cell use IBP fsl possibte activated
Use linear program to find exact activated
8. use Linear Program Intersection V
Figure 1: Illustration of proposed coarser-to-finer searching method. Hyper-cubes that intersect the safety boundaries are marked red. When all possible activation sets are listed, we can identify exact activation set and intersections.
4 Verification Algorithm
The preceding proposition motivates our overall approach to verifying NCBFs, consisting of the following steps. (Step 1) We conduct coarser-to-finer search by discretizing the state space into hyper-cubes and use linear relaxation based perturbation analysis (LiRPA) identify grid squares that intersect the boundary {# b(x) = 03. (Step 2) We enumerate all possible activation sets within each hyper-cube using Interval Bound Propagation (IBP). We then identify the activation sets and intersections that satisfy b(x) = 0 using linear programming. (Step 3) For each activation set and intersection of activation sets, verify the conditions of Proposition] I In what follows, describe each step in detail.
4.1 Enumeration of Activation Set Boundaries
We next present the approach to enumerate activation sets of a given ReLU NCBF that intersect the safety boundary, 6(x)
Our approach first conducts a coarse-graines search that over- approximates the collection of activation sets that intersect with the safety boundary. We then prune this collection to remove activation sets that cannot be realized. Specifically, we first identify regions that contain b(x) = 0, then enumerate all possible activation sets within the region and finally identify the sets that intersect the safety boundaries.
We first discretize the given state space X' into hyper-cubes. We compute lower and upper bounds of b(z) each hyper-cube, denoted and 6, respectively, with linear relaxation based perturbation analysis (LiRPA), i.e., auto LiRPA 38 For each hyper-cube B. we determine B contains b(x:) = 0 (red squares in Fig Dh criteria sgn((b) (b:) sgg(bb.) S 0 holds, where sgn(*) is the sign function. For each B contains b(z) = O, we utilize IBP to over-approximate unstable neurons. Details on this IBP
procedure can be found in Section A.7
Let S denote the over-approximated collection of activation

---

sets computed by IBP. Note that S E & may not intersect with b(x) = 0. As shown in Fig. S denote the collection of activation sets S S that satisfy
we let
W(S) +
(W. (SW.( 2 0V((,) S ( ",, S OV(1,) E
(16)
for some x E B. The activation set boundaries indicate unstable neurons, which need to be verified separately. Hence, we search for intersections follows, where 2 denotes the set of subsets of S.
v { E 28:
X SEZ
fæ : b(x) = 03 +
4.2 Verifying Safety of Each Activation Set
With the activation sets enumerated, the following result gives an equivalent condition for verifying that there is no safety counterexample in the interior of (S) for given activation set S.
Lemma 3. There is no safety counterexample in the set X(()) Us+s X(S) if and only if:
1. There do not exist E X and y Re+1 satisfying (a) x E int (S())) (b) b(x) (c)
y 2 0, (d) (d) (
-W g(x)))))))))))){))) ) O. and (n) y" W(S) <0.
A
2. There does not exist E X with b(x) = 0, x E int (S))), and h(x) <
The proof can be found in the supplementary material. Conditions and of Lemma (aamma33cr can be verified by solving nonlinear programs (see supplementary material for the formulations of these nonlinear programs). Such nonlinear programs are solved for each activation set S in the collection S computed during the enumeration phase. The following corollary describes the special case where there constraints on the control, i.e., U = R
Corollary 1. IfU= = gmm then there no safety counterexample the set X(S) Us X('') if and only (I) there does not exist x E X satisfying in)() b(x) O. W(S) g())) and WSS fx) < 0 and (2) there does not exist I E X with b(x:) 0, x E inr( and h(x) 0.
Under the conditions of Corollary the complexity of the verification problem can be reduced. If g(x) a constant matrix G. then safety is automatically guaranteed W(S) G # 0. If f(x) is linear in well, then verification can be performed via linear program.
4.3 Verification of Activation Set Intersections
With the activation set boundaries enumerated, we now describe an approach for verifying safety of intersections between activation sets.
Lemma 4. Suppose that the Si,..., S, satisfy condition (üi) of Lemma 3
There no safety
counterexample in the set
(.((s)
U
X(S')
(S..
if and only if there do not exist & X and "i..... Vr T where T =
satisfying (a) E int(x n.... in (b) b(x) = 0, (c) > 0 Vl, (d) vI I,...,,, yt (S) (S,,..,,.((())) = O, where (S, S.. is (T (T+p+1) m matrix
S.,
-(W, (.., (S. (o(z) (i.j) T(S n,
(W. (W.,(S))W,, (x() ((s...)
T(S
S.)
Os(S,...., s,,
(17)
- (( (" g(z)

---

and (e) 1A = -........ AS .,, < O. where (S........................... S, E RT+++I is given by
(W (S),( (t.)) ( SS,,...,,,))s,, (W.-1(S))W.,) f(r)) (i.j) E T(S S,) f()))
(18)
The proof can be found in the supplementary material. The verification problem can be mapped to solving nonlinear program. This nonlinear program is solved for each (S....., S,)) E V. where V computed during the enumeration phase. Note that, if g(x) is constant, then the constraints of the nonlinear program are linear, and if f(x) is linear then the problem reduces to solving system of
linear and bilinear inequalities. Furthermore, if [1x: can be bounded over ((())) n - and b(x) = 0, then this bound can be used to derive a linear relaxation to the objective function of (27). thus relaxing the nonlinear program
linear program.
The complexity of this approach can also be reduced by utilizing sufficient conditions for safety that easier to check. For instance, if there exists u u such that W (S)) (f(x) + g(x)u) 2 0 for all S E S(x),, then the criteria of Lemma are satisfied. In particular, if W(S) [(x) for all
E S(x), then the conditions are satisfied with = 0. The following result is a straightforward consequence of Proposition] T Lemma and Lemma
Theorem 2. Suppose that the conditions of Lemmal Bare satisfied for each S E S and the conditions of Lemma f are satisfied for each (Si,...,S, E Then the NCBF satisfies the conditions of Problem
5 Experiments
In this section, we evaluate our proposed method to verify neural control barrier functions three systems, namely Darboux, obstacle avoidance and spacecraft rendezvous. The experiments run on a 64-bit Windows PC with Intel i7-12700 processor, 32GB RAM and NVIDIA GefFrce RTX 3080 GPU. We include experiment details the supplement.
5.1 Experiment Setup
We consider the Darboux system 33 nonlinear open-loop polynomial system that has been widely used as a benchmark for constructing barrier certificates. The dynamic model is given in the supplement. We obtain the trained NCBF by following the method proposed in (24].
Darboux:
Obstacle Avoidance (OA): We evaluate our proposed method a controlled system 40 We
consider an Unmanned Aerial Vehicles (UAVs) avoiding collision with tree trunk. We model the system as a Dubins-style [4]] aircraft model. The system state consists of 2-D position and aircraft yaw rate æ := [x1, 12, v..". We let denote the control input to manipulate yaw rate and the dynamics defined in the supplement. We train the NCBF via the method proposed (44 with assumed be and the control law designed as u Mnom (x) sin + 2i 1-+-22-008
0.5+2f+uū
Spacecraft Rendezvous (SR): We evaluate our approach on a spacecraft rendezvous problem from [22. A station-keeping controller is required to keep the "chaser" satellite within certain relative distance to the "target" satellite. The state of the chaser is expressed relative to the target using linearized Clohessy- Wiltyy-riitteeeeeeeee Hill equations, with state [P.. Py. Pay Ug By uz]"". control input [uz My. u and dynamics defined in the supplement. We train the NCBF as in [3]
hi-ordg: We evaluate our approach on an eight-dimensional system that first appeared in 21 to evaluate the scalability of proposed verification method.
5.2 Experiment Results
We first verify that D C in the Darboux and obstacle avoidance scenarios. We trained four hidden layer NCBFs with 20, 5, 32, 10 neurons, respectively. NCBF (a) and (c) completed training, (b) terminated after 3 epochs and (d) terminated after 5 epochs. Our verification algorithm identifies safety violations. NCBF (a) and (c) pass the verification while NCBF (b) and (d) fail. As shown in

---

1
-1
-
-1
-22
-2
-2
-2
(a)
(b)
(c)
(d)
Figure 2: Comparison of NCBFs that pass and fail the proposed verification. We show O-level set boundary in blue, initial region in green and the unsafe region in red. (a) and (b) visualize NCBFs for Darboux. (c) and (d) shows projection of NCBFs for Obstacle Avoidance.
Fig. 2a the fully-trained NCBF (a) separates the safe and unsafe regions while the NCBF (b) with unfinished training has boundary that intersects the unsafe region in Fig. 26 As shown in Fig. 2d the 2-D projection with -0.5 of NCBF (d) shows its boundary overlap the unsafe region.
We next verify the positive invariance of DD All NCBFs for Darboux pass feasibility verification with run-time presented in Table [ We compare the run-time of proposed verification with SMT-based approaches using translator proposed in (21) and SMT solver dReal [43] and Z3 [44]. The proposed method can verify NCBFs with more ReLU neurons while SMT-based verifier return nothing. All of
Table Comparison verification run-time of NCBF in seconds. The table contains the dimension n, network architecture with denoting ReLU, the number of activation sets N and run-time of proposed method including time of enumerating, verification and total run-time denoted as Les by and T, respectively. We compare with the run-time of dReal (Taneat) and 73 (Tz3).
Case
NN Architecture
N
Le
Lp
T
TaReat
Tz3
2
2-20-o-1
13
0.39
0,04
0.43
0.36
33hss
2-32-o-1
20
0.23
0.03
0.27
1.27
>3hrs
2
2-64-o-1
47
1.89
0.13
2.02
>3hrs
>3hrs
Darboux
2-96-a-1
63
4.17
0.14
4.31
>3hrs
>3hrs
2-128-0-1
65
4.77
0.03
4.90
>3hrs
>3hrs
2-512-0-1
258
33.44
0.61
34.05
>3hrs
>3hrs
2-1024-0-1
548
107.63
0.81
108.44
>3hrs
>3hrs
2-10-0-10-o-1
0.42
0.05
0.47
7.70
15.81
2
2-16-0-16-o-1
26
2.13
0.11
2.23
>3hrs
>3hrs
2-32-0-32-a-1
8.35
6.28
14.64
>3hrs
>3hrs
Darboux
2
2-48-o-48-o-1
58
13.69
0.19
13.88
>3hrs
>3hrs
2-64-0-64-a-1
102
31.30
0.47
31.77
>3hrs
>3hrs
2
2-256-0-556-44
402
319.81
1.92
321.73
>3hrs
>3hrs
2-512-0-512---1
1150
619.10
0.75
619.85
>3hrs
>3hrs
8-8-o-1
98
3.70
0.02
3.72
>3hrs
>3hss
hi-ordg
8-16-o-1
37
35.05
0.0
35.05
>3hrs
>3hrs
the generated NCBFs for obstacle avoidance and spacecraft rendezvous passed the verification. The run-times are presented in Table / We find that the activation set sizes grow with the size of neural network and the state dimension n.. We conjecture that this growth rate could be reduced by using tighter approximations for the activated sets.
key feature of our approach is that the verification process does not depend on the control policy for all 0D is safe. This improves flexibility
but rather we verify that any l satisfying while reducing false negatives in safety verification, as we illustrate in the following example. The NCBF for obstacle avoidance with one hidden layer and neurons fails the SMMT-assed verification using dReal given nominal controller fnom The counter example is at the point (-0.20, 0, -0.73).
At this point, we have 6(x) = 0.0033, dz f(x) 0.0095, which satisfies the sufficient conditions for safety in Lemma However, the nominal controller yields dz (f(x) + g(z)u) -1.30 and hence
&h

---

fails verification. Hence, by following a safe control policy of the form (TO) with the learned value of b and nominal policy pnom- we can retain the performance of fnom while still ensuring safety.
Table 2: Comparison of verification run-time of NCBF in seconds. We denote the run-time as 'UTD' when the method is unable to be directly used for verification.
Case
n
NN Architecture
N
c
T
TaReal
Tz3
3
3-32-o-1
436
6.94
0.40
7.35
>6hrs
>6hrs
3
3-64-o-1
1645
19.17
1.87
21.05
>6hrs
>6hrs
OA
3
3-96-o-1
3943
58.96
6,26
63.22
>6hrs
>6hrs
3-128-0-1 3
5695
169.51
15.56
185.07
>6hrs
>6hrs
3
3-16-0-16---1
467
18.72
2.66
21.39
>6hrs
>6hrs
3
3-32-0-32-o-1
1324
218.86
54.51
273.37
>6hrs
>6hrs
OA
3
3-48-0-48-0-1
3754
3197.59
9.75
3207.34
>6hrs
>6hss
3
3-64-0-64-0-11
6545
11730.28
18.22
11748.50
>6hrs
>ōhrs
6
6-8-0-8-0-8-1
270
78.77
10.23
89.00
UTD
UTD
SR
6616-0-660--6-1
32937
1261.60
501.06
1762.67
UTD
UTD
6 6-32-0-32-o-333
207405
12108.11
1798.08
13906.19
UTD
UTD
The computational complexity of our approach will be determined by several factors including the dimension of the state, the number of layers, the number of neurons each layer, and the geometry of the O-vel set of the NCBE As shown in Table 2 the dimension of the system plays the most important role.
Conclusion
This paper studied the problem of verifying safety of nonlinear control system using a NCBF represented by a feed-forward neural network with ReLU activation function. We leveraged generalization of Nagumo's 's theorem for proving invariance of sets with nonsmooth boundaries to derive necessary and sufficient conditions for safety. The exact safety conditions addressed the issue that ReLU NCBFs will be nondifferentiable at certain points, thus invalidating traditional safety verification methods. Based on this condition, we proposed an algorithm for safety verification of NCBFs that first decomposes the NCBF into piecewise linear segments and then solves nonlinear program to verify safety of each segment as well as the intersections of the linear segments. We mitigated the complexity by only considering the boundary of the safe region and pruning the segments with IBP and LiRPA. We evaluated our approach through numerical studies with comparison to state- of-the-an art SMT-based methods. Future extensions of this work could include improving scalability for nigher-diiensione. systems and deeper neural networks, as well as other activation functions.
Acknowledgements
This research was partially supported by the NSF (grants CNS-1941670 ECCS-2020289, IIS- 1905558, and IIS-2214141), AFOSR (grants FA9550-22-1-008 and (.9550-23-1-02088, and ARO (grant I9IINF-I9---0041),
References
[1] Devansh R Agrawal and Dimitra Panagou. Safe control synthesis via input constrained control barrier functions. In 2021 60th IEEE Conference on Decision and Control (CDC), pages 6113-6118 18. IEEE, 2021.
[2] Shao-Chen Hsu, Xiangru Xu, and Aaron Ames. Control barrier function based quadratic programs with application to bipedal robotic walking. In 2015 American Control Conference (ACC), pages 4542-4544 IEFE, 2015.
[3] Xiangru Xu, Jessy W Grizzle, Paulo Tabuada, and Aaron D Ames. Correctness guarantees for the composition of lane keeping and adaptive cruise control. IEEE Transactions on Automation Science and Engineering, 12166:121 2017.
10

---

[4] Joseph Breeden and Dimitra Panagou. High relative degree control barrier functions under input constraints. 2021 60th IEEE Conference on Decision and Control (CDC), pages 6119-619666 6124.
IEEF, 2021.
[5] Hongkai Dai and Frank Permenter. Convex synthesis and verification of control--yypunnov and barrier functions with input constraints. arXiv preprint arXiv:22/0.00629, 2022.
[6] Shucheng Kang, Yuxiao Chen, Heng Yang, and Marco Pavone. Verification and synthesis of robust control barrier functions: Multilevel polynomial optimization and semidefinite relaxation, 2023.
[7] Nicholas Rober, Michael Everett, Songan Zhang, and Jonathan P How. A hybrid partition- ing strategy for backward reachability of neural feedback loops. In 2023 American Control Conference (ACC), pages 3523-3522 IEEE, 2023.
[8] Aaron D Ames, Samuel Coogan, Magnus Egerstedt, Gennaro Notomista. Koushil Sreenath, and Paulo Tabuada. Control barrier functions: Theory and applications. In 2019 18th European control conference (ECC), pages 3420-3431. IEEE, 2019.
[9] Wenceslao Shaw Cortez, Denny Octomo, Chris Manzie, and Peter Choong. Control barrier func- tions for mechanical systems: Theory and application to robotic grasping. IEEE Transactions on Control Systems Technology, 29(2):530-54) 2019.
[10] Aaron D Ames, Jessy W Grizzle, and Paulo Tabuada. Control barrier function based quadratic programs with application to adaptive cruise control. In 53rd IEEE Conference on Decision and Control, pages 6271-6278, IEEE, 2014.
[11] Joseph Breeden and Dimitra Panagou. Robust control barrier functions under high relative degree and input constraints for satellite trajectories. arXiv preprint arXiv:2107.0409) 2021.
[12] Charles Dawson, Zengyi Qin, Sicun Gao, and Chuchu Fan. Safe nonlinear control using robust neural Lyapunov-barrier functions. In Conference Robot Learming, pages 1724-1735. PMLR, 2022.
[13] Charles Dawson, Sicun Gao, and Chuchu Fan. Safe control with learned certificates: A survey of neural Lyapunov, barrier, and contraction methods for robotics and control. IEEE Transactions on Robotics, 2023.
[14] Simin Liu, Changliu Liu, and John Dolan. Safe control under input limits with neural control barrier functions. In Conference on Robot Learning, pages 1970-1980. PMLR, 2023.
[15] Stephen Prajna, Ali Jadbabaie, and George J Puppas. A framework for worst-cass and stochas- tic safety verification using barrier certificates. IEEE Transactions on Automatic Control, 52(5):1415-1428 1428, 2007.
[16] Wei Xiao and Calin Belta. Control barrier functions for systems with high relative degree. In 2019 IEEE 58th conference on decision and control (CDC), pages 479. IEEE, 2019.
[17] Andrew Clark. Verification and synthesis of control barrier functions. In 2021 60th IEEE Conference on Decision and Control (CDC), pages 6105 61 12. IEEE, 2021.
[18] Weiye Zhao, Tairan He, Tianhao Wei, Simin Liu, and Changliu Liu. Safety index synthesis via sum-of-squares programming. arXiv preprint XXXX:22209.09134 2022.
[19] Michael Schneeberger, Florian Dörfler, and Silvia Mastellone. SOS construction of compatible
control Lyapunov and barrier functions. arXiv preprint arXiv:2305.0122) 2023.
[20] Felix Berkenkamp, Matteo Turchetta, Angela Schoellig, and Andreas Krause. Safe model-based reinforcement learning with stability guarantees. Advances in Neural Information Processing Systems, 30, 2017.
[21] Alessandro Abate, Daniele Ahmed, Alec Edwards, Mirco Giacobbe, and Andrea Peruffo. Fossil: A software tool for the formal synthesis of Lyapunov functions and barrier certificates using neural networks. In Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control, pages 1-11, 2021.
[22] Zengyi Qin, Kaiqing Zhang, Yuxiao Chen, Jingkai Chen, and Chuchu Fan. Learning safe multi- agent control with decentralized neural barrier certificates. arXiv preprint 1rXiv:2201105444 2021.
11

---

[23] Zhizhen Qin, Tsui Wei Weng, and Sicun Gao. Quantifying safety of learning- based self- driving control using cammost-barrics functions. In 2022 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 12903-12910. IEEE, 2022.
[24] Hengjun Zhao, Xia Zeng, Taolue Chen, and Zhiming Liu. Synthesizing barrier certificates using neural networks. In Proceedings of the 23rd international conference hybrid systems: Computation and control, pages 1-11, 2020.
[25] Alessandro Abate, Daniele Ahmed. Mirco Giacobbe, and Andrea Peruffo. Formal synthesis of Iyаpunov neural networks. IEEE Control Systems Letters, 5(3):773-778, 2020.
[26] Qingye Zhao, Xin Chen, Zhuoyu Zhao, Yifan Zhang, Enyi Tang, and Xuandong Li. Verifying neural network controlled systems using neural networks. In 25th ACM International Conference on Hybrid Systems: Computation and Control, pages 1-11, 2022.
[27] Karsten Scheibler, Stefan Kupferschmid, and Bernd Becker. Recent improvements in the SMT solver iSAT. MBMV, 13:231-241, 2013.
[28] Weiming Xiang, Hoang-Dung Tran, and Taylor T Johnson. Output reachable set estimation and verification for multilayer neural networks. IEEE Transactions on Neural Networks and Learning Systems, 29(11):5777-578 2018.
[29] Meng Sha, Xin Chen, Yuzhe Ji, Qingye Zhao, Zhengfeng Yang, Wang Lin, Enyi Tang, Qiguang Chen, and Xuandong Li. Synthesizing barrier certificates of neural network controlled contin- uous systems via approximations. In 2021 58th ACM/IEEE Design Automation Conference
(DAC), pages 631-636. IEEE, 2021.
[30] Claudio Ferrari, Mark Niklas Muller, Nikola Jovanovic, and Martin Vechev. Complete verifica- tion via multi-neuron relaxation guided branch-and -nd----nndddd.....--- arXiv preprint arXiv:2205.0026. 2022.
[31] Patrick Henriksen and Alessio Lomuscio. Deepsplit: An efficient splitting method for neural network verification via indirect effect analysis. In IJCAI, pages 3549,2555, 2021.
[32] Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. General cutting planes for soaundd-opagation--oa -based neural network verification. Ad- vances in Neural Information Processing Systems, 35: 15:1655-166 1656-1670, 2022.
[33] Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Purt 30, pages 97-117. Springer, 2017.
[34] Guy Katz, Derek A Huang, Duligur lbeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljić, et al. The Marabou framework for verification and analysis of deep neural networks. In Computer Aided Verification: s1 International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I 31, pages 443-452. Springer, 2019.
[35] Frederik Baymler Mathiesen, Simeon C Calvert, and Luca Laurenti. Safety certification for stochastic systems via neural barrier functions. IEEE Control Systems Letters, 7:973-978, 2022.
[36] Rayan Mazouz, Karan Muvvala, Akash Ratheesh Babu, Luca Laurenti, and Morteza Lahijanian. Safety guarantees for neural network dynamic systems via stochastic barrier functions. Advances in Neural Information Processing Systems, 35:9672-9686 9686. 2022.
[37] Franco Blanchini and Stefano Miani. Set- Theoretee Methods in Control, volume 78. Springer, 2008.
[38] Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsich. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems, 33:1 129-1141, 2020.
[39] Xia Zeng, Wang Lin, Zhengfeng Yang, Xin Chen, and Lilei Wang. Darboux-type barrier certificates for safety verification of nonlinear hybrid systems. In Proceedings of the 13th International Conference on Embedded Sofwware, pages 1-10, 2016.
[40] Andrew J Barry, Anirudha Majumdar, and Russ Tedrake. Safety verification of reactive controllers for uav flight in cluttered environments using barrier certificates. In 2012 IEEE International Conference on Robotics and Automation, pages 484-490. IEEE, 2012.
12

---

[41] Lester E Dubins. On curves of minimal length with constraint on average curvature, and with prescribed initial and terminal positions and tangents. American Journal of mathematics, 79(3):497-516, 1957.
[42] Christopher Jewison and R Scott Erwin. A spacecraft benchmark problem for hybrid control and estimation. In 2016 IEEE 55th Conference Decision and Control (CDC), pages 3300-3305.
IEEE, 2016.
[43] Sicun Gao, Soonho Kong, and Edmund M Clarke. dreal: An SMT solver for nonlinear theories over the reals. In Automated Deduction CADE-24: 24th International Conference Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013, Proceedings 24, pages 208-214. Springer, 2013.
Deduction-CADE-22
[44] Leonardo De Moura and Nikolaj Björner. 73: An efficient SMT solver. In Tools and Algorithmss for the Construction and Analysis of Systems: 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings 14, pages 337-340. Springer, 2008.
[45] Stephen Prajna, Antonis Papachristodoulou, Peter Seiler, and Pablo A Parrilo. SOSTOOLS and its control applications. Positive polynomials control, pages 273-292, 2005.
13

---

A Supplementary Material
In what follows, we give some details of content omitted in the paper due space limit. The
supplements are organized as follows. We give some proof of Lemma 2 Proposition Lemma 3 and Theorem Section A.1 A.6 respectively. We present system dynamics Darboux, obstacle avoidance, spacecraft rendezvous and hi-ordg in Section A.12 We provide some training details in Section[A.13
well as experiment details and results Section A.144 We compare
polynomial CBFs with NCBF in A.15 compare NCBFs with different activation functions in A.16
We present more details in A.17 on the example in 3.2
A.1 Proof of Lemma
We prove by induction on L. If L. = 1, then E X(S) if the pre-activation input to the (1,j) neuron nonnegative for all j S₁ and nonpositive for all j & S1. We have that the pre-activation input is equal to W + Tijs establishing the result for L = 1.
Now, inducting L, we have that XSS...... SL-1) if and only if
L-1
E
n 1=1
n JES;
1 tri 20}
n fo: : W WW: x +F:-1) + try s 50} jES:
by induction. If æ E Xx ST. then a E (Sr. if and only if the pre-activation input to the j-th neuron layer L is nonnegative for all j E Sr. and nonpositive for j & St.. The pre-activation input is equal to WT + TLJ. TLJ, which we can expand by induction as
Mr
WT 1 + + =
(W1g)y21-113 + r1j
M
(WL)) (SL-1)()) + (S) + TLJ
M
Σ WL))).W(-11716
I FLy
(W ('
completing the proof.
A.2
Proof of Lemma
The proof approach is based on Nagumo's Theorem, which gives necessary and sufficient conditions for positive invariance of a set. We first define the concept of tangent cone, and then present positive invariance conditions based the tangent cone. The approach of the proof is characterize the tangent cone to the set D = {x b(x)= 2 0}.
Definition 2. Let A be a closed set. The tangent cone to A at x defined by
lim inf dist(a + T2, +=, A)
0f
Ta(x)
(19)
The following result gives an approach for constructing the tangent cone.
Lemma ((37). ). Suppose that the set A is defined by
A = {x: (x) 0, k 1, I,...,A N}
14

---

for some collection of differentiable functions 41 . For any let J(x) {k qx(()) = 0}. Then
Ta(x) = {=: Vg & 4 E J(x)).
The following is a fundamental preliminary result for establishing positive invariance.
Theorem 3 (Nagumo's Theorem [77, Section 4.2). closed set A is controlled positive invariant if
and only if. whenever æ=t) E O.A, u(t) E u satisfies
(f(x(tt) + g(z(t))u((t) E Ta(x(t))
(20)
The following lemma characterizes the tangent cone to Proposition 2. For any E 8D, we have
Tx( = U
{=: (W.-(S)),,) 07
SES(2)
(()))ss
(:: (W), =0) nfz: W(S)" 20) (21)
(1.))T(()))
Proof. Define Ro(S) X(S) D.D We will first show that, for all x with b(x) = 0,
To(x) = U
(x))))()).
(22)
SES(x)
We observe that
dist x, D
U Po(())
> 0,
SES(n)
and hence
dist(r + D)
min dist(x T2,
SES(a)
for sufficiently small.
Suppose that (s)) (z). Then for any 0, dist(x: T2,
dist(r Zo()) since
(S) C D, and hence
lim inf dist(x + +2,
dist(r T2, Xo(S))
lim inf 7-0
+-0
7
We therefore have E Tz(x). Now, suppose that E (x) and yet & USES(w) xx(1s(()) (I). Then for all S S(z), there exists es such that
lim inf dist(x + (o)
Let ē = min {es S e S(x)) For any E (0,z), there exists F > 0 such that 7 < 7 implies
dist(r + T2
dist(æ + To,
min SES(*)
T
implying that lim inf dist(a+rs,D) > 0 and hence = & (x(x). This contradiction implies 22
It now suffices to show that, for each S S(z).
fe: W (W) ==20 )01)
(x)
n
{a: (W. = s0} n W(S) 0}.
((J)TT())
15

---

We have that each (S) is given by
Ro(S) (a': [W - +ry 2 20(())) E ray (S) & Ov(i,) & (a W(S) + +(() 2 0),
0f (W. (W-1(SS).,,)
thus matching the conditions of Lemma when each function is affine. Furthermore, the set J(x is equal to the set of functions that are exactly zero at z, which consists of (WW-i(S)W, x+ (S)
(i.j) } together with W(S) F(S). This observation combined with Lemma gives the desired result.
Lemma 2 is consequence of Proposition 2 For of exposition, first reproduce the lemma and then present the proof.
Lemma 6. The set is positive invariant if and only for all x E ÖD, there exist S E S(x) and E U satisfying
( (V
E T(x) ns (W. (W==( (0v(() T(x) \
(23)
(24)
(W (V-=(S)),,)"(((((>>>>>> 20
(25)
Proof. By Theorem 3 the set D is positive invariant if and only if for every x E OD, there exists such that (f(x) g (()))) TD(x).. By Proposition this condition holds iff there exists S(z)
such that
g(()))
f=: (W (W., 220) (AJETT())s
(s: (SW, n (2: (=:WW()) (c)))
The above condition equivalent to the conditions of the lemma, completing the proof.
A.3 Proof of Proposition I
First, suppose that condition (i) holds. Then for any x E with S(x) .S...... S,}, there exists I rI....,r} and l such that æ (Si) and H8 hold. For this choice u, have (f(x) + g()) E Tw. (x) by Proposition Hence D is positive invariant under any control policy
consistent with by Lemma
Next, suppose that condition (ii) holds. Since 'D is contained in the union of the activation sets X(S). this condition implies that D C.
A.4 Proof of Lemma
S,), there exists 1 E (1....,,') r} such that x E X((S)) and u E satisfy 7 and (8). For this choice of u, we have (f(x) + (() E (z) by Proposition 2 Hence D is positive invariant under any control policy consistent with by Theorem
Suppose that condition 1 holds. Then for any x 0D with S(z) (
If Condition 2 holds, then there is with b(x) 0 and E int(X((S) such that & C. Hence, there are no counterexamples to condition (ii) of Proposition I
A.5 Proof of Lemma
The approach to prove that condition (ii) of Proposition [holds; condition (i) holds automatically each SI...., S, satisfies condition (ii) of Lemma 3 We have that conditions (a) and (b) equivalent
16

---

to b(x) - and 11 In order for to be safety counterexample, for all / ...... at least one of Eqs. and 8 must fail. Equivalently, for all | I....,7, there does not exist satisfying
w -- (S,)W,)) " (()) I
V(, V(i,)) E f()) I(S........ 8,)
[ (W.-(SS) g(x) 2
W (S.) g(x) S W(S))"
Au S
By Farkas Lemma, non-existence of such a u is equivalent to existence of yr satisfying 2 0 as well as and (18).
A.6 Proof of Theorem 2
Suppose that x is a safety counterexample for the NCBF with b(x) 0. If E int for some
S, then we have that S E S and hence contradiction with Lemma 3 some Si,..., then there is a contradiction with Lemma
If x E X(() (..)))....() ..,(S)) for
A.7 Details on the IBP Procedure
Interval bound propagation aims to compute an interval of possible output values by propagating range of inputs layer-by-layer and is integrated into our approach as follows. We first use partition the state space into cells and, for each cell, use LiRPA to derive upper and lower bounds on the value of b(x) when x takes values in that cell. When the interval of possible b(x) values in cell contains zero, we conclude that that cell may intersect the boundary b(x) = For each neuron, we use IBP to compute the activvavvtion input interval for values of x within the cell. When the pre-activation input has positive upper bound and negative lower bound, we identify the neuron as unstable, i.e., enumerate
may be either positive negative for values of x within the cell. Using this approach, collection of activation sets S. We then identify the activation sets S S such that b(x:) = 0 for some I E (S) by searching for an x that satisfies the linear constraints in (16). This approach uses LiRPA and IBP to identify the activation regions that intersect the boundary {x b(x) = 0} without enumerating and checking all possible activation sets, which would have exponential runtime in the number neurons in the network.
A.8 Nonlinear Programming
The condition 2 of Lemma suffices to solve the nonlinear program
minimize
h(r) W (S) + +r,(S) (V(1,) E Wi + < V(i.j) &S
s.t.
(26)
W(S) x x+ +r(S)= =0
and check whether the optimal value is nonnegative (unsafe) negative (safe).
The verification problem of Lemma can then be mapped to solving the nonlinear program
ming Vi.....
max (S......
s.t.
W. (
U US,
S . ns, (W " 0Y(i)) I(S....... S,)
[W
(27)
(S...,..
1....,,
2 2
and checking whether the optimal value is nonnegative (safe) negative (unsafe).
A.9 Experiment Settings: Darboux
We show the settings of NCBF verification for Darboux system whose dynamic is defined
i1
22 +
2x
(28)
- + +17
17

---

We define state space, initial region, and unsafe region as A {x E RR: : E [-2, x 1-2. X1 {x E R² 0 S 1, x2 S 2] and x fx R² + z 0} respectively.
A.10
Experiment Settings: Obstacle Avoidance
We next evaluate that our proposed method on a controlled system (4)). The system state consists of 2-D position and aircraft yaw rate æ := [21, 22, w/"". We let denote the control input to manipulate yaw rate and define the dynamics as
#1 82
sin vi v cos vb
+
0
(29)
We define the state space, initial region and unsafe region X, X, and Xr. respectively
X' [x E R 12, v [- [-
[-,
X, {x R -01 S s 0.1, -2 -2 1.8, - < 7/
(30)
Xv {x +f 0.04]
A.11 Experiment Settings: Spacecraft Rendezvous
The state of the chaser is expressed relative to the target using linearized Bathessy-Wilsshre--ee equations, with state [Px. Py Pa Up Ugy uzl". control input defined as follows.
[Uge By us 1" and dynamics
Px Py
0
0
0
1
0
0
Py
P=
0
0
0
3n2
Ux
+
Uly
(31)
By
0
0
2m
0
0
0
Ugy.
2
U/
We define the state space and unsafe region as X and Nr. respectively as
X' : fx R p. u. [-1.5, 1.5) x 1-1.5, 1.5]
(32)
X 0.25 < < 1.5, where
v22 + pr + 1²
We obtain the trained NCBF with neural CLBF training in with a nominal model predictive controller.
A.12 Experiment Settings: hi-ords
The dynamic model of the system is captured by ODE follows.
(x) + (7) + 170x (6) (6) + 2273. 39) 41880 + 2400.
576 0 (33)
where we denote the i-th derivative of variable x by ()) We define the state space and unsafe region as X' and Ny. respectively
X' { + +... x
Xe { (m) + 2)² +... (xs + 2)² < 0.16}
(34)
We obtain the trained NCBFs with training method proposed in 21
A.13 Training Details
We trained the NCBFs for Darboux and obstacle avoidance via the approach proposed in (24). Models trained with their open source code with default settings. Detailed parameters for both cases listed Table 3a
18

---

We then trained NCBFs for Spacecraft Rendezvous by following approach proposed in [13] with the empirical loss defined in Eq. (5) in [2]. Models are trained with their open source code with default settings. The hyper-parameters are listed in Table 3b
Table 3: Hyper- parameters for training NCBBs to be verified
(a) Hyper-papne parameters for Darboux and OA
Hyper-Parameten:
Value
(b) Hyper-parameters for Spacecraft Randezvous
LEARNING RATE
0.01
Value
LOSS OPT FLAG
1e-16
LEARNING RATE
0.01
TOL MAX GRAD
BATCH SIZE
512
EPOCHS
5
CONTROLLER BORNOLLEERPRRIODD
PERIOD
0.01
TOL. INIT
TOL_
0.0
SIMULATION DT
0.01
TOL_
0.0
CBF_HIDDEN LIADENNLLYYRS
TOL, BOUNDARY
0.05
CBF OBF_HIDDEN, WRIDDEN_SITEE
16
TOL LIE
0.0
LAMBDA
0.1
TOL NORM LIE
0.0
CBF RELAXATION PEN
le4
WEIGHT LIE
SCALE PARAMEETR
10.0
WEIGHT NORM
PRIMAL LEARNING RATE
1e-3
DECAY LIE
LEARN SHAPE, EPOCHS
100
DECAY INIT
DECAY UNSAFE AESSFFE
A.14 Experiment Details and Results
We use translators and verifiers proposed in FOSSIL for SMT-based verification with solver dReal and Z3 baselines. Our proposed enumerating algorithm utilize auto-LiRPA with default settings and linear program with HiGHS solvers provided by SciPy Detailed settings can be found in our attached code.
We further visualize the trend of the number of activation sets and run-time with respect to the total number of neurons with ReLU activation function in Fig. We can find that the logarithm of the activation sets size grows with the size of the neural network. The dimensionality of the state is the dominant factor determining the run-time. The logarithm of the run-time is determined by both the state dimension and the number of ReLU hidden layers. The potential result can be cause by loose activation set estimation. Methods deriving tighter bounds than IBP may mitigate the influence the ReLU hidden layers.
A.15 Comparison of NCBF and SOS-based Synthesis
We compare NCBF with traditional SOS synthesized polynomial CBF for the obstacle avoidance case study in two aspects, namely, training time T; and volume V of the guaranteed safe region. In order to synthesize the polynomial CBF, we adopt the procedure introduced in [45). This procedure first constructs nominal controller p(x), and then uses SOS programming to construct a barrier certificate for the system (t) = f(x) + +g(x) (())).
(z). We choose μ(x) = -2y as the nominal controller and synthesize CBFs of degree 2, 4, 6, 8, and 10 using the Matlab SOSTOOLS toolbox. We compared the result with an NCBF with one hidden layer of 32 neurons trained using the method proposed in (4 with the same nominal controller. The experiment results shown below. The time of SOS CBF synthesis grows with the degree of the barrier function. Degree 10 CBF takes twice the time compared to NCBE On the other hand, NCBF outperforms all SOS synthesized CBFs by having the largest safe region volume.
http:p/pptossaa..ooooooooooooooe 1inprog highs .tml
19

---

Logarithm of Activation Set Size Comparison
Logarithm Run-time Comparison
5.00
4.00
3.00
2,00
1.00
32
64
96
128
-1.00
64
96
128
Darboux
Darboux 2 Obs Obs
Darboux 1
Darbboxx
Obs
Obs
(a)
(b)
Figure Comparison of the number of activation sets and run run-time with respect to number of neurons in total. (a) shows logarithm of activation set size. (b) shows logarithm of run-time. We denote Darboux respectively. We denote
NCBFs Darboux with I and hidden layers as Darboux NCBFs for obstacle avoidance with I and 2 hidden layers as obs I and obs 2, respectively.
Table 4:
Comparison of the training time T. and safe region volume V of NCBF and SOS synthesized CBFs for Obstacle Avoidance
Types
Ti (s)
(m² x deg)
NCBF 3-32-a-1
262.89s
37.76
SOS Degree 2
7.36s
16.14
SOS Degree 4
6.65s
13.44
SOS Degree 6
19.88s
31.36
SOS Degree 8
125.10s
25.93
SOS Degree 10
551.31s
19.99
A.16 Comparison between Activation Functions
We considered three case studies, namely, Darboux. obstacle avoidance, and spacecraft rendezvous. For each case study, we trained and verified three NCBFs with the same architecture (2 hidden layers of 32 neurons each) but different activation functions, namely, ReLU, sigmoid, and tanh. We found
Table 5: Comparison of training time T, safety region volume V and verification time T, of ReLU, Sigmoid and Tanh NCBF for Darboux, Obstacle Avoidance and Spacecraft Rendezvous. ReLU NNs verified by proposed method while others are verified by dReal and Z3. We write UTD when the method cannot be not directly used for verification
Obstacle
Spacecraft Rendezvous
Case
Darboux
Avoidance
ReLU
Sigmoid
Tanh
ReLU
Sigmoid
Tanh
ReLU
Tanh
Te
28.53s
51.14s
69.49s
71.44s
78.66s
76.49s
879.388s
953.469s
V
2.27
1.62
2.8
4.99
2.17
3.50
0.20
0.22
T,
14.64
>3hrs
>3hrs
273.37s
>3hrs
>3hrs
13906.19s
UTD
that, for the Darboux and obstacle avoidance case studies, the ReLU NCBF completed training faster than both sigmoid and tanh NCBFs. The volume of the safe region was comparable for all three activation functions, with the tanh outperforming the ReLU NCBF Darboux and the ReLU NCBF providing the largest volume for obstacle avoidance. The most significant difference between the three activation functions was at the verification stage. Our proposed method for verifying ReLU NCBFs terminated within 15 and 274 seconds in the Darboux and obstacle avoidance, respectively, while SMT-based methods did not terminate within three hours for both test cases. the spacecraft rendezvous example, the ReLU NCBF completed training before the tanh NCBE Moreover, while our approach verified the correctness of the ReLU NCBF within 4 hours, the tanh NCBF exhibited safety violation.
20

---

A.17
Example Details
Consider the setting the example in Section 3.2 Let be denote the NCBF defined in the example, which fails our defined safety conditions. For comparison, we trained an NCBF by and verified using our proposed approach. We then constructed nominal controller Prom as a Linear Quadratic Regulator (IQQ) controller that drives the system from initial point (0,0.1) to the origin. We compared the trajectories arising from the optimization- baased controller defined by Eq. (10) using the by and be- For the unsafe NCBF be. the optimization-base controller is unable to satisfy the safety constraints the boundary point (0, 1). resulting safety violation. On the other hand, while the NCBF by contained multiple non-diffecrentaall points, it is possible to choose u to ensure safety at these points. For example, the point (-0.19, 2.91) is a non-differentiable point on the boundary by O. There are four activation sets intersecting at this point, with corresponding values of tbe
8z g(x) given by {-0.0455, -0.053, 0.025, -0.033). Since any control input with negative sign and sufficiently large magnitude will satisfy dbe (f(x) + g(x)u) for all of these values, this non-differentiable point does not compromise safety of the system, and the trajectory of the system constrained by by remains in the safe region for all time.
Comparison of trajectory of bg and b..
Safety Boundary of bş
Safety Boundary of b,
NCBF Trajectory
CE Trajectory
Safety Boundary h(x)
Figure 4: Comparison of optimization based controller using trained NCBF bg and unsafe NCBF be-
21


Reviews:
[{"review_id": "bl3qM3KZPy", "reviewer": "Reviewer_5o49", "summary": "The paper proposes a technique to verify the safety of NCBF-based control policies. Usually, the verification depends on the CBF to be continuously differentiable. This is not the case for NNs, however using NCBFs is beneficial as it allows to encode more complex safety constraints.\nTheir approach identifies the piecewise linear segments of the NCBF. The number of segments is reduced by only focusing on those at the boundary of the safe region. The remaining linear segments are overapproximized and verified using nonlinear programs.\nThe authors compare their proposed technique with SOTA SMT based methods and demonstrate that they are able to verify NCBFs that previously resulted in a timeout.", "questions": "Main question: Why can't one use regular verification of safety properties of neural networks? If $D$ is convex (or can be split into a reasonable number of convex subsets), then one could verify that no input in $D$ is mapped to an output outside of $D$. When $f$, $g$ and $\\\\mu$ in Equation 1 are known, that equation could most probably be encoded as a NNs, so all common tools (compare e.g. VNN-COMP 2022 or 2023) should be able to verify this (or time out). You state the main benefit of your approach is that it does not depend on the specific choice of $\\\\mu$ (line 288). However, I do not know if this is often a requirement. If $\\\\mu$ changes, the verification using a technique that depends on $\\\\mu$ could be repeated. Did you do an experimental comparison of your approach with a NN-Verification-Tool-based approach to see how costly this would be?\n\nOther questions:\n\n1) In the text above Proposition 1, is $\\\\overline{X}(S_1) \\\\cap \\\\ldots \\\\cap \\\\overline{X}(S_r) \\\\cap S'$ well-defined? $\\\\overline{X}(S)$ is a set of inputs $x$, but $S'$ is a set of neurons. Should this be $\\\\overline{X}(S')$?\n\n2) In Equation 11, is the term to the right of $ \\\\textbackslash $ obsolete? If $\\\\{S_1, \\ldots, S_r\\\\}$ is complete, then no input that activates all of $\\\\{S_1, \\ldots, S_r\\\\}$ also activates any other $S'$ (based on the text above Proposition 1). So what is removed by the term right of $ \\\\textbackslash $ ?\n\n3) What's the significance of the three different lines in Figure 2? They represent different \"set boundaries\", bu I do not know what that visualization achieves compared to one with just set boundary 0\n\nMinor: What is the missing reference in line 243?\n\nMinor note: Line 268: \"with in\" -> \"within\"", "limitations": "The authors do not provide a list of limitations or potential negative societal impact. However, the potential negative societal impact is probably small, as this technique is developed to increase the provable safety of NCBFs. So the potential negative societal impact is identical to that of any AI-based technology.\nThe paper would benefit from a description of the limitations of their proposed approach.", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "The paper propose a new original technique to prove the safety of NCBFs.\nThe authors do a good job of motivating their new approach by demonstrating the shortcoming of techniques that expect $b$ to be continuously differentiable.\nThe paper is mostly clear in its explanation and formulas, and gives intuitive explanations for many of them.\nIn their experimental evaluation, they use one benchmark to compare their performance against two other SOTA techniques, and demonstrate that they are able to verify instances that would otherwise lead to a timeout. This indicates the significance of their proposed technique, should the results carry over to other benchmarks.", "weaknesses": "The equations in the paper get increasingly complicated to follow, even with the provided explanations. Especially Lemma 4 is hard to follow. \n\nIn the experimental evaluation, the paper would strongly benefit from exploring more benchmarks. The comparison to SOTA techniques dReal and Z3 is limited to one benchmark, with two more benchmarks that do not include a comparison to those tools. Also, a comparison to an approach based on neural-network-verification (e.g. \"A Hybrid Partitioning Strategy for Backward Reachability of Neural Feedback Loops\" by Nicholas Rober, Michael Everett, Songan Zhang, and Jonathan P. How) would help to demonstrate that the proposed technique can solve previously hard problems.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Regarding the benchmarks considered in this work, we have evaluated our approach on additional test systems and compared with dReal and Z3. Our results are summarized in Tables 2 and 3 of the pdf attachment to the general rebuttal. Our approach verified a three-dimensional system (obstacle avoidance) with a 128-neuron NCBF in roughly 3 minutes, a six-dimensional system with an NCBF consisting of 102 neurons with three hidden layers within four hours, and an eight-dimensional system with an 18-neuron NCBF within 35 seconds. In contrast, the SOTA algorithms dReal and Z3 did not terminate within six hours for the obstacle avoidance and eight hours for the eight-dimensional system. All experiments were performed on the desktop PC environment described in our manuscript.\n\nWe thank the reviewer for suggesting comparisons with the VNN-COMP benchmarks. VNN-COMP is primarily concerned with verifying input/output relationships of neural networks, i.e., proving that, given a neural network $b$ and a set of inputs $\\mathcal{X}$, we have $b(\\mathcal{X}) \\subseteq \\mathcal{Y}$ for some set $\\mathcal{Y}$. In principle, it would be possible to train a neural network $\\phi(x)$ to approximate $f(x)+g(x)\\mu(x)$ as suggested by the reviewer, and then use the methodologies of VNN-COMP to check whether there exists $x$ with $b(x) \\geq 0$ and $b(x+\\phi(x)dt) < 0$, where $dt$ is a discrete-step size that approximates the evolution of the ODE (1). However, in order to achieve an exact verification algorithm, the errors introduced by the NN approximation $\\phi(x)$ and the discrete-time approximation of (1) would need to be characterized and incorporated into the verification. Furthermore, as mentioned by the reviewer, our approach does not depend on the control policy $\\mu(x)$. We believe that this is an advantage because we can ensure safety under any nominal control policy $\\mu(x)$ by incorporating the policy into the optimization-based control (10). This provides the system designer with an additional degree of flexibility, which has been highlighted in recent works on CBF-based safety filters (e.g., A.D. Ames et al, “Control Barrier Functions: Theory and Applications”) and safe shield policies in reinforcement learning (e.g., I. ElSayed-Aly et al, “Safe Multi-Agent Reinforcement Learning via Shielding”).\n\nSimilarly, we would like to highlight the following distinction with the related work “A Hybrid Partitioning Strategy for Backward Reachability of Neural Feedback Loops” by Rober et al. The main goal of this related work is to verify safety of a given neural network controller using backwards reachability analysis. In contrast, the goal of our work is to construct an NCBF b and prove that any control policy $\\mu$ satisfying Eqs. (7)--(9) is safe. Our approach could be considered complementary to Rober et al in the following two ways. First, a given neural network controller $\\mu$ could be modified to provide verifiable safety guarantees by following the quadratic program-based policy defined by Eq. (10) with $\\mu_{nom} = \\mu$. Second, one could attempt to prove that a NN feedback control policy satisfies Eqs. (7)--(9) for a given $b$ and all x, which would prove that the policy is safe. This latter approach to NN safety verification would be an alternative to backward reachability analysis, and is a direction of future research.\n\nFinally, we thank the reviewer for identifying several typos in the paper. Proposition 1 should be \n$\\cdots \\cap \\overline{\\mathcal{X}}(\\mathbf{S}_{r}) \\cap \\overline{\\mathcal{X}}(\\mathbf{S}^{\\prime})$ \nas suggested by the reviewer. The term to the right of \\ can indeed be omitted in Eq. (11). We have revised the visualization of Fig. 2 to remove the additional lines and thus improve readability. The missing reference in line 243 refers to Eq. (27) of the supplement and will be fixed. We will revise the paper carefully including Lemma 4 to simplify and clarify the notations."}, {"review_id": "RQ5AJdaYGR", "reviewer": "Reviewer_wvvT", "summary": "In this paper, the authors present a new strategy for verifying neural control barrier functions (NCBFs) to ensure safe control of nonlinear systems. Specifically, the authors address the challenge posed by NCBFs when ReLU activation functions are employed. This renders existing verification strategies inapplicable due to the non-differentiability of resulting NCBFs. The authors tackle this issue by introducing conditions for a ReLU NCBF to satisfy \\emph{positive invariance}, which forms the basis for constructing safe control policies. The proposed verification algorithm enumerates \\emph{activation sets} and individually verifies their positive invariance defined based on the positivity of the activation outputs. The paper demonstrates the effectiveness of the proposed approach by comparing it with Satisfiability Modulo Theory (SMT) based methods across three control problems.", "questions": "N/A", "limitations": "The authors should consider the possibility of clearly outlining the limitations of their study and potential negative societal impacts.\n\nAfter the rebuttal phase (the same as the post-rebuttal comments):\nI thank the authors for their response and conducting the additional experiments. The majority of the concerns raised in my initial evaluation have been effectively attended to. While I acknowledge the efforts undertaken by the authors to conduct an additional round of experiments, I still have reservations about how well the proposed algorithm would work for problems with high dimensions. The additional experiments provided are still confined to low-dimensional scenarios. I recommend that the authors explore this aspect in their future research endeavors.", "rating": 6, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- The paper contributes to the field by introducing a new verification algorithm and control strategies that apply to NCBFs using ReLU activation functions. Existing verification approaches are not directly applicable, and the authors address this limitation by introducing a new characterization of active sets and a corresponding verification algorithm. This approach has the potential to broaden the application domain of neural control barrier functions.\n- The paper appears to be technically sound.", "weaknesses": "- While the comparison with SMT-based methods is informative, it would be beneficial to include a more comprehensive performance evaluation of ReLU NCBFs against classical NCBFs with differentiable activations, such as sigmoid. Assessing factors like NCBF training time, verification time, and the expressive capabilities of the resulting NCBFs in real-world control problems would add depth to the analysis. If ReLU NCBFs consistently outperform sigmoid NCBFs, the proposed verification strategy's utility would be significantly enhanced.\n- The authors could provide a thorough analysis of the time complexity of the proposed verification strategy. As the algorithm discretizes the state space into hyper-cubes and calculates corresponding bounds of $b(x)$ individually, it is important to understand how the complexity scales in high-dimensional problems. Also, the authors should provide experiments on more complex, potentially higher-dimensional control problems.\n- (Minor) the manuscript contains several typos that require careful proofreading.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "In order to compare with NCBFs that have differentiable activation functions, we conducted the following additional simulation study. We considered three test systems, namely, the Darboux, obstacle avoidance, and spacecraft rendezvous test cases. For the Darboux and obstacle avoidance  systems, we trained three NCBFs with the same architecture, i.e., 2 hidden layers and 32 neurons in each hidden layer, but different activation functions. The chosen activation functions were ReLU, Sigmoid, and tanh. We compared the performance based on three metrics: (i) training time, defined as the time required for the running loss to converge to 0, (ii) volume of the safe region $\\{x: b(x) \\geq 0\\}$, and (iii) time required to verify the trained NCBF. We verified the ReLU-activated NCBF using our proposed method and verified the Sigmoid and tanh-activated NCBFs using dReal and Z3.\n\nWe trained NCBFs for spacecraft rendezvous using the NCBF training approach proposed  in “Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction Methods for Robotics and Control” (Dawson et al, ref. [13] of the manuscript). We compared NCBFs with ReLU and tanh activation functions using the metrics (i)-(iii) above.\n\nThe results are summarized in Table 1 of the pdf attachment to the general rebuttal. We found that, for the Darboux and obstacle avoidance case studies, the ReLU NCBF completed training faster than both sigmoid and tanh NCBFs. The volume of the safe region was comparable for all three activation functions, with the tanh outperforming the ReLU NCBF in Darboux and the ReLU NCBF providing the largest volume for obstacle avoidance. The most significant difference between the three activation functions was at the verification stage. Our proposed method for verifying ReLU NCBFs terminated within 15 and 274 seconds in the Darboux and obstacle avoidance, respectively, while SMT-based methods did not terminate within three hours for both test cases. In the spacecraft rendezvous example, the ReLU NCBF completed training before the tanh NCBF. Moreover, while our approach verified the correctness of the ReLU NCBF within 4 hours, the tanh NCBF exhibited a safety violation.\n\nFinally, to address the concern regarding high-dimensional problems, we evaluated our approach on an eight-dimensional system first defined in “Fossil: A Software Tool for the Formal Synthesis of Lyapunov Functions and Barrier Certificates Using Neural Networks” (Abate et al, ref. [1] in the manuscript). The results are summarized in Table 2 of the pdf attached to the general rebuttal. Our approach verified an NCBF with a single hidden layer containing 16 neurons in 35 seconds. The SOTA algorithms dReal and Z3 did not terminate within six hours. \n\nTo address the concern on scalability to complex neural networks, we conducted additional experiments as shown in Tables 2 and 3 of the pdf attachment to the general rebuttal. We verified an NCBF for Darboux example with one hidden layer of 1024 neurons and an NCBF with two hidden layers of 512 neurons each. The verification terminated successfully in 108 and 620 seconds, respectively. The computational complexity of our approach will be determined by several factors including the dimension of the state, the number of layers, the number of neurons in each layer, and the geometry of the 0-level set of the NCBF. As shown in Table 3, the dimension of the system plays the most important role, which is a widely-shared issue in traditional SOS verification of CBFs as well as neural network verification algorithms. While the focus of this paper is on developing exact safety conditions, improving scalability is a direction of future work that we will pursue. "}, {"review_id": "ctJWoi0w2f", "reviewer": "Reviewer_U7BK", "summary": "The authors consider the problem of synthesising control barrier functions parametrised as ReLU neural networks for non-linear deterministic dynamical systems. The authors first extend standard approaches for synthesising control barrier functions to the case where the barrier function is non-differentiable in a zero-measure set. Then, they encode the synthesis of a neural control barrier function as a nonlinear optimisation problem and illustrate the effectiveness of the approach on three benchmarks", "questions": "Please, see Weaknesses Section and in addition consider the following points:\n\n- Equation (7) and (8) quantifies over pairs $(i, j)$ of the set $\\mathbf{T}(x) \\cap \\mathbf{S}$. However, $\\mathbf{T}(x)$ is the set of unstable neurons produced by input $x$, hence it is unclear what pairs the quantification is referring to. Is it any two unstable neurons in the set $\\mathbf{T}(x) \\cap \\mathbf{S}$?\n\n- Set $\\bar{\\mathcal{X}}(\\mathbf{S})$ is defined both inside Lemma 1 and right after the Lemma. Please, be consistent\n", "limitations": "Please, see Weaknesses Section", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "-\tThe theory is sound and the extension of standard results for synthesizing control barrier functions to non-differentiable barriers is surely of interest\n-\tPaper is overall well written and the problem considered of interest\n", "weaknesses": "-\tThe main weakness is the scalability of the approach wrt the complexity of the neural barrier function. While I acknowledge that the algorithm is superior in terms of scalability than SMT based approaches, still experimental results are limited to neural networks of 1 hidden layer and 20 neurons at most \n-\tSome of the statements in the related works are not precise. In fact, the authors claim that it is not possible to use convex programming to synthesize/verify neural barrier functions. This is not accurate, in fact recent approaches rely on piecewise linear uncertain relaxations of neural networks to encode the problem of verifying neural barrier functions using linear programming [Mathiesen, Frederik Baymler, et al. \"Safety certification for stochastic systems via neural barrier functions.\" IEEE Control Systems Letters 7 (2022): 973-978.] or SDP [Mazouz, Rayan, et al. \"Safety guarantees for neural network dynamic systems via stochastic barrier functions.\" Advances in Neural Information Processing Systems 35 (2022): 9672-9686.]. Of course, the resulting approach will be more conservative compared to the one proposed by the authors, but more scalable. Also, please expand the discussion of why approaches employed to synthesize neural Lyapunov functions, e.g. [Abate, Alessandro, et al. \"Formal synthesis of Lyapunov neural networks.\" IEEE Control Systems Letters 5.3 (2020): 773-778], cannot be employed in the setting of this paper\n-\tTo demonstrate the importance of using neural control barrier functions, I believe that in the experiments there should be at least one experiment where the authors compare with the standard approaches commonly employed to synthesise control barrier functions, e.g. parametrising them as a SoS polynomial. This should serve to empirically demonstrate the advantages in being able to make use of the flexibility of neural networks in the context of barrier functions.\n", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "In order to evaluate our approach on more complex neural networks, we conducted additional experiments as shown in Tables 2 and 3 of the pdf attachment to the general rebuttal. We verified an NCBF for the two-dimensional Darboux example with two hidden layers of 512 neurons each. The verification terminated successfully in 620 seconds. We verified an NCBF with two hidden layers of 64 neurons each for the three-dimensional obstacle avoidance example in 3 hours, 15 minutes. Finally, we verified an NCBF with three hidden layers, each containing 32 neurons, for a six-dimensional spacecraft rendezvous problem within four hours. For each of these networks, state of art verification algorithms dReal and Z3 did not terminate within three hours.\n\nThe reviewer is correct that prior works have developed computationally tractable relaxations of the problem of verifying neural Lyapunov and barrier functions, whereas the aim of our paper is to develop exact conditions and algorithms. Moreover, we note the following key differences between our problem setting and the problems studied in the works identified by the reviewer. First, the prior works consider a discrete-time setting. Developing analogous conditions in continuous time requires addressing the non-differentiability of the gradient of the neural network activation functions, which is a contribution of the present paper. Second, the prior works assume that a control law has been given, while our proposed approach can be applied as a safety filter to an arbitrary given controller via the optimization problem (10). \n\nTo reduce confusion, we will change the last sentence of the first paragraph of the related work to “However, SOS-based approaches for polynomial CBFs cannot be applied directly to NCBF verification, since activation functions used in neural networks are not polynomial and may be non-differentiable.” We will also add a sentence to the second paragraph of the related work that reads “Piecewise linear approximations of ReLU neural networks have been used to develop tractable safety verification algorithms using linear and SOS programming. This approach leads to sound and incomplete verification algorithms, whereas the present paper proposes exact verification algorithms. Moreover, these existing works apply to discrete-time systems with a priori given controllers.” We will add citations to the papers suggested by the reviewer.\n\nWe compare NCBF with traditional SOS synthesized polynomial CBF for the obstacle avoidance case study in two aspects, namely, training time $T_t$ and volume $V$ of the guaranteed safe region. In order to synthesize the polynomial CBF, we adopt the procedure of “SOSTOOLS and its Control Applications” (Prajna et al). This procedure first constructs a nominal controller $\\mu(x),$ and then uses SOS programming to construct a barrier certificate for the system $\\dot{x}(t) = f(x) + g(x)\\mu(x)$. We choose $\\mu(x)=-x_{3}$ as the nominal controller and synthesize CBFs of degree 2, 4, 6, 8, and 10 using the Matlab SOSTOOLS toolbox. We compared the result with an NCBF with one hidden layer of 32 neurons trained using the method proposed in [34] with the same nominal controller. \nThe experiment results are shown below. The time of SOS CBF synthesis grows with the degree of the barrier function. Degree 10 CBF takes twice the time compared to NCBF. On the other hand, NCBF outperforms all SOS synthesized CBFs by having the largest safe region volume.\n\n\n| CBF Type                | $T_t \\ (s)$ | $V \\ (m^2\\times deg)$ |\n|----------------------|-------------|-----------------------|\n| NCBF 3-32-$\\sigma$-1 | 262.89s     | 37.76                 |\n| SOS Degree 2         | 7.36s       | 16.14                 |\n| SOS Degree 4         | 6.65s       | 13.44                 |\n| SOS Degree 6         | 19.88s      | 31.36                 |\n| SOS Degree 8         | 125.10s     | 25.93                 |\n| SOS Degree 10        | 551.31s     | 19.99                 |\n\nIn Eqs. (7) and (8), $(i,j)$ refers to the $j$-th neuron at the $i$-th layer. We will remove redundant definitions from the final manuscript."}, {"review_id": "TuiOfIC7p2", "reviewer": "Reviewer_yuYJ", "summary": "Neural control barrier functions offer wider expressive power but do not satisfy the continuously differentiable assumption with ReLU activation functions. In this paper, the authors propose a method to verify that a neural ReLU CBF is a valid CBF and is hence capable of rendering a set forward-invariant. This method derives its foundations by extending the conditions of Nagumo’s theorem. These observations provide a set of necessary and sufficient conditions for verification. Algorithmically, these conditions are verified by a combination of linear relaxation to do a coarse analysis followed by interval bound propagation to fine-tune the regions of violation. Then, two non-linear programs are used to check for the CBF conditions. The final verification engine runs faster than existing SMT methods and works correctly on three benchmarks: Darboux, Obstacle avoidance and Spacecraft.", "questions": "1) In proposition 1, equation (11), is the set difference explicitly needed given that the collection of sets $\\{ S_1, \\dots, S_r \\}$ is defined as complete.\n\n2) What is the meaning of equation (15) in line 186? Why can that not just be written as $\\mathcal{D} \\subset \\mathcal{C}$ ?\n\n3) For the procedure discussed in figure 1, I did not find a lot of background material in the appendix on exactly how IBP is used to enumerate activated sets and which linear program is used for pruning. I recommend a discussion on this in greater detail in the Appendix similar to Section 7.7 for the non-linear program. This is the phase that is seen to be time-consuming from Table 2 and needs to be justified.\n", "limitations": "The societal impact of this work is likely positive.\nLimitations on the scalability of the approach to higher dimensional systems and deeper networks is discussed.", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 2, "contribution": 3, "strengths": "The theoretical conditions for verification and the proposed algorithm are novel, principled, creative and non-trivial. Previous works typically gloss over the points of non-differentiability in energy functions such as CLF/CBF. Hence, I believe this is an important contribution which can be extended further in future work.", "weaknesses": "1) The presentation needs to be improved and there are several minor mistakes which put off the reader.\nLine 243 - missing reference, Line 181 - mistake in the definition of complete collection, Line 439 -  What definition of distance is used in the definition of tangent cone?, Multiple typos in Lemma 5 in appendix\n\n2) If the set of non-differentiable points has measure zero, it will not actually affect the practical safety filtering application as the system can shoot through those points. \n\n3) For the experiments section, it would be interesting to also plot the points of non-differentiability in figure 2. The current result comparing to improperly trained CBF is rather expected. Showing the enhancement of safety verification/safety filtering by virtue of considering non-differentiable points will enhance the contribution.\n", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for identifying some minor mistakes in the manuscript. The missing reference refers to Eq. (27) from the supplementary material and will be corrected. The definition of complete collection will be modified to $\\cdots \\cap \\overline{\\mathcal{X}}(\\mathbf{S}^{\\prime})$. Distance is defined by $\\mbox{dist}(x,\\mathcal{C}) = \\min{\\\\{||x-z|| : z \\in \\mathcal{C}\\\\}}$, where $||\\cdot||$ is a $p$-norm for some $p \\in [1,\\ldots,\\infty]$. In Lemma 5, the definition of $J(x)$ should be $J(x) = \\\\{k: q_k(x) = 0\\\\}$, while the following equation should be $\\mathcal{T}\\_{\\mathcal{A}}(x) = \\\\{z : z^{T}\\nabla q_{k}(x) \\leq 0 \\ \\forall k \\in J(x)\\\\}.$\n\nThe reviewer is correct that the set of non-differentiable points will have measure zero. As shown in the example on Page 4, although this set has measure zero, safety of the CBF cannot be guaranteed if the non-differentiable points fail the conditions (7)--(9). When applying the safety filter at runtime, the optimization problem (10) reduces to a standard CBF-based quadratic program, except at the measure-zero set of non-differentiable points. If non-differentiable points occur in the interior of the region $\\mathcal{D} = \\\\{x : b(x) \\geq 0\\\\}$, we conjecture that it may be possible to shoot through them as suggested by the reviewer. Safety violations may occur if the controller attempts to shoot through non-differentiable points at the boundary, as shown in the following example.\n\nConsider the setting of the example on Page 4 of the manuscript. Let $b_{c}$ denote the NCBF defined in the example, which fails our defined safety conditions. For comparison, we trained an NCBF $b_{\\theta}$ and verified it using our proposed approach. We then constructed a nominal controller $\\mu_{nom}$ as a Linear Quadratic Regulator (LQR) controller that drives the system from initial point $(0,0.1)$ to the origin. We compared the trajectories arising from the optimization-based controller defined by Eq. (10) using the $b_{\\theta}$ and $b_{c}$. For the unsafe NCBF $b_{c}$, the optimization-based controller is unable to satisfy the safety constraints at the boundary point $(0,1)$, resulting in a safety violation as described in the manuscript. On the other hand, while the NCBF $b_{\\theta}$ contained multiple non-differentiable points, it is possible to choose $u$ to ensure safety at these points. For example, the point $(-0.19, 2.91)$ is a non-differentiable point on the boundary $b_{\\theta} = 0$. There are four activation sets intersecting at this point, with corresponding values of $\\frac{\\partial b_{c}}{\\partial x}g(x)$ given by $\\\\{-0.0455, -0.053, -0.025, -0.033\\\\}$. Since any control input $u$ with negative sign and sufficiently large magnitude will satisfy $\\frac{\\partial b_{c}}{\\partial x}(f(x)+g(x)u) \\geq 0$ for all of these values, this non-differentiable point does not compromise safety of the system, and the trajectory of the system constrained by $b_{\\theta}$ remains in the safe region for all time.\n\nThe reviewer is correct that the set difference is not needed in Eq. (11). It will be removed. Eq. (15) is presented to specify the conditions that must hold for all activation set $\\mathbf{S}$. After taking the union over $\\mathbf{S}$, the statement is equivalent to $\\mathcal{D} \\subset \\mathcal{C}$ as pointed out by the reviewer. \n\nInterval bound propagation aims to compute an interval of possible output values by propagating a range of inputs layer-by-layer, and is integrated into our approach as follows. We first use partition the state space into cells and, for each cell, use CROWN to derive upper and lower bounds on the value of b(x) when x takes values in that cell. When the interval of possible b(x) values in a cell contains zero, we conclude that that cell may intersect the boundary b(x) = 0. For each neuron, we use IBP to compute the pre-activation input interval for values of x within the cell. When the pre-activation input has a positive upper bound and negative lower bound, we identify the neuron as unstable, i.e., it may be either positive or negative for values of $x$ within the cell. Using this approach, we enumerate a collection of activation sets $\\mathcal{S}$. We then identify the activation sets $\\mathbf{S} \\in \\tilde{\\mathcal{S}}$ such that $b(x) = 0$ for some $x \\in \\overline{\\mathcal{X}}(\\mathbf{S})$ by searching for an $x$ that satisfies the linear constraints in (16). This approach uses CROWN and IBP to identify the activation regions that intersect the boundary $\\\\{x: b(x) = 0\\\\}$ without enumerating and checking all possible activation sets, which would have exponential runtime in the number of neurons in the network. We will add a section to the appendix that elaborates on IBP and its use in our verification algorithm."}, {"review_id": "AOeA63ePf5", "reviewer": "Reviewer_hbj4", "summary": "This paper studies the exact conditions under which a learned CBF $b$ with ReLU activations yields the positive invariance property. Even though the set of inputs for which the CBF is non-differentiable has measure zero, the paper shows by example that safety can be still violated. This is because the slope of $b(x)$ can be discontinuous at the boundary $b(x) = 0$. To address this, the paper derives a theoretical result (Proposition 1) that provides a necessary and sufficient condition for a valid ReLU CBF. Based on this central result, the paper presents a verification algorithm that consists of state space discretization and search, activation set enumeration, and solving nonlinear programs. The experiments show faster safety verification for low-dimensional systems than SMT-based approaches.", "questions": "* What are the theoretical and practical advantages of using ReLU activations over differentiable activations (as done in [1], for example) for modeling neural CBFs?\n\n* Shouldn't the last formula in the proof of Lemma 1 use $W_{Lj}$, not $W_{ij}$?\n\n[1] Dawson, Charles, Zengyi Qin, Sicun Gao, and Chuchu Fan. \"Safe nonlinear control using robust neural lyapunov-barrier functions.\" In Conference on Robot Learning, pp. 1724-1735. PMLR, 2022.", "limitations": "* The most concerning limitation is the scalability of the verification method. Even if the state space has a low-dimensionality, the usage of more layers or neurons can lead to combinatorial explosion of the runtime complexity.", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 2, "contribution": 2, "strengths": "* ReLU is a popular activation function that is often used for constructing feedforward neural networks. The paper addresses the important theoretical problem of verifying learned CBFs with ReLU activations.\n* The paper provides a novel, central theoretical result (Proposition 1) that gives necessary and sufficient conditions for a given ReLU neural CBF to be valid.\n* As shown in Section 5, the proposed verification algorithm yields more efficient run-time than SMT-based approaches.\n", "weaknesses": "* From a practical point of view, an engineer or a researcher can always choose a differentiable activation function to design a neural CBF, such as tanh or softplus. Then, the CBF remains differentiable. This leads to a motivational question of why we should use ReLU activations for modeling CBFs in the first place. Specifically, the proposed approach seems to possess several disadvantages compared to learning differentiable CBFs and verifying them. 1) The verification algorithm involves state-space discretization and activation set enumeration, both of which have inherent poor scalability with respect to the state-space dimensionality and the size of the neural network, respectively. In particular, the enumeration seems to suffer a lot as the network becomes complex, as observed in Table 2. 2) The online optimization problem for control (i.e. equation 10) requires solving possibly multiple quadratic programs, adding complexity to the standard CBF-QP.\n\n* The presentation can be improved so that mathematical descriptions are easier to follow. Especially, it is recommended that the paper 1) clearly define dimensionality of every vector and matrix-valued variables introduced in the paper, such as $W_i$, $W_{ij}$. 2) Define clearly any non-trivial variables in the main statement of mathematical results. For instance, the definition of $\\bar{W}_0$ and $\\bar{r}_0$ should be provided in the main statement of Lemma 1, not in the proofs in the appendix.\n", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We conducted an experimental study to compare NCBFs with different activation functions, including ReLU, sigmoid, and tanh. The results are shown in the pdf attachment to the general rebuttal, and are discussed in detail in the rebuttal to Reviewer wvvT above. In particular, we find that our proposed algorithm for verifying ReLU-activated NCBFs is more computationally tractable compared to SOTA algorithms for verifying NCBFs with differentiable activation functions. \n\nThe reviewer is correct that the online optimization-based control requires solving multiple quadratic programs in the worst-case. However, there will only be multiple quadratic programs at points where the NCBF is nondifferentiable, or equivalently, where the pre-activation input to one of the neurons in the NCBF is exactly zero. In order to evaluate the complexity of the CBF-QP, we compared the computation time of (i) Eq. (10) with a NCBF consisting of one hidden layer of 32 neurons and (ii) a CBF-QP using a degree-two polynomial CBF. Averaging over 300 iterations, we found that the NCBF-based controller had a runtime of 0.0015s while the polynomial CBF-based controller had a mean runtime of 0.0012s.\n\n$W_{ij}$ has dimensionality $n \\times 1$ for $i=1$ and $M_{i-1} \\times 1$ for $i > 1$. $W_{i}$ is an $n \\times M_{i}$ matrix. We will clearly define matrix and vector dimensions throughout the paper, as well as provide definitions of $\\overline{W}\\_{0}$ and $\\overline{r}\\_{0}$ in the main statement of the lemma. The reviewer is correct regarding the last formula in the proof of Lemma 1. It should be $W_{Lj}$."}]

Author rebuttal:
We would like to thank the reviewers for providing detailed comments that have helped to improve the quality of our manuscript. We have provided rebuttals to the comments of each reviewer. We have also attached a pdf file containing figures and tables from additional simulations that were requested by the reviewers. In this general rebuttal, we briefly summarize these additional figures and tables. Figure 1 is in response to a comment from Reviewer yuYJ. The reviewer asked about the impact of non-differentiable points on safety filtering. We considered the example from Page 4 of the manuscript, and compared the unsafe NCBF from the manuscript (which we denote $b_{c}$) with a trained NCBF $b_{\theta}$ that we verified using our approach. We compared optimization-based controllers based on Eq. (10) of the manuscript using the NCBFs $b_{c}$ and $b_{\theta}$, where the nominal controller was a linear quadratic regulator that drives the system to the origin. The NCBF $b_{c}$ resulted in a safety violation due to the non-differentiable point identified in the manuscript, while the NCBF $b_{\theta}$ ensured that the system state remained within the safe region. Additional descriptions can be found in the rebuttal to Reviewer yuYJ.

Table 1 is in response to comments from Reviewers wvvT and hbj4. Both reviewers asked why ReLU activation function would be used for NCBFs instead of differentiable activation functions. To address this question, we considered three case studies, namely, Darboux, obstacle avoidance, and spacecraft rendezvous. Descriptions of each of these systems can be found in the manuscript. For each case study, we trained and verified three NCBFs with the same architecture (2 hidden layers of 32 neurons each) but different activation functions, namely, ReLU, sigmoid, and tanh. We found that the NCBF with ReLU activation function had the shortest training time for all test cases and resulted in the largest safe region volume for the obstacle avoidance test case. Moreover, our proposed verification algorithm for the ReLU NCBF terminated within 15, 274, and 13907 seconds for Darboux, obstacle avoidance, and spacecraft rendezvous, respectively, while the SOTA verification algorithms (dReal and Z3) did not terminate within three hours for any of the test cases.. Additional descriptions of these experiments can be found in the rebuttal to Reviewer wvvT.

Tables 2 and 3 are in response to comments from Reviewers 5o49, wvvT, U7BK, yuYJ, and hbj4 regarding the scalability of the proposed approach to higher-dimensional systems as well as neural networks with larger numbers of neurons. We trained NCBFs for an additional eight-dimensional system that first appeared in “Fossil: A Software Tool for the Formal Synthesis of Lyapunov Functions and Barrier Certificates Using Neural Networks” (Abate et al, ref. [1] in the manuscript), as well as more complex neural networks for the three case studies already considered in the paper. Our approach verified a 1024-neuron NCBF for the Darboux system in 620 seconds, a 128-neuron NCBF with two hidden layers for obstacle avoidance in 11749 seconds, a 96-neuron NCBF for spacecraft rendezvous in 13907 seconds, and a 16-neuron NCBF for the eight-dimensional test case in 35 seconds. Neither of the SOTA verification algorithms (dReal and Z3) terminated within three, six, and six hours for the Darboux, obstacle avoidance, and eight-dimensional systems, respectively. Additional details can be found in the rebuttals to Reviewers 5o49 and wvvT.

Meta-review: During the initial phase of reviewing, some issues were raised regarding the clarity and experimental setup of the submission. The rebuttal provided the necessary clarifications. All five expert referees recommend acceptance. The authors should take into account the detailed reviews, discussions and their own rebuttal while preparing the camera-ready version of the paper.
Decision: Accept (poster)