SEEV: Synthesis with Efficient Exact Verification for ReLU Neural Barrier Functions
Authors: Hongchao Zhang
Zhizhen Qin
Sicun Gao
Andrew Clark
Venue: NeurIPS 2024 poster (2024)
Keywords: Safe Control
Barrier Functions
Control Barrier Functions
Neural Networks
Primary area: safety_in_machine_learning
TL;DR: This paper proposes a ReLU NCBF synthesis framework with efficient exact verification for robotic safety. Key insights: ReLU NCBF can be verified in linear pieces, boundary pieces are safety-critical, and limiting them improves efficiency.

Abstract: Neural Control Barrier Functions (NCBFs) have shown significant promise in enforcing safety constraints on nonlinear autonomous systems. State-of-the-art exact approaches to verifying safety of NCBF-based controllers exploit the piecewise-linear structure of ReLU neural networks, however, such approaches still rely on enumerating all of the activation regions of the network near the safety boundary, thus incurring high computation cost. In this paper, we propose a framework for Synthesis with Efficient Exact Verification (SEEV). Our framework consists of two components, namely (i) an NCBF synthesis algorithm that introduces a novel regularizer to reduce the number of activation regions at the safety boundary, and (ii) a verification algorithm that exploits tight over-approximations of the safety conditions to reduce the cost of verifying each piecewise-linear segment. Our simulations show that SEEV significantly improves verification efficiency while maintaining the CBF quality across various benchmark systems and neural network structures. Our code is available at https://github.com/HongchaoZhang-HZ/SEEV.

SEEV: Synthesis with Efficient Exact Verification for ReLU Neural Barrier Functions
Hongchao Zhang"
Zhizhen Qin"
Electrical & Systems Engineering Washington University St. Louis hongchao@wustl..ed
Computer Science & Engineering University of California, San Diego zhizhenqin@uesd. edu
Sicun Gao
Andrew Clark
Computer Science & Engineering University of California, San Diego
Electrical Systems Engineering Washington University in St. Louis
scungaolucsd.
andrenclark0rustl..
Abstract
Neural Control Barrier Functions (NCBFs) have shown significant promise in en- foreing safety constraints nonlinear autonomous systems. State-of-the art exact approaches to verifying safety of NCBF-based controllers exploit the piecewise- linear structure of ReLU neural networks, however, such approaches still rely on enumerating all of the activation regions of the network near the safety boundary, thus incurring high computation cost. In this paper, we propose framework for Synthesis with Efficient Exact Verification (SEEV). Our framework consists of two components, namely an NCBF synthesis algorithm that introduces novel regu- larizer to reduce the number of activation regions at the safety boundary, and (ii) a verification algorithm that exploits tight over aver-approximation of the safety condi- tions to reduce the cost of verifying each piecewise-linedd segment. Our simulations show that SEEV significantly improves verification efficiency while maintaining the CBF quality across various benchmark systems and neural network structures. Our code available at htttts::///. //gi thub. com/Honggchaozaangg -Z//SEV
Introduction
Safety is crucial property for autonomous systems that interact with humans and critical infras- tructures in applications including medicine, energy, and robotics 212, which has motivated recent research into safe control 3 5 7. Control Barrier Functions (CBFs), which apply constraint the control input at each time in order to ensure that safety constraints are not violated, have attracted significant research attention due their ease of implementation and compatibility with variety of safety and performance criteria [8]. Recently, CBFs that are defined by neural networks, denoted as Neural Control Barrier Functions (NCBFs), have been proposed leverage the expressiveness of NNs for safe control of nonlinear systems 99 10 [1]. NCBFs have shown substantial promise in applications including robotic manipulation
navigation 22 and flight control (14.
key challenge in NCBF-based control is safety verification, which amounts to ensuring that the constraints the control be satisfied throughout the state space under actuation limits. The NCBF safety verification problem effectively combines two problems that are known to be difficult, namely, input-output verification of neural networks (VNN) [15] [6] 17 [8 [9] 20 and reachability verification of nonlinear systems. While sound and complete verifiers such as dReal can be applied to
Equal contribution
38th Conference on Neural Information Processing Systems (NcurIPS 2024).

---

NCBFs, they typically can only handle systems of dimension three or small neural networks 22 22
In 23 exact conditions for safety verification of NCBFs with ReLU activation functions were proposed that leverage the piecewise-linearty of ReI.U-NNs to reduce verification time compared to dReal for general activation functions. The exact conditions, however, still require checking correctness of the NCBF by solving a nonlinear optimization problem along each piecewise- linear segment. Hence, the NCBF verification problem remains intractable for high-dimensional systems.
In this paper, we propose a framework for Synthesis with Efficient Exact Verification (SEEV) for piecewise-liness NCBFs. The main insight of SEEV is that the computational bottleneck of NCBF verification is the inherent requirement of verifying each linear segment of the neural network. We mitigate this bottleneck by (i) developing a training procedure that reduces the number of segments that must be verified and (ii) constructing verification algorithms that efficiently enumerate the linear segments at the safety boundary and exploit easily-checked sufficient conditions to reduce computation time. Towards (i), we introduce a regularizer to the loss function that penalizes the dissimilarity of activation patterns along the CBF boundary. Towards (ii), we propose a breadth- first search algorithm for efficiently enumerating the boundary segments, as well tight linear over-approximations of the nonlinear optimization problems for verifying each segment. Moreover, we integrate the synthesis and verification components by incorporating safety counterexamples returned by the safety verifier into the training dataset. Our simulation results demonstrate significant improvements in verification efficiency and reliability across a range of benchmark systems.
Related Work: Neural control barrier functions have been proposed describe complex safety sets to remain inside and certify safety of controlled system [24 21 25 26 or synthesize control input
based on NCBFs to ensure safety ||] [7] However, the synthesized NCBF may not ensure safety. Safety verification of NCBFs is required. Sum-of-squares (SOS) optimization (28 29 30 31 [2] has been widely used for polynomial barrier functions, however, they are not applicable due to the non-polynomial and potentially non-differentiable activation functions of NCBFs. VNN [33
34 35 and methods for ReLU neural networks [36]] 37 are also not directly applicable to NCBF verification. Nonlinear programming approach (23) provides another route for exact verification but is computationally intensive and relies on VNN tools. To synthesize neural networks with verifiable guarantees, Counterexample Guided Inductive Synthesis (CEGIS) has been applied using SMT- based techniques [21 39 [T]. Other verification-in-te-llog approaches utilize reachability neural network verification tools [43 However, existing
analysis (42] and branch-and-bour works suffer from the difficulty of performing verification and generating counterexamples
a computationally efficient manner. Sampling-bai based approaches [41 [T] aim to prove safety using Lipschitz conditions, but they rely on dense sampling over the state space, which is computationally prohibitive. In this work, we present SEEV to integrate the synthesis and efficient verification by incorporating safety counterexamples from the exact verification.
Organization The remainder of the paper is organized follows. Bection22gitt gives the system model and background on neural networks and the conditions of valid NCBFs. Scction presents the SEEV framework. Section 4 presents our efficient and exact verification. Section 5 contains simulation results. Section 6 concludes the paper.
2
Preliminaries
This section presents the system model, notations on neural networks, and exact conditions of safety,
2.1
System Model
We consider a system with state xtt) E X C 12 and input u(t) E U C R!",, with initial condition (to)) = zo where zo lies in an initial set I C X. The continuous-time nonlinear control-affine system has the dynamics given by
a(t) = f(x(t) + +(((t)))u(()
where R - Rd and g Rd + R xm are known continuous functions.
We consider the case that the system is required to remain inside given set of states, i.e., sx(() E C for all time 2 40- The set C, referred to as the safe set, is defined as = {a M(x) 2 0) by some given continuous function h _² + R. The unsafe region is given by X C.

---

2.2 Neural Network Model and Notations
We let W and r denote the weight and bias of a neural network, and let 0 be parameter vector obtained by concatenating W and r. We consider a e-parameterized feedforward neural network bg 1 + R constructed as follows. The network consists of layers, with each layer i consisting of M; neurons. We let (i:j) E {I,.... 7.j x (1...., M. denote the j-th neuron at the i-th layer. We denote the pre-activation input as z) piecewise linear activation function and the post-activation output as 2 = (2) Specifically, we assume that the NN has the Rectified Linear Unit (ReLU) for = 2 0 and (=)
for < 0. We define the neuron (i) (i,j) as active if 2 > O, inactive if (6) {j < 0 and unstable if 2j 0. Let S Ts Ts( {i..))
activation function, defined by (=)
0} S ((i.)) :i I,.., L 1, ..... Mi} denote the set of activated and unstable neurons,
produced by state x and function Ts. Let T(x) = TT(#) ((i.)) = 0) denote the set of unstable neurons produced by and TT. T(S S,) denote the set of unstable neurons produced by activation sets Si....,S S, The set of inactive neurons is given by S i.e., the complement of S, and consists of neurons with negative pre-activation input. We define vectors W (S)(S) E IR"
(i)
and scalars 7.,(S) E IR such that 2; (i) (S)(S) x + Ti, (S) in the Appendix A.1
The symmetric B) U (B A).
difference between two sets A and B, denoted by AAB, is defined as AAB (A
Finally, we define the terms hyperplane and hinge. For any S C (1,.... X(S) := {a (z)) = S}. The collection of (S) for all with the ReLU neural network. A hyperplane that intersects the set fx (z) 0} is boundary hyperplane. The intersection of hyperplanes X(S)). . X(S,)) is called a hinge. A hinge that intersects the set {a (n(x)) = 0} is a boundary hinge.
1 x (1,..., M,), we define
the set of hyperplanes associated
2.3 Guaranteeing Safety via Control Barrier Functions
Barrier certificates (28 ensure the safety of a feedback-controlles system under policy μ(rr A) by identifying CBF represent the invariant safe set. The barrier certificate defines an inner safe region D = {x b(x) 2 0} for some continuous function b. The verifiable invariance of D is obtained from the following result.
Theorem 1 (Nagumo's Theorem [44), Section 4.2). A closed set D is controlled positive invariant if. whenever z ÖD, where 0D denotes the boundary of D. we have
(f(z) + g(z)u)+ E Ap(z)
(2)
for some U where AD(x) is the tangent cone to at x.
We denote a state &ce with &cc E OD that violates (2) as a safety counterexample. In the case where 6 is continuously differentiable, (2) can be satisfied by selecting u to satisfy the condition 0b (f(()) ((x(t))u(t)) 2 -o(b(x(t)), where R R is strictly increasing function with a(0)= = O. When is not continuously differentiable, as in a ReLU NCBFs, a modified condition is needed. Prior work 23] introduces exact conditions for safety verification of ReLU NCBFs, based on the following proposition. A collection of activation sets S, S,,..., S, is complete if, for any S' & (S1...., Sr). we have X(S)) n.... n (S())) n ((S))=
Proposition 1. Suppose the function ReLU neural network-defined function b satisfies the following conditions:
(i) For all activation sets Si,...;5. Sr with (Si,..., S.) complete and any satisfying b(x) 0 and
)x(ss))
x E
(3)
1=1
there exist E (1.....,r] and u E U such that
(f) +(z))) 2 0
Vi.jj E ((S)...,,S))s,,
(4)
W ) 0
v(i.) e T(S,....,S,)
(5)
(6)
3

---

(ii) For all activation sets S. we have
(A(S) ( | =
If (((((())) 2 0, then z(t) E C for all 0.
Any feedback control law μ X' - U that satisfies 6 is guaranteed to ensure safety and is referred to as NCBF control policy. Given nominal control policy Tnom safe actions can be derived from a ReLU NCBF as a safety filter by solving the following optimization problem
proposed in 23
Lemma 2]:
||u - nom (z)ll2 S.L. W(S)" + 2 -a(b(x)), u E Ed, 4 S
min
6
(8)
The solution to this optimization problem provides a control u that minimally deviates from the nominal control nno (I) while satisfying NCBF constraints derived in Proposition| ennsuring that D is positive invariant and is contained in C. Based on Proposition [ we can define different types of safety counterexamples. Correctness counterexamples. denoted by 4 refers state te E D n (X' C). Hyperplane verification counterexamples refer states &h that violate (6). Hinge verification counterexamples are states x with T(x) * @ that violate
6).
3 Synthesis
In this section, we present the framework to synthesize NCBF by (z) to ensure the safety of the system The synthesis framework aims to train an NCBF and construct an NCBF-based safe control policy. We first formulate the problem and present an overview of the framework in 3.1 Then we demonstrate the design of the loss function in 3.2
(T.
3.1 Overall Formulation
Our primary objective is to synthesize ReLU Neural Control Barrier Function (ReLU-NCBF) for ① and develop a safe control policy to ensure system safety.
Problem 1. Given a system ( initial set I and a safety set C, synthesize a ReLU NCBF (x parameterized by such that the conditions in Proposition Mare satisfied. Then construct control
policy to synthesize such that the system remains positive invariant in D = {r: by ba(x) 2 0} C.
We propose SEEV to address this problem with the synthesis framework demonstrated in Fig. D The training dataset T is initialized by uniform sampling over X. The training framework consists of two loops. The inner loop attempts to choose parameter 0 for (xx) to satisfy the safety condition by minimizing the loss function over training data T. The outer loop validates given NCBF by (z) by searching for safety counterexamples &ee and updates the training dataset as {f
To train the parameters of the NCBF to satisfy the conditions of Proposition I we propose loss function that penalizes the NCBF for violating constraints (i) and (ii) at collection sample points. The loss function is weighted sum of three terms. The first term is the correctness loss penalizing state X'' C with (ar)) 2 The second term verification loss that penalizes states that th such that (6 hold. The third term is regularizer minimizing the number of hyperplanes and hinges along the boundary. However, minimizing the loss function insufficient ensure safety [9] because there may exist safety counterexamples outside of the training dataset. In order to guarantee safety, SEEV introduces an efficient exact verifier to certify whether bo(x) meets the safety conditions outlined in Proposition]] I The verifier either produces proof of safety generates a safety counterexample that can be added to the training dataset to improve the NCBE.
The integration of the verifier can improve safety by adding counterexamples to guide the training process, however, it may also introduce additional computation complexity. We propose combined approach, leveraging two complementary methods to address this issue. First, the verification of SEEV introduces an efficient algorithm Section ( mitigate the computational scalability challenges that arise neural network depth and dimensionality increase. Second, SEEV introduces a regularizer to limit the number of boundary hyperplanes and hinges be verified, addressing the complexity that arises as neural network size increases.

---

Proposition
NCEF Training Sec. 3
NCBF
Enumcration Sec. 411
Boundary Activation Regularizer
Hyper plames & Hinges
Training Dotasct
Velllooioo Sec. 4.2
(1 Proposition
Counterexamples
No
Figure 1: SEEV: Synthesis with Efficient Exaet Verifier for ReLU NCBF
3.2 Loss Function Design and NCBF Training
The goal of the inner loop is to choose parameters 9 so that the conditions of Proposition are satisfied for all å T and the computational cost of verifying safety is minimized. To achieve the latter objective, we observe (based on results presented in Table that the computational complexity of verification grows with the cardinality of the collection of activation sets that intersect the safety boundary 0D. The collection is defined as B == {S; : 8D n (S.) & 0}. Hence, we formulate the following unconstrained optimization problem to search for 0.
min 0
ABCB(T) (TT((T) AcCo
(9)
where CB(T) regularizer to minimize B), (T) is the loss penalizing the violations of constraint (4)(6) (()) of Proposition D Lc(T) penalizes the violations of constraint 7 ((ii) of Proposition and λg, Ay and d are non-negative coefficients defined as follows.
Cy Regularizer: For each sample & T the safe control signal is calculated by
min u.y
||u Tuom (x)11² s.t. W(S)) + ((0))) +r
(10)
where W = W for differentiable points and W = W defined as the subgradient at non con-differentiable points. The regularizer Ly enforces the satisfaction of the constraint by inserting positive relaxation term in the constraint and minimizing with large penalization in the objective function. We have the loss L,j defined as L,- = ||u noom (1) + We use 45 to make this procedure differentiable, allowing us employ the relaxation loss into the NCBF loss function design.
Lo Regularizer: Le regularizer enforces the correctness of the NCBF. In particular, it enforces the (x( of safe samples x E Tz to be positive, and (z: of unsafe samples Txxe to be negative. Define Neate = TT and Nunsafe = |x and with a small positive tuning parameter >
0, the loss term
L. can be defined
1 Ek- bo (x)) 02 Nunsafe zETxie
Le =0=1 01 Nsatc
Ie+ le bo(x)]+
(11)
#ETz
where H++ = mwx(- 0). a and a2 are positive parameters controlling penalization strength of the violations of safe and unsafe samples.
Lg Regularizer: We propose a novel regularizer to limit the number of boundary hyperplanes and hinges by penalizing the dissimilarity. i.c., AS(;)) of boundary activation sets S(ă) B. However, the dissimilarity measure of boundary activation sets inherently nondifferentiable. To address this issue the regularizer introduces the generalized sigmoid function (2(2) T+exp(
to compute the vector of smoothed activation defined as Φo,, (a)) = [o<((z,)), Vi. j E (1....,T))
(1...., M. The LE regularizer conducts the following two steps to penalize dissimilarity.
In the first step, the regularizer identifies the training data the boundary hyperplanes and hinges denoted as è Tap. The set is defined Tap := {# f XS)), YS B). To further improve the efficiency, the regularizer approximates Tep with a range-based threshold e on the output of the NCBF, i.e., (+) < e.
The second step is to penalize dissimilarity e B. To avoid the potential pitfalls of enforcing similarity across the entire boundary B, the regularizer employs unsupervised learning approach to
5

---

group the training data into NB clusters. We define the collection of the activation set in each cluster as B; S B and the collection each cluster as TB. = {á & E USEB. X(S))- The LB is then defined as follows, with an inner sum over all pairs of Æ E TB, and an outer sum over all clusters.
L8
E EBB
1100r (1x)) Doa (3))
(12)
NB
TB.
BEEB
4 Verification
typorplanee
NBPS
Comrenio Volifeatin
Fail
Iakaval 12 (20)
Verifation
Fail
Reer Condition Veallenice Ae
Foil
Safey CE
Hyperpiaso
(20)
Pass
Pass
Frumenee (1P)) (,), 5,,55
Seftiient Coaditis Bouisto
Fall
Theoren
Safety
Figure 2: Overview of the Efficient Exact Verifier for ReLU NCBFs
In this section, demonstrate the efficient exact verification of the given NCBF 6p(x)) to ensure the positive invariance of the set under the NCBF-based control policy. In what follows, we propose an efficient enumeration and progressive verification moving from sufficient to exact conditions. The overview of the proposed approach as shown in Fig. SEEV decomposes the NCBF into hyperplanes and hinges and verifies each component hicrarchically, with novel tractable sufficient conditions verified first and the more complex exact conditions checked only the sufficient condi- tions fail. Given NCBF (xx). the verification of SEEV returns (i) Boolean variable that is 'true' the conditions of Proposition are satisfied and 'false' otherwise, and (ii) a safety counterexample i that violates the conditions of Proposition if the result is 'false". Algorithm presents overview of the verification of SEEV. The algorithm consists of an enumeration stage to identify all boundary hyperplanes and hinges, and verification stage certify satisfaction of conditions in Proposition for all hyperplanes and hinges.
Algorithm Efficient Exact Verification
1: Input: n, Txye; Tz
2: Output: Verification Boolean result r, Categorized counterexample &ce
3: procedure EFFICIENT EXACT VERIFICATION(TXXC- TT)
4: Sp < ENUMINIT(Tx.. Tz)
b Initial Activation Set Identification, Section Activation Sets Enumeration, Section
5:
S NBFS(S,)
6:
Correctness
Correctness Verification, Section 4.2
7:
r, th) + veperrpaaeVerifierr(
Hyperplane Verification, Section
4.2
8:
V - HingeLEnu((,,
> Hinges Enumeration, Section
9:
r. Pec +- Hinge HingeVerifier(V))
b Hinge Verification, Section
4.2
10:
Return for
4.1
Enumeration of Hyperplanes and Hinges
The boundary enumeration identifies the boundary hyperplanes S, E B. It initially identifies the initial boundary activation set S, E B, enumerates all E B by NBFS starting from Sg, and finally enumerates all hinges consisting of the intersections of hyperplanes. The NBFS approach avoids over-approximation of the set of boundary hyperplanes that may be introduced by, e.g., interval propagation methods, and hence is particularly suited deep neural networks.
In what follows, we assume that the unsafe region X C and initial safe set I are connected, and use 8D to refer to the connected component of the boundary of D that separates I and X' \,C C. This

---

assumption is without loss of generality since we can always repeat the following procedure for each connected component of I and X' C.
Initial Activation Set Identification: First, we identify the initial boundary activation set Sp. Given ty X') \. C and dzz E I, define line segment
i= f R" æ (1 x)x + AZz, A [0,
(13)
The following lemma shows the initial boundary activation set So can always be produced as So = S()) for some ă E L.
Lemma Given two sample points iv. such that b(āt) < O, and iz, such that b(āy) > 0. ler L denote the line segment connecting these two points. Then, there exists a point 7t E L. with by (i)
Lemma 1 follows from the intermediate value theorem and continuity of by (ar). . In order to search for So, we choose sequence of Nj, points = ".....,,Yy, L. For each 2Q. we check to see if N(S @ by solving boundary linear program BoundarYLP(S(x))) (14 in Appendix
A.4 A.4 Activation Sets Enumeration: We next describe Neural Breadth-First Search (NBFS) for enumerat- ing all activation sets along the zero-level set, given an initial set Sg. NBFS enumerates a collection of boundary hyperplanes denoted S by repeating the following two steps.
Step 1: Given set S, NBFS identifies a collection of neighbor activation sets denoted B as follows. [S (i,5), (i,5) E E''
For each (i.j) with 1..... L and j
M, construct S' as S' S (i,j), (i. $ S
We check whether S' B by solving the linear program USLP(S, (i.5))
(15) in Appendix A.4
If there exists such a state v; then S' is added to B. To further improve efficiency, we employ the simplex algorithm to calculate the hypercube that overapproximates the boundary hyperplane, denoted as H((S) 2 X(S), and relax the last constraint of (14) to z E H(S)..
Step 2: For each S' E B. NBFS determines if the activation region X(S)) is on the boundary (i.e., satisfies (S') aD * 0) by checking the feasibility of BoundaryT.P(S') If there exists such a state then S' is added to S. This process continues in a breadth-first search manner until all such activation sets on the boundary have been enumerated. When this phase terminates, S B. Detailed procedure is described as Algorithm 3 in Appendix A.3
Hinge Enumeration: The verifier of SEEV enumerates collection V of boundary hinges, where each boundary hinge V E V is subset S S, of B with ((, n X(S)) aD * 0.
Given S C and S. hinge enumeration filter the set of neighbor activation sets of S defined as (S, = (S' S' Ás = 1, E S.... Then, hinge enumeration identifies hinges V by solving linear program (PAV3 (S,)) (66 Appendix A.4 If 3a., hinge enumeration includes the hinge into the set VUV. The efficiency can be further improved by leveraging the sufficient condition verification proposed in Section 4.2 The following result describes the completeness guarantees of S and V enumerated in Line 5 and 8 of Algorithm
Proposition 2. Let S and V denote the output of Algorithm 7 Then the boundary 0D satisfies 0D C Uses (S). Furthermore, if is complete and (N (S.)) n fx : b(x) = 0} * then (SI.... S,) E V.
The proof is omitted due to the space limit. A detailed proof is provided in Appendix A.2
4.2 Efficient Verification
The efficient verification component takes the sets of boundary hyperplanes S and boundary hinges V and checks that the conditions of Proposition I hold for each of them. As pointed out after Proposition[]] the problem of searching for safety counterexamples can be decomposed into searching for correctness, hyperplane, and hinge counterexamples. In order to maximize the efficiency of our approach, we first consider the least computationally burdensome verification task, namely, searching for correctness counterexamples. We then search for hyperplane counterexamples, followed by hinge counterexamples.
7

---

Correctness Verification:
The correctness condition 77) can be verified for boundary hyperplane
X() by solving the nonlinear program 17 in Appendix A.5 When (( is convex, (17) can be
solved efficiently. Otherwise, dReal can be used check satishability of 17 in a tractable runtime.
Hyperplane Verification: Hyperplane counterexamples can identified by solving the optimization problem (T8) in Appendix A.5 Solving (8) can be made more efficient when additional structures
on the input set and dynamics f and are present. Consider a case 24 = { Dw ||||| S 1). In this case, the problem reduces to the nonlinear program (99) in Appendix A.5 If f(x) and g(x) are linear in æ, then the problem boils down to a linear program. If bounds on the Lipschitz coefficients of and g available, then they be used to derive approximations of 19
If u Thm then by 123 Corollary 1J, the problem can be reduced to the nonlinear program
(20 in Appendix A.5 If g(x) is constant matrix G, then safety is automatically guaranteed if W(S) If [
is linear in x as well, then (0) is linear program.
Hinge Verification: The hinge V (S Sr} can be certified by solving the nonlinear
optimization problem (2) in Appendix A.5 In practice, simple heuristics are often sufficient to verify safety of hinges without resorting to solving (2T). If (F)"
> 0 for all x E X(())) x (S)(s)) then the control input u 0 suffices to ensure safety. Furthermore, if 4 Im and there exists i (l...., m and E {0, 1} such that sign((W (S,)* g()))) for all E (' n .....
(S,) (S,)
and = 1,...... r, then u can be chosen as u, Kss for some sufficiently large K to ensure that the conditions of Proposition[]]
Safety Guarantee: The safety guarantees of our proposed approach are summarized in Theorem
Theorem 2. Given a NCBF (z(z). (x) is valid NCBF if it passes the verification of Algorithm ! using dReal to solve the optimization problems I7 and (II.
The proof is derived from completeness of the enumeration Algorithm and dReal. A detailed proof can be found in Appendix A.6
Experiments
In this section, we evaluate the proposed SEEV in regularizer efficacy and verification efficiency. We also demonstrated the improved performance with counter-example guidance in the synthesis framework, whose results are detailed in B.2 We experiment on four systems, namely Darboux, obstacle avoidance, hi-ordg, and spacecraft rendezvous. The experiments run on a workstation with an Intel 1170KF CPU, and an NVIDIA GeForce RTX 3080 GPU. We include experiment settings and in Appendix and byperparameters settings in Table Appendix B.3
5.1 Experiment Setup
Darboux: We consider the Darboux system [46), a nonlinear open-loop polynomial system with detailed settings presented in Appendix[B.. [B.]
Obstacle Avoidance (OA): We evaluate our proposed method on a controlled system 47 We
consider Unmanned Aerial Vehicles (UAVs) avoiding collision with tree trunk. The system state consists of 2-D position and aircraft yaw rate x := [21, 22, "0""" The system is manipulated by the yaw rate input with detailed settings presented in Appendix B.]
22,
Spaceeraft Rendezvous (SR): We evaluate our approach on a spacecraft rendezvous problem from [48). The system state is x [Pz: PPx: Py. Us, U2. Uy. 1= and control input is u [ My. uz]" with with detailed settings presented Appendix
hi-ordg: We evaluate our approach on an eight-dimensional system that first appeared in evaluate the scalability of the proposed method. Detailed settings be found in Appendix B.1
21 to
5.2 Regularizer Efficacy Evaluation
Table 2 and Figure 3 iillustrates the impact of regularization on the CBF boundary's activation sets. Table compares various configurations, where n denotes the input dimensions, represents the number of layers, and M indicates the number of hidden units per layer. N, and N, are the number of

---

0.25
-0.25
0.00
0.25
0.25
0.50
0.75
0.75
1.00
1.0
0.5
0.5
-0.5
0.0
-1.0
-0.5
0.0
0.0
X1
0.0
X0 1,0
XO
1.0
(a) r
(b) 50
Figure 3: Effects of boundary regularization (r) on activation sets along the boundary. The figures show the results from a neural network with layers of 8 hidden units, applied to the Spacecraft case. The surface represents the first two dimensions with the last four dimensions fixed at O. Increasing results in more organized boundary activation sets.
Table Comparison of N the number of boundary hyperplanes and C coverage of the safe region D of NCBF trained with and without boundary hyperplane regularizer denoted with subscripts and
Case
n
No
C,
Nr=1
Pr=1
N
Pr=10
Nr=50
Pr=50
2
8
26
89.46%
25
0.996
23.3
0.994
13.3
1.006
3
2
16
116
83.74%
119
1.012
111
1.005
98
1.055
OA
4
8
40
91.94%
38
0.988
36
0.993
13
0.937
4
16
156
87.81%
170
0.971
147
1.003
64
1.038
2
8
2868
98.58%
2753
1559
418
SR
6
4
8
6371
98.64%
6218
1
3055
1
627
1
2
16
N/A
N/A
204175
N/A
68783
N/A
13930
N/A
hyperplanes along the zero-level boundary of the CBF without and with regularization, respectively, with r indicating the regularization strength. C. captures the CBF's coverage of the safe region, while P() = Cty/Co represents the safety coverage ratio relative to the unregularized CBF. Notably, "N/A" entries indicate configurations where training a fully verifiable network was infeasible due the excessive number of boundary hyperplanes, which leads the verification process to time out.
The results demonstrate that regularization effectively reduces the number of activation along the CBF boundary without compromising the coverage of the safe region. The efficiency especially improved in cases with greater number of hidden layers, where the unregularized model results in significantly higher number of hyperplanes. For instance, in the SR case with n = 6, = 4, and M 8, the regularization reduces N,=50 627 from N. 6218, maintaining the same safety coverage (Pr=50 = 1). See Appendix B.4 hyperparameter sensitivity analysis.
Figure illustrates the level sets of two CBFs trained for the SR case with
6, L. 4, and M These level sets are extracted from the first two dimensions with the rest set to zero. Each colored patch represents activation pattern. The regularizer organizes the activation sets around the boundary, reducing unnecessary rapid changes and thereby enhancing the verification efficiency.
5.3 Efficient Verification Evaluation
The results presented in Table 2 illustrate significant improvement in verification efficiency for Neural Control Barrier Functions NCBFs using the proposed method. In the table t,, represents the time spent searching for hyperplanes containing the CBF boundary and verifying CBF sufficient conditions on these boundaries, and ty represents the time spent in hinge enumeration and verification.
The total time, T, is the sum of t,, and ty. We compare approach with three baselines, exact verification [23]. SMT- based verification [21] with dReal and Z3. Baseline methods' run times are represented by Baseline (3). dReal, and Z3.
In the Darboux cases, our method achieves verification seconds and 3.3 seconds for M 252 and M 512 respectively, whereas bascline methods take substantially longer, with Baseline 233

---

Table 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
M
f/1
tg
SEEV
Baseline
[23
dReal
Z3
2
256
15
2.5s
0
2.5s
315s
>3h
>3h
Darboux
2
512
15
3.3s
0
3.3s
631s
>3h
>3h
3
16
86
0.41s
0
0.41s
16.0s
>3h
>3h
3
4
8
15
0.39
0
0.39
16.1s
>3h
>3h
OA
3
16
136
0.65s
0
0.65s
36.7s
>3h
>3h
3
128
5778
20.6s
0
20.6s
207s
>3h
>3h
8
8
73
0.54s
0
0.54s
>3h
>3h
>3h
hi-ords
8
16
3048
11,8s
0
11.8s
>3h
>3h
>3h
8
4
16
3984
22.4s
0
22.4s
>3h
>3h
>3h
6
2200
7.1s
2.7s
9.8s
179s
UTD UTD
UTD
SR
6
4
8
4918
45.8s
14.3s
60.1s
298.7s
UTD
taking 315 seconds and 631 seconds, and both dReal and Z3 taking more than 3 hours. Similarly, the OA cases, our method's run times range from 0.39 seconds 20.6 seconds, faster than the baseline methods. In the more higher dimensional systems high-ords and SR, our method significantly outperforms Baseline [23]. Specifically, in high-ordg our methods finishes within 22.4 seconds while Baseline 223 dReal and Z3 times out, due to the need to enumerate the 8-dimensional input space. For the SR case, SEEV's run time are 9.8 seconds and 60. seconds, beating Baseline [23] which takes 179 seconds and 298.7 seconds respectively. Neural barrier certificate based dReal and Z3 are able to directly applicable since they require an explicit expression of the controlled feedback system. However, the SR system is manipulated by an NCBF-based safe controller that is nontrivial derive an explicit expression.
Note that hinge enumeration and certification may be time-consuming procedure, since they involve enumerating all combinations of hyperplanes. However, the results from Table show that the certification can be completed on most hyperplanes with sufficient condition verification in Section greatly improving the overall run time.
6
Conclusion
This paper considered the problem of synthesizing and verifying NCBFs with ReLU activation function in an efficient manner. Our approach is guided by the fact that the main contribution to the computational cost of verifying NCBFs is enumerating and verifying safety of each piecewise- activation region the safety boundary. We proposed Synthesis with Efficient Exact Verification (SEEV), which co-designs the synthesis and verification components to enhance scalability of the verification process. We augment the NCBF synthesis with regularizer that reduces the number of piecewise-limee linear segments at the boundary, and hence reduces the total workload of the verification. We then propose verification approach that efficiently enumerates the linear segments at the boundary and exploits tractable sufficient conditions for safety.
The method proposed in this paper mitigated the scalability issue. However, the synthesis and verification of NCBFs for higher-dimensionall systems is challenging. Exact verification of Ren- NCBFs, which lack ReLU's simple piecewise linearity, remains an open problem.
Limitations:
Acknowledgements and Disclosure of Funding
This research was partially supported by NSF grant CNS-1941670, CMMI-2418806 AFOSR grant FA9550-22-1-000 NSF Career CCF 2047034, NSF CCF DASS 2217723, NSF AT Institute CCF 21 2116665, and Amazon Research Award.
10

---

References
[1] Shao-Chen Hsu, Xiangru Xu, and Aaron Ames. Control barrier function based quadratic programs with application bipedal robotic walking. In 2015 American Control Conference (ACC), pages 4542-455 4548. IEEE, 2015.
[2] Devansh R Agrawal and Dimitra Panagou. Safe control synthesis via input constrained control barrier functions. In 202/ 60th IEEE Conference Decision and Control (CDC), pages 6813-6118. IEEE, 2021.
[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, 15():1211-1229, 2017.
[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 61 612--112. IEEE, 2021.
[5] Hongkai Dai and Frank Permenter. Convex synthesis and verification of control-lyapunov and barrier functions with input constraints. 2023 American Control Conference (ACC), pages 4116 4123. IEEE, 2023.
[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 3528. IEEE, 2023.
[8] 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.
[9] Oswin So, Zachary Serlin, Makai Mann, Jake Gonzales, Kwesi Rutledge, Nicholas Roy, and Chuchu Fan. How to train your neural control barrier function: Learning safety filters for complex input-constrained systems. arXiv preprint ar Xiv: 15478, 2023.
[10] Charles Dawson, Zengyi Qin, Sicun Gao, and Chuchu Fan. Safe nonlinear control using robust neural Lyapunov-barrier functions. In Conference Robot Learning, pages 1724-1735. PMLR, 2022.
[11] Manan Tayal, Hongchao Zhang, Pushpak Jagtap, Andrew Clark, and Shishir Kolathaya. Learn- ing formally verified control barrier function in stochastic environment. arXiv preprint arXiv:2403. 19332, 2024.
[12] Kehan Long, Cheng Qian, Jorge Cortés, and Nikolay Atanasov. Learning barrier functions with memory for robust safe navigation. IEEE Robotics and Automation Letters, 6(3):4931-499) 2021.
[13] Wei Xiao, Tsun-Hsuan Wang, Ramin Hasani, Makram Chahine, Alexander Amini, Xiao Li, and Daniela Rus. Barriernet: Differentiable control barrier functions for learning safe robot control. IEEE Transactions Robotics. 2023.
[14] Hengjun Zhao, Xia Zeng, Taolue Chen, Zhiming Liu, and Jim Woodcock. Learning safe neural network controllers with barrier certificates. Formal Aspects of Computing, 33:437-455, 2021.
[15] Huan Zhang, Tsui- Tsu Weng, Pin- Yu Chen, Cho-Jui Hsich, and Luca Daniel. Efficient neu- ral network robustness certification with general activation functions. Advances in Neural Information Processing Systems, $1:49399494444 2018.
[16] Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems, 33, 2020.
11

---

[17] Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. A convex relaxation barrier to tight robustness verification of neural networks. Advances in Neural Information Processing Systems, 32:9835- 9846, 2019.
[18] Kaidi Xu, Huan Zhang. Shiqi Wang. Yihan Wang. Suman Jana, Xue Lin, and Cho-Jui Hsieh. Fast and Complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In International Conference on Learning Representations, 2021.
[19] Shiqi Wang, Huan Zhang. Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. Advances in Neural Information Processing Systems, 34, 2021.
[20] Huan Zhang, Shiqi Wang, Kaidi Xu, Yihan Wang, Suman Jana, Cho-Jui Hsieh, and Zico Kolter. branch and bound framework for stronger adversarial attacks of ReL. networks. In Proceedings of the 39th International Conference on Machine Learning. volume 162, pages 26591-26604, 2022.
[21] Alessandro Abate, Daniele Ahmed, Alec Edwards, Mirco Giacobbe, and Andrea Peruffo. Fossil: software tool for the formal synthesis of Lyapunov functions and barrier certificates using neural networks. In Proceedings of the 24th International Conference Hybrid Systems:
Computation and Control, pages 1-11, 2021.
[22] Alec Edwards, Andrea Peruffo, and Alessandro Abate. Fossil 2.0: Formal certificate synthesis for the verification and control of dynamical models. arXiv preprint arXiv:2311.09793 2023.
[23] Hongchao Zhang, Junlin Wu, Yevgeniy Vorobeychik, and Andrew Clark. Exact verification of relu neural control barrier functions. Advances in Neural Information Processing Systems, 36, 2024.
[24] 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.
[25] Zengyi Qin, Kaiqing Zhang, Yuxiao Chen, Jingkai Chen, and Chuchu Fan. Learning safe multi- agent control with decentralized neural barrier certificates. arXiv preprint arXiv:2101.05430, 2021.
[26] Zhizhen Qin, Tsui-Wei Weng, and Sicun Gao. Quantifying safety of learning- self- driving control using almost-barrier functions. In 2022 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 12903-12910. IEEE, 2022.
[27] 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.
[28] Stephen Prajna, Ali Jadbabaie, and George J Pappas. A framework for worst-case and stochas- tic safety verification using barrier certificates. IEEE Transactions on Automatic Control, 52(8):1415-1428, 2007.
[29] 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.
[30] Weiye Zhao, Tairan He, Tianhao Wei, Simin Liu, and Changliu Liu. Safety index synthesis via sum-of-squares programming. In 2023 American Control Conference (ACC), pages 732-737.
IEEE, 2023.
[31] Michael Schneeberger, Florian Dörfler, and Silvia Mastellone. SOS construction of compatible control Lyapunov and barrier functions. arXiv preprint arX:022305.01222, 2023.
[32] Andrew Clark. Verification and synthesis of control barrier functions. In 202/ 60th IEEE Conference Decision and Control (CDC), pages 6105-6112. IEEE, 2021.
12

---

[33] Claudio Ferrari, Mark Niklas Muller, Nikola Jovanovic, and Martin Vechev. Complete verifica- tion via multi-neuron relaxation guided and-bound. arXiv preprint arXiv:2205.00263, 2022.
[34] Patrick Henriksen and Alessio Lomuscio. Deepsplit: An efficient splitting method for neural network verification via indirect effect analysis. In IJCAI, pages 2549-2555, 2021.
[35] Huan Zhang, Shiqi Wang. Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. General cutting planes for bound-preed wwtto-ppropo---eeeeeeeeeeee vances in Neural Information Processing Systems, 35: 35:1656-1670, 2022.
neural network verification. Ad-
[36] 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, Part I 30, pages 97-117. Springer, 2017.
[37] Guy Katz, Derek A Huang, Duligur Ibeling. Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljić, et al. The Marabou framework for verification and analysis deep neural networks. In Computer Aided Verification: 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I 31, pages 443 452. Springer, 2019.
[38] 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.
[39] Alessandro Abate, Daniele Ahmed. Mirco Giacobbe, and Andrea Peruffo. Formal synthesis of Lyapunov neural networks. IEEE Control Systems Letters, 5(3):773-778, 2020.
[40] Andrea Peruffo, Daniele Ahmed, and Alessandro Abate. Automated and formal synthesis of neural barrier certificates for dynamical models. In Tools and Algorithms for the Construction and Analysis of Systems, pages 370-388. Springer International Publishing, 2021.
[41] Mahathi Anand and Majid Zamani. Formally verified neural network control barrier certificates for unknown systems. IFAC- PapersOnrrn 56(2))2431-24333 2023.
[42] Yixuan Wang, Chao Huang, Zhaoran Wang, Zhilu Wang, and Qi Zhu. Design-while-verifyy -oooettbby-oonsttuuttio control learning with verification in the loop. In Proceedings of the 59th ACM/IEEE Design Automation Conference, pages 925-930, 2022.
[43] Xinyu Wang, Luzia Knoedler, Frederik Baymler Mathiesen, and Javier Alonso-Mora Simulta- neous synthesis and verification of neural control barrier functions through Franch-and-boud verification-in in-the-loop training. In 2024 European Control Conference (ECC), pages 571-578. IEEE, 2024.
[44] Franco Blanchini and Stefano Miani. Set-Theoretic Methods in Control, volume 78. Springer, 2008.
[45] A. Agrawal, B. Amos, S. Barratt, S. Boyd, S. Diamond, and Z. Kolter. Differentiable convex optimization layers. In Advances in Neural Information Processing Systems, 2019.
[46] 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 Software, pages 1-10, 2016.
[47] 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 490. IEEF, 2012.
[48] 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 3300-3305. IEEE, 2016.
13

---

A Supplement
A.1 Definition of Way (S) and (S)
In what follows, define vectors W (S) E RD and scalars Tiy(S) E R such that zf²
W W + The weight and bias of the input layer is defined by
W (S) = Wiy: (1,j) ES
Ti)(S) = { Tijs (L,j) E else
0,
else
0,
Proceeding inductively, define (S) E Mix to be matrix with columns Wa, (S) for 1. 1..... Mr and (S) E RM to be vector with elements Tiy(S), We then define
W WS-n(S) (i,)) 0,
Tsy(() = W W ( + Tijs 0,
(i,j) E S else
W Wyy(S) =
else
At the last layer, let W(S) = W2(S)9 and F(S) = Ω2 (S) + +/. that y = F(S) if {(.,)): 22) 2 03.
A.2 Proof of Proposition 2
Proof. Suppose that x' E 0D (USes R())). and let denote the state OD found by Line 5 of Algorithm 1 Since ÖD is connected, there exists a path y with 7()) and (1) x' contained in ØD. Let So. S,,...,Sk, denote a sequence of activation sets with Sg E S2x). SK E S(z²), ) and So equal to the set computed at Line 5 of Algorithm [ Then there exists i 2 2 such that S E S and S, & S, and there exists t' such that (t') E (S.)-1) 1) n (S,) n {z b(x) = 0}. We then have that T(S St) is a subset of the set T, and hence S, will be identified and added to at Line 5 of Algorithm
Now, suppose that S S, E S is complete and (N Ro(())) f 6(z) = 0} + 0. Let = T(S S,). Then T is a subset of the sets Si...., S, E S. Since the intersection of the ((S) sets with {a b(x) = 0} is nonempty, (S S } is added to V.
A.3 Algorithm for Verification
SEEV identifies the initial activation set by conducting a BoundaryL.P-aarn based binary search as shown in Algorithm. 2 The algorithm presents procedure to identify a hyperplane characterized by an initial activation set Sn that may contain the boundary @D. It iterates over pairs of sample states from the unsafe training set c and the safe training set Tr. For each pair (ix &rr), the algorithm initializes the left and right points of search interval. It then performs binary search by repeatedly computing the midpoint Øiid and checking the fcasibility of the boundary linear program BoundaryLP(zmia) The algorithm terminates when BoundaryLP(ramm is feasible, returning the activation set (Imma) as Sy-
SEEV utilizes NBFS for enumerating all activation sets along the zero-level set in breadth-first search manner, starting from an initial set So. The algorithm initializes a queue
and a set S with So. While Q is not empty, it dequeues activation set S and checks if the set S E B by solving the boundary linear program MoundaryLLP(S) If so, identified and added to S. The algorithm then explores its neighboring activation sets by flipping each neuron activation (i.j) in S. For each flip, it solves the unstable neuron linear program USLP(S, (i. If USLP is feasible, the new activation set S' obtained by flipping (i.j) is added to Q for further search its neighbors. This process continues until all relevant activation sets are explored, resulting in a set that contains activation sets potentially on the boundary.
SEEV enumerates all hinges VE with Algorithm 4 Algorithm outlines a method to enumerate all feasible hinge hyperplanes formed by combinations of activation sets up to size n. The algorithm takes as input a set of activation sets S and a maximum combination size n. It initializes an empty list to store feasible hinges. For each combination size & from 2 to the algorithm iterates over all activation sets in S. For each activation set S, it generates candidate combinations V. based on adjacency-eithee the set of adjacent activation sets when k 2, the feasible combinations
14

---

for (i,j) j) E (1...., M,, do D- For activation (i,j) of each neurons Check if the neighbor may contain zero-level set Algorithm 2 Binary Search for So
1: Input: Txee TI.
2: Output: initial activation So
3: procedure ENUMINIT(TxYYC, Tr)
4: for &xic Txyc and 2g Tz do
Loop over all pairs of samples
5: Cleft; Bright <- Ex .z
6: Emid = 0.5( + Tright)
7:
while Tieft Fright do then
8:
if BoundaryL.P(Immn Return S (Imid)
D. Check if the Boundary is feasible
9:
Return S ((mmid) as So
10:
W (S Tmid + r(S(x')) 2 then
b Check b(Tmid) >
11:
Fright Emid
Update the right point
12:
else
Fteft Tmid
Update the left point
Algorithm Enumerate Activated Sets
Input: So
2: Output: Set of activation sets S
3: procedure NBFS(Sa)
4: Initialize queue Q with initial activation set So
5: Initialize sets with So
6: while queue Q is not empty do Dequeue S from Q if BoundaryL.P(S) is feasible then i & S then
7:
Dequeue the first activation set from the queue D Check if S is boundary activation set b If S is not already in S
8:
9:
10:
Add S S
11:
if USLP (i, then
13:
Create by flipping activation (i,j) Add S' Q
Add adjacent activation S' to the queue
15: Return
from the previous iteration when > 2. It then checks each candidate combination S. by verifying adjacency and solving the hinge linear program HingeLP(SS, U (S)). If the HingeLP is feasible, the combination added to the list of feasible hinges V. This process continues until all combinations up size have been examined, resulting in comprehensive list of feasible hinge hyperplanes that are essential for understanding the intersections of activation regions.
A.4 Linear Programs for Enumeration
Given state 2t. define the activation set is =s To determine if the activation set S B, we solve a linear program referred to as the boundary linear program. The program checks the existence a state x E (S()))) that satisfies (SS(=,)) F(S(x?)) = 0. The boundary linear
program (BoundaryLP(S( is defined follows.
find s.t.
BoundaryLP(S(22))
((S(a?)) +(((() = E (((()))
(14)
NBFS conducts its search in breadth-first manner. To determine if neighboring activation set, resulting from a flip its (i,j) neuron, may contain the boundary, NBFS solves a linear program, referred to the unstable neuron linear program of USLP(S, (1,5)). This linear program checks the existence of state e X(S) n {x Wyz Táj 0} that satisfies W())z + F(S) 0. The
15

---

Algorithm 4 Enumerate Hinges
1: Input: S, n
2: Output: V
3: procedure HINGEENUM(S,7)
4: Initialize hinge list as an empty list
5: for & from 2 to n do do
Outer loop to iterate over combination sizes Iterate over all activation set
6: for
7:
if k = 2 then
8:
V. - Ns
9:
else
V. - ((k
for each combination S. E V. and & S. do S and Se not adjacent then
D Iterate over combinations
12:
13:
Continue
D skip non-adjacent combinations
14:
if Hingel.P(S (S, U {S}) then
15:
Add V < S. U (S) to v()
b Add to set of corresponding
16:
Add (*)) to V
17:
return hinge_ list
unstable neuron linear program is defined as follows.
find I
s.t.
W(S) =
USLP(S, (i.j))
(15)
( = x X(S)
Finally, enumerate all hinges by solving the hinge linger program HingeLP(S..). defined as follows.
(ingeLP(N(((SS)) find I
W(S) + =0, N XE)(S), VS Ns(
(16)
A.5
Nonlinear Programs for Verification
The correctness condition (7) can be verified for boundary hyperplane X((S) by solving the nonlinear program
minz
h(x:) W(S) x + 0, E X((S)
(17)
s.t.
If we found some state & such that h(x) < 0 and W(S) + +(S) 0. it indicates that the state lies
on boundary of the set but not inside the set C, i.e., x 0D & C. This implies violation of the condition D C C.
Hyperplane counterexamples can be identified by solving the optimization problem
min, max (W(S)T(f(2) g(x)u) u E U}}
(18)
s.t. " 0,
Consider case U (Dw |klloc 1}. The bounded input set U allows replace the maximization over u with L-1 norm (S)" 9x))))) which simplifies the computational complexity, In this case, the problem reduces to the nonlinear program
min Jr
W(S) + IW())* g(x)
(19)
s.t.
= 0, E (()
If 14 = R,,, then by 23 Corollary 1]. the problem be reduced to the nonlinear program
minz
(())
(20)
s.t.
W(S)"g(<) = 0, W(S)z F(S) = 0, E X(())
16

---

The hinge V = {Si..... },) can be certified by solving the nonlinear optimization problem max { +
s.t. x (t)) : .,.,..,, v, l...., r(())) =0
ming
satisfies 4 -
(21)
A.6 Proof of Theorem
Proof. By Lemmal ! the initial boundary activation set So is ensured to identified by the verifica- tion of SEEV in Line 4 Algorithm. [ Given Su and the enumeration in Line 5 and 6 Algorithm. T being complete, the completeness of S and V is guaranteed by Proposition By dReal solving the satisfied. Therefore, by (z) is valid NCBF
equivalent NLPs, the conditions of Proposition [
B
Experiments
B.1 Experiment Settings
Experiment Settings of Darboux:
The dynamic model of Darboux is given as follows.
21 22
22 + 2r
(22)
x1 + 2n x3
We define state space, initial region, and safe region X {x E R2, : : [-2, x 1-
I: {x E R² 0 S < 1, < x22 2 and C {x R² æ + 2 0] respectively,
Experiment Settings of the Obstacle Avoidance: The dynamic model of obstacle avoidance is given as follows.
1
sin vb v cos
0
22
+
(23)
y
0
We define the state space, initial region and safe region X, I and C, respectively as
X' R²= :4, 22, v E [-2, x
[- x [-2,
I: I: x Rd
< Φ - 0.1, -2 22 f -18, -5 < v </6]
(24)
C: R
R
0.04)
Experiment Settings of the Spacecraft Rendezvous: the target using linearized Haaheesy-Wiltshi---tiiii equations, with state x [pas Py: P2, Cny Vy Uz)" control input
The state of the chaser is expressed relative to
Uary Myy
uz]² and dynamics defined as follows.
Pa
1
0
0
Pz
Py
0
Py
0
P=
Us
3n2
0
0
0
0
1
2n
0
0
Pz
+
1
0
0
0
Ur
"l
(25)
Wtg
by
Vyy
02
0
n
0
0
We define the state space and safe region as X. initial safe region X7 and respectively
X'
fxx R$ p, E [-5.5] x 1-1,
I 0.75, where v p3 + pī + D²
(26)
22 + nr + p2 C: { 0.25, where V
hi-ordg: The dynamic model hi-ords is given as follows.
(8) + (7) + 17) + (5) + (2) 39) + 41 12) + (4) - 576 - 0 (27) where we denote the i-th derivative of variable x: by z(0) We define the state space X, initial region X7 and safe region C, respectively as
X' { +.. < 4]
(rs - 1)2 < 1} C : (1) + 2)² +... + (xx + 2)² 2 23
I (x1 +
+......
(28)
17

---

B.2 Synthesis Framework Evaluation
The experimental results presented in Table demonstrate the effectiveness of Counter Example (CE) guided training on Darboux and hi-ords system. In this method, after each training epoch, we calculate the Control Barrier Function (CBF) outputs on representative samples. If the CBF correctly categorizes the samples into safe and unsafe regions, the certification procedure is initiated. If the CBF fails certification, the counter example is added to the training dataset for retraining. Otherwise, training is stopped early.
We capped the maximum training epochs at 50 and conducted three rounds of training for each network structure and system using different random seeds. The results indicate that without CE, the training process could basrely generate CBF that passes certification. In contrast, with CE enabled, there was a success rate of at least 1/3 for most network structure, with verifiable policies generated as few as 10 epochs. This highlights the improvement in training efficiency and reliability with the incorporation of CEs.
No CE
With CE
Case
M
Sr
min epoch
2
8
0/3
3/3
38
2
16
0/3
1/3
10
Darboux
4
8
0/3
1/3
43
4
16
0/3
2/3
26
8
1/3
1/3
15
2
16
0/3
2/3
19
hi-ords
8
0/3
0/3
4
16
0/3
2/3
13
Table 3: Success rates (sr) and minimum epochs required for certification with and without Counter
Example (CE) guided training for different network structures on Darboux and hi-ordg systems.
B.3
Hyperparameters
Table 4
shows values the following hyperparameters used during CBF synthesis:
Na number samples to train CBF on.
dj weight penalizing incorrect classification of safe samples in Equation
02: weight penalizing incorrect classification of unsafe samples Equation
Ay: weight penalizing violation of Lie derivative condition of CBF in Equation 9
de: weight penalizing correct loss for in Equation
Neluster number of clusters in L8 regularization.
k value of l used in generalized sigmoid function to perform differentiable activation pattern approximation.
: the threshold for range-based approximation of CBF boundary.
Case
Nast
Q1
0:2
X
A
neluster
ko
Cboundary
Darboux
5000
100
100
4.0
1.0
N/A
N/A
N/A
hi-ords
50000
100
200
1.0
1.0
N/A
N/A
N/A
OA
10000
100
100
2.0
1.0
5.
1.0
SR
10000
100
100
2.0
1.0
1.0
Table 4: Hyperparameters of CBF synthesis.
B.4 Sensitivity Analysis of Hy perraaarssts
Next, we performed sensitivity analysis of the hyperparameters. chose the case study of Spacecraft Rendezvous with the number of layers L = 4 and the number of hidden units per layer
18

---

X
SR
ME
N
SR
ME
N
K
SR
ME
N
0/3
X
3/3
16.3
3254
3/3
18
3842
10
0/3
2
3/3
17
3265
3/3
15.7
3523
100
3/3
17
3265
4
3/3
17
3352
4
3/3
17
3265
200
3/3
17.7
2922
8
2/3
29.5
3419.5
1/3
10
1984
(a) Ablation study on Ae
(b) Ablation study on X
(c) Ablation study on k
Table 5: Ablation study for training hyperparameters. In each table, the bold lines indicate the baseline setting. SR: the success rate among runs with three random seeds. ME; the average first training epoch when valid NCBF is obtained. N: the average number of boundary hyperplanes.
N = 8. We studied the sensitivity of the training performance to the hyperparameters λg. Xy. and A, in Equation 8, corresponding the weightings for regularizing the number of boundary hyperplanes, NCBF value violation, and NCBF Lie derivative violation, respectively. We also studied the sensitivity the hyperparameter k employed in the modified sigmoid function (=( I+=xp(-k-=] to approximate the regularization pattern. We compared against the settings used the original paper: Äs = 10, A
Å 100, and k 4. For each hyperparameter, we chose four values to perform the ablation study: λạ E {0, 1, 10, 50), ' {1, 4, 8), A E {1, 10, 100, 200), and A E 2, 4, 8). For each setting, performed three runs with different random seeds. We measured the results by Success Rate (SR), Min Epoch (ME), and N, as described in the caption of T
d regularizes the shape the NCBF by penalizing incorrectly categorized samples. Table 5a indicates that when Åe is too small, the training procedure fails to train an NCBF that correctly separates the safe and unsafe regions, resulting in failure of certification. Meanwhile, a larger weight delivers similarly good performance.
A penalizes violations of Lie derivative conditions. Table 5b shows that the result is sensitive this hyperparameter, as this term quickly goes down to 0 when the Lie derivative condition is satisfied. We note that over-penalizing this condition should be avoided since the NCBF would otherwise learn an unrecoverable incorrect shape, as demonstrated by the failure case when 'y = 8.
Àg has been studied in the original paper, with detailed analysis in Section 5.2. The boundary regularization term reduces the number of boundary hyperplanes and benefits convergence.
Table 5c shows the importance of the term & used in the modified sigmoid function. Since this term appears in the exponential part of the sigmoid function, when it is too large, leads to gradient explosions during backpropagation, which crashes the training process. Conversely, reasonably larger better approximates the activation pattern, leading to a reduced number of boundary hyperplanes.
In summary, balancing the hyperparameters is relatively straightforward, as the training performance remains robust across a wide range of hyperparameter values. When training failures do occur, we can sy systematically identify the cause from observation. This enables proper guidance in choosing and adjusting the appropriate hyperparameters.
19

---

NeurIPS Paper Checklist
The checklist is designed encourage best practices for responsible machine learning research, addressing issues of reproducibility, transparency, research ethics, and societal impact. Do not remove the checklist: The papers not including the checklist will be desk rejected. The checklist should follow the references and follow the (optional) supplemental material. The checklist does NOT count towards the page limit.
Please read the checklist guidelines carefully for information on how to answer these questions. For each question in the checklist:
You should answer [Yes], [No] or [NA].
[NA] means either that the question is Not Applicable for that particular paper or the relevant information is Not Available.
Please provide short (1-2 sentence) justificatin right after your answer (even for NA).
The checklist answers are an integral part of your paper submission. They are visible to the reviewers, area chairs, senior area chairs, and ethics reviewers. You will be asked to also include it (after eventual revisions) with the final version of your paper, and its final version will be published with the paper.
The reviewers of your paper will be asked to use the checklist as one of the factors their evaluation. While "[Yes] is generally preferable to "[No]" ", is perfectly acceptable to answer "[No] pprovided proper justification is given (e.g., "error bars are not reported because would be too computationally expensive" or "we were unable to find the license for the dataset we used"). In general, answering "[No] or "[NA] is not grounds for rejection. While the questions are phrased in binary way, we acknowledge that the true answer is often more nuanced, so please just use your best judgment and write justification to elaborate. All supporting evidence can appear either in the main paper or the supplemental material, provided in appendix. If you answer [Yes] to question, in the justification please point to the section(s) where related material for the question can found.
IMPORTANT, please:
Delete this instruction block, but keep the section heading "NeurIPS paper checklist",
Keep the checklist subsection headings, questions/answers and guidelines below.
Do not modify the questions and only use the provided macros for your answers.
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification:
The abstract and introduction clearly states the paper's contributions and scope.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or
NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize other settings.
It is fine include aspirational goals as motivation long is clear that these goals are not attained by the paper.
2. Limitations
Question:
Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Justification:
We point out the limitation on dynamical models Section 2.1 and limitations the type of activation functions throughout the paper.
20

---

Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create separate "Limitations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g.. independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution is low or images are taken in low lighting. Or speech-to-text system might not be used reliably provide closed captions for online lectures because it fails handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and faireess
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory Assumptions and Proofs
Question: For each theoretical result, does the paper provide the full of assumptions and a complete (and correct) proof?
Answer: [Yes]
Justification: We present assumptions in Section 2, and theoretical contributions in Section 4 with proof in the appendix.
Guidelines:
The answer NA means that the paper does include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated referenced in the statement of any theorems.
The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental Result Reproducibility
Question: Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that it affects the main claims and/or conclusions the paper (regardless whether the code and data are provided or not)?
Answer: [Yes]
Justification: We specified random seeds for reproducibility. The code is uploaded with all the commands containing random seeds.
Guidelines:
The answer NA means that the paper does not include experiments.
21

---

If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. w
For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution is specific model and empirical evaluation, it may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access the model. In general. releasing code and data is often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access a hosted model (e.g., in the case of a large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
While NeurlPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily a new algorithm, the paper should make it clear how to reproduce that algorithm. (b) the contribution is primarily a new model architecture, the paper should describe the architecture clearly and fully.
(c) If the contribution is new model (e.g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., registered users), but it should be possible for other researchers to have some path to reproducing or verifying the results.
5. Open access to data and code
Question: Does the paper provide open access to the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, as described in supplemental material?
Answer: [Yes]
Justification:
The code is submitted with the paper.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (nttps://nips.co
for more details.
While we encourage the release of code and data, we understand that this might not be possible, so "No" an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurlPS code and data submission guidelines (https
/ 7/nips. /ttppp.cc/pblic/guideeee http://oeeubiiisssoooooooooo
for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
22

---

Providing as much information as possible in supplemental material (appended to the paper) recommended, but including URLs to data and code permitted.
6. Experimental Setting/Details
Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Question:
Answer: [Yes]
Justification: We provide the detailed experiment settings with hyperparameters in the appendix. We present how to generate training data in Section 3.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, as supplemental material.
7. Experiment Statistical Significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer: [Yes]
Justification: All verification experiments are conducted in a deterministic manner. We also present the success rate of training with random seeds in the appendix.
Guidelines:
The answer NA means that the paper does include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, statistical significance tests, least for the experiments that support the main claims of the paper.
The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g.. Normally distributed errors).
It should be clear whether the error bar is the standard deviation the standard error of the mean.
It is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful to show in tables or figures symmetric error bars that would yield results that are out of range (e.g. negative error rates).
If error bars are reported in tables or plots, The authors should explain the text how they were calculated and reference the corresponding figures or tables in the text.
8. Experiments Compute Resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of exccution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification:
We present the details of the machine experiment on in Section 5.
Guidelines:
The answer NA means that the paper does not include experiments.
23

---

The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount compute required for each of the individual experimental runs well estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't make into the paper).
9. Code Of Ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurlPS Code of Ethics atttps://neurb: httppp/://oorppsscc///b///aaaaas
Answer: [Yes]
Justification: the research conducted in the paper conforms, in every respect, with the NeurIPS Code of Ethics
Guidelines:
The answer NA means that the authors have reviewed the NeurIPS Code of Ethics.
If the authors answer No, they should explain the special cireumstances that require deviation from the Code of Ethics.
The authors should make to preserve anonymity (e.g., if there is special consid- eration due to laws or regulations in their jurisdiction).
10. Broader Impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [NA]
Justification: This paper focuses on the safe control problem of dynamical systems. There- fore it would not harm or raise technology to harm the society.
Guidelines:
The answer NA means that there no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and tied to particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional unintentional) misuse of the technology.
there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML).
11. Safeguards
Question: Does the paper describe safeguards that have been put in place for responsible release of data models that have a high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?

---

Answer: [NA]
Justification: the paper poses no such risks. The experiments we conduct only generate simulation-based data of dynamic systems with such risks.
Guidelines:
The answer NA means that the paper poses such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere usage guidelines restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards challenging, and many papers do not require this, but encourage authors to take this into account and make best faith effort.
Licenses existing assets
Question: Are the creators or original owners of assets (e.g.. code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Answer: [Yes]
Justification: We cited all references in the both the paper and the code Readme file.
Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package dataset.
The authors should state which version of the asset used and, possible, include URL.
The name of the license (e.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (e.g., website). the copyright and terms of service of that source should be provided.
If assets are released, the license, copyright information, and terms of use in the bataasess.ppprsstttt paperswi theode. com/datasets package should be provided. For popular datasets,
has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided. If this information is available online, the authors are encouraged to reach out to the asset's 's creators.
13. New Assets
Question: Are new assets introduced in the paper well documented and the documentation provided alongside the assets?
Answer: [Yes]
Justification:
We upload our code with the submission.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset used.
At submission time, remember to anonymize your assets (if applicable). You can either create anonymized URL or include anonymized zip file.
14. Crowdsourcing and Research with Human Subjects
25

---

Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well as details about compensation (if any)?
Answer: [NA]
the paper does not involve crowdsoureing nor research with human subjects
Guidelines:
The answer NA means that the paper does not involve crowdsourcing research with human subjects.
Including this information in the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included in the main paper.
According to the NeurIPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional Review Board (IRB) Approvals or Equivalent for Research with Human Subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or equivalent approval/review based the requirements of your country or institution) were obtained?
Answer: [NA]
Justification: the paper does not involve crowdsourcing nor research with human subjects. Guidelines:
The answer NA means that the paper does not involve crowdsourcing research with human subjects.
Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.
26


Reviews:
[{"review_id": "0x55sh4MCE", "reviewer": "Reviewer_nDkY", "summary": "This paper proposes a new training and verification method to synthesize control barrier functions to formally prove the safety of a neural network-controlled nonlinear system. The approach used by this paper involves a new verification procedure that systematically enumerates all linear pieces of ReLU neural networks at the boundary of the barrier function via a breadth-first manner, as well as training strategies with various regularizations to ensure that the neural network does not have too many nonlinear pieces and also encourage the satisfaction of the safety condition. During training, counterexamples were also added to ensure convergence. The proposed method is then evaluated on several dynamical systems and the proposed approach outperformed the previous baseline and naive approaches.", "questions": "According to the appendix, several nonlinear programs are needed for the enumeration procedure, and some of them still require expensive solvers such as dReal to solve. Among these nonlinear programs, which ones are harder and take the majority of computation time? Is it possible to further scale up this approach using SOTA neural network verification tools such as alpha-beta-CROWN? A recent work (https://arxiv.org/pdf/2404.07956) has successfully applied neural network verification tools for synthesizing Lyapunov functions, which is also quite related to this work.", "limitations": "A limitation paragraph can be helpful. There are still many unsolved challenges in this field, and while this paper outperforms existing approaches, the scalability is still limited to less than 100 neurons and low dimensional environments, and it cannot be applied to non-ReLU neural networks.", "rating": 6, "confidence": 3, "soundness": 4, "presentation": 2, "contribution": 4, "strengths": "1. The new verification approach, which enumerates linear pieces on the boundary in a breadth-first search manner, is (relatively) efficient and technically novel.\n\n2. The training procedure is carefully designed with several loss terms to aid the synthesizing of neural barrier functions. Some of these loss terms, such as the regularizer to limit the number of boundary hyperplanes, are insightful and may inspire future work.\n\n3. Numerical evaluations are comprehensive and also noticeably outperform existing baselines.\n\nBased on these contributions, I tend to accept this paper.", "weaknesses": "1. The proposed verification procedure is based on enumeration of the linear pieces in a ReLU neural network, and can be slow when the neural network is large. But since the problem under study is very difficult and the proposed approach can outperform naive baselines like directly using SMT solvers (dReal, Z3), this is not a big concern.\n\n2. The training loss involves multiple regularization terms, each with its own regularization parameter. Adjusting these parameters to balance each term can be difficult. It would be ideal to show a sensitivity analysis for these hyperparameters.\n\n3. The writing of this paper can be improved. It is difficult to follow the technical details in this paper as many essential formulations are presented only in the appendix.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "The reviewer is correct that our result involves multiple parameters, including the regularizer coefficients $\\lambda_B$, $\\lambda_f$, and $\\lambda_c$, as well as the parameter $k$ used by the regularizer $L_{B}$. We have included ablation studies of these parameters in the supplemental PDF.\n\nWe thank the reviewer for the feedback regarding the paper presentation. We will improve the readability of the paper by adding an overview figure to Section 4, as shown in the supplemental PDF, and improving the clarity of the notations in the paper. Furthermore, we will move the definitions of the regularizers $\\mathcal{L}_f$ and $\\mathcal{L}_c$ to Section 3 of the paper. Although we will leave the optimization problem formulations (14)--(22) in the appendix due to space constraints, we will provide additional explanations (including derivations of Lipschitz-based relaxations) for each formulation.\n\nThe reviewer correctly points out that our approach, although falls back to expensive SMT/non-linear programs, greatly outperforms the algorithms directing employing them. Our hierarchical pipeline performs cheap sufficient condition checking to quickly reduce the need for solving expensive non-linear problems.\n\nAs for the question regarding the cost of solving nonlinear programs during enumeration, we first apologize for a confusion - there is a typo in the section title of A.5, which is supposed to be written \"A.5 Linear Programs for Enumeration\". The enumeration relies solely on linear programs. BoundaryLP in Eq. (14) is used to determine if S is on a boundary activation set. USLP in Eq. (15) checks if the neighboring hyperplane may contain the zero-level set, while HingeLP in Eq. (16) assesses whether the intersection of hyperplanes may contain the zero-level set. These linear programs can all be solved quickly. To further answer the reviewer's question about the **cost of solving nonlinear programs during verification**, we extend the discussion to \"A.6 Nonlinear Programs for Verification\". The hierarchical verification involves nonlinear programs for sufficient conditions in Eqs. (20) and (21), and exact conditions in Eqs. (19) and (22). Among these, Eq. (22) is the most challenging. However, the difficulty in solving Eq. (22) does not hinder the overall efficiency of the verification process due to the hierarchical design. In the Spacecraft Rendezvous case study, we observed that only 5% of hinge verifications are solved by Eq. (22), taking 3.0 seconds (34% of the hinge verification time).\n\nWe thank the reviewer for the suggestion of scaling up the approach using alpha-beta-CROWN and other NN verification tools. We first note that the referred paper [1] focuses on synthesizing a Lyapunov function, which is different from our contribution in efficient synthesis and verification of neural control barrier function. We will make sure to add the reference to it in the final version. We further note that, in the prior work [15] used as the baseline for our evaluation, NN verification tools such as Linear Relaxation Based Perturbation Analysis (LiRPA) were used to enumerate activation sets at the boundary. Our proposed approach significantly reduces the runtime of this enumeration stage compared to this baseline. For example, in the obstacle avoidance case, [15] used 169.5s for enumeration, while our method used 20.6s. Moreover, unlike many of the existing NN verification works (including the recent work suggested by the reviewer), we consider a continuous-time problem setting. In continuous-time, the verification problem reduces to proving that, for any x with $b_{\\theta}(x) = 0$, there exists control $u$ satisfying $$\\frac{\\partial b_{\\theta}}{\\partial x}(f(x)+g(x)u) \\geq 0.$$ Hence, verifying safety in continuous time requires joint consideration of the reachable set of $b_{\\theta}(x)$ *as well as the gradient $\\frac{\\partial b_{\\theta}}{\\partial x}$*, rendering many of the SOTA NN verification tools not directly applicable. We believe that generalizing such tools to our problem setting is a promising direction for future work and has the potential to further improve the scalability of the verification.\n\nWe plan to include a limitation paragraph in the final version of the paper that contains the points raised by the reviewer, including scalability to higher-dimensional systems and more complex NNs as well as generalization to non-ReLU activation functions.\n\n[1] Yang, Lujie, et al. Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation for Efficient Synthesis and Verification. CoRR, abs/2404.07956.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "9yPdqfuXrn", "reviewer": "Reviewer_bZn2", "summary": "The authors propose a novel approach to synthesize neural control barrier functions (NCBFs) for continuous-time deterministic dynamical systems. Their goal is to synthesize a NCBF to prove the set invariance of the system wrt a given set. In order to do that, the authors propose a verification algorithm to prove that a neural network is a NCBF for a given system based on enumerating boundary segments. The efficacy of the method is evaluated on various benchmarks.", "questions": "Additionally for for the points identified in the Weaknesses Section, consider also the following:\n\n- If I got it correctly, in solving the various non-linear optimization problems to prove that a neural network is a NCBF in practice you are relying on over-approximations and heuristics. Is this correct? If so, why you can call your method exact?", "limitations": "Please, see Weaknesses Section", "rating": 5, "confidence": 4, "soundness": 3, "presentation": 2, "contribution": 2, "strengths": "- The paper consider an important problem that is of interest for the community\n\n- The approach developed by the authors seems sound to me and the empirical evaluation highlights the improved efficiency of the methods compared to other existing approaches", "weaknesses": "- The approach considered in this paper follows closely the approach developed in [15]. While this is not necessarily a problem, I feel that the results in this paper are a bit too incremental compared to the ones in [15]. To limit this risk, it would be important that the authors would extend the discussion in the related works compared to [15]. On this context, I acknowledge that in Table 2 SEEV shows improved computation times compared to [15], but it is not clear if that comes with an increased conservatism (because of the over-approximations introduced in SEEV) or if both methods are guaranteed to always return the same verification value.\n\n- I found some parts of the paper to be non-clear. For instance:\n\na) The overloading of notation of \\mathbb{S} in Section 2.1 makes understanding the rest of the paper hard. In fact, first  \\mathbb{S} is first presented as a function of x and then is used as a set of neurons. Please, be precise and if you overload notation please say it explicitly\n\nb) Proposition 1, I could not find the definition of what it means for a set of activation sets to be complete.\n\nc) Problem 1 is a bit unclear. In fact, according to Proposition 1 a NCBF guarantees invariance with respect to set \\mathcal{C}. But in Problem 1 additionally to that, it is required that a control action keep the system invariant wrt to another set \\mathcal{D}\\subseteq \\mathcal{C}. Why is it this? Please, motivate why you need both of these conditions\n\n- Related to point c) it is unclear how in this paper the authors synthesize a control policy to satisfy Problem 1", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "A comparison of the present paper with [15] is as follows. We note that our paper considers both the synthesis and verification of neural CBFs (NCBFs), while [15] only considered the verification problem. Moreover, while our approach verifies the exact conditions developed in [15], we greatly enhance scalability via the following novel technical contributions: (i) Instead of relying on off-the-shelf tools such as Linear Relaxation Based Perturbation Analysis (LiRPA) to enumerate the activation sets at the boundary of the safe region, we develop an enumeration algorithm that leverages the connectivity properties of the safe region to reduce runtime while maintaining the completeness of the enumeration; (ii) We propose a hierarchical verification approach in which novel tractable sufficient conditions are verified first, and the more complex exact conditions of [15] are only checked if the sufficient conditions fail; and (iii) We propose a new regularizer for training the NCBF that attempts to minimize the number of activation sets at the boundary, and hence minimizes the number of nonlinear programs that must be solved by the verifier. As shown in Table 1 of the paper, this regularizer reduced the number of boundary activation sets from 6,371 to 627 for a six-dimensional system (a reduction of over 90%). Our approach can be interpreted as introducing verification time as a criterion during NN training, and it could be of use in other NN applications.\n\nRelated to the comparison with [15], we emphasize that *our approach is not conservative. It has the same exactness guarantees and is guaranteed to return the same value as [15]*. While we utilize conservative over-approximations as a first step in the verification, the exact algorithms are used whenever the conservative over-approximations fail to return a conclusive result, i.e., either a proof of safety or a safety counterexample. We will revise the paper to make this point clear.\n\nThus, our paper utilizes over-approximations **only as the first stage in the hierarchical pipeline to improve efficiency** -- our verification checks easier problems and then solves harder problems if necessary. The final verification result is both sound and complete as the hinge enumeration and verification step **solves the exact verification problem**.\n\n\nWe will revise the paper to remove the overloaded notation $\\mathbf{S}$. A collection of activation sets $\\mathbf{S_1},\\ldots,\\mathbf{S_r}$ is complete if, for any $\\mathbf{S}^{\\prime} \\notin \\{\\mathbf{S_1},\\ldots,\\mathbf{S_r}\\}$, we have $\\overline{\\mathcal{X}}(\\mathbf{S_1}) \\cap \\cdots \\cap \\overline{\\mathcal{X}}(\\mathbf{S_r}) \\cap \\overline{\\mathcal{X}}(\\mathbf{S}^{\\prime}) = \\emptyset$. We will add this definition to the statement of Proposition 1. \n\nWe clarify Problem 1 and Proposition 1 as follows. The set $\\mathcal{D} = \\{x: b(x) \\geq 0\\}$, where $b$ is the NCBF to be trained, while the set $\\mathcal{C}$ is the given safety constraint. Proposition 1 ensures that $\\mathcal{D}$ is positive invariant and $\\mathcal{D}$ is contained in $\\mathcal{C}$. This condition is weaker than the positive invariance of $\\mathcal{C}$, since there may exist $x_0 \\in \\mathcal{C} \\setminus \\mathcal{D}$ such that $x(t) \\notin \\mathcal{C}$ for some $t \\geq t_{0}$ when $x(t_0) = x_0$. Since $\\mathcal{C}$ is given a priori, it is generally not possible to guarantee the positive invariance of $\\mathcal{C}$. We will elaborate on this point in the text of the paper after Proposition 1.\n\nThe synthesis of a safe control policy for a given NCBF $b$ is discussed in [15] and is omitted from our paper due to space constraints. When $x(t)$ is in the interior of an activation region $\\overline{\\mathcal{X}}(\\mathbf{S})$, the gradient $\\frac{\\partial b}{\\partial x}$ is well-defined and any control input $u \\in \\mathcal{U}$ satisfying $$\\frac{\\partial b}{\\partial x}(f(x(t))+g(x(t))u) \\geq -\\alpha(b(x(t))$$ for some strictly increasing function $\\alpha: \\mathbb{R} \\rightarrow \\mathbb{R}$ with $\\alpha(0) = 0$ will ensure safety. If $x(t)$ lies at the intersection of multiple activation regions $\\overline{\\mathcal{X}}(\\mathbf{S_1}),\\ldots,\\overline{\\mathcal{X}}(\\mathbf{S_r})$, any control $u \\in \\mathcal{U}$ that satisfies $$\\overline{W}(\\mathbf{S_i})^{T}(f(x(t))+g(x(t))u) \\geq -\\alpha(b(x))$$ for some $i \\in \\{1,\\ldots,r\\}$ will ensure safety. We have added a description of how to choose the control policy to the appendix.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "SintFozKMg", "reviewer": "Reviewer_q91P", "summary": "This paper presents an efficient NCBF training and verification framework by leveraging activation regions along the safety boundary. Specifically, reducing piecewise-linear segments acts as a regularizer and nonlinear programs are solves for efficient verificaiton. Experiemnts validates the efficiency of the proposed method compared to the exact verificaiton baselines.", "questions": "See Weaknesses.", "limitations": "There is no explicit Limitation section in the main text or appendix.", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 2, "contribution": 3, "strengths": "The motivation for training and verifying neural CBFs is sound and important, especially for improving the efficiency of exact (complete) verification. Sections 2 and 3 are well-written and easy to follow. I like the idea of regularizer as a training loss to limit the number of boundary hyperplanes, and it is insightful and novel. The experiments are comprehensive, and the effectiveness of the proposed method is validated.", "weaknesses": "- The idea of incorporating verification in the training process by counterexample is not new; it is also called verificaiton-in-the-loop training in the literature [1,2]. The last two terms of training losses in Eq. (8) are also off-the-shelf, which weakens the contribution. The new regularizer in Eq. (9) is not very clear, how to determine k here?\n- Section 4 is poorly organized and looks sophisticated but trivial for each individual part. It is recommended that figures are adopted to illustrate the high-level idea clearly and more details are included in the appendix.\n- For the Hyperplane Verification in Section 4.2, it is hard to find a global solution for nonlinear programming. But if we adopt bounds on the Lipschitz of f and g, the approximation error may cause incompleteness or unsoundness for the exact verification. \n- Similarly, in the Hige Verification, if the sufficient condition is verified for efficiency, the verification will be sound but incomplete, which is OK but not exact. Consequently, the baselines in the experiment should include incomplete verification methods for a fair comparison, or at least the verified rate should be reported compared to the exact verification.\n\n---\n[1] Wang et al. Design-while-verify: correct-by-construction control learning with verification in the loop, 2022\n\n[2] Wang et al. Simultaneous synthesis and verification of neural control barrier functions through branch-and-bound verification-in-the- loop training, 2023", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for providing [1] and [2], and we will include a discussion about these works in the final submission. The reviewer is correct that verification-in-the-loop training is a known approach. The main contribution of this paper is to enhance the scalability of verification-in-the-loop training of NCBFs. We focus on a key bottleneck of existing verification-in-the-loop training methods, namely, the difficulty of performing verification and generating counterexamples in a computationally efficient manner. We make the following contributions in this direction: (i) algorithms for enumerating the boundary activation sets to be verified that leverage the topological properties of the safe region to reduce runtime; (ii) a hierarchical verification approach that first verifies tractable sufficient conditions and then checks exact conditions if no safety proofs or counterexamples can be found; and (iii) a novel regularizer that minimizes the number of activation sets at the boundary of the safe region, and thus incorporates efficient verification as one of the criteria for training the NCBF.\n\nIn Equation 8, the last two terms are widely used in the training of the NCBFs. The first term of Equation 8 encourages fewer linear hyperplanes along the boundary of the obtained NCBF. To do this, we need to penalize the dissimilarity of activation patterns in such regions. To make the computation of this dissimilarity differentiable with respect to the neural network's parameters, we introduced a modified sigmoid function, controlled by $k$, to perform the regularization. Figure 2 visualizes the effectiveness of this approach by showing the reduced variety of activation patterns of the trained neural network, and Table 1 quantitatively studies the number of boundary hyperplanes and the improved verification efficiency by employing this approach.\n\nWe further performed an ablation study on the hyperparameter $k$, which can be found in the supplemental PDF. According to this study, we note that the training performance is robust in the choice of $k$, as long as it is not too large to lead to gradient explosion during the backpropagation stage of training the neural network.\n\nWe will clarify Section 4 by adding an initial figure, as shown in the supplemental PDF, to describe the components of our approach. We will also add detailed descriptions of the algorithms (Appendix A.4) and the optimization problems (Appendices A.5 and A.6).\n\nThe reviewer is correct that it is difficult to directly compute exact solutions for the optimization problems for hyperplane and hinge verification, while conservative sufficient conditions may be more efficient but inexact. Our approach takes advantage of both methods by first attempting to verify safety using sufficient conditions. If the sufficient conditions are not satisfied, then we check safety using the exact conditions. In our evaluation of Spacecraft Rendezvous, we found that around 95% of the hinges can be verified with sufficient conditions, spending 5.9s (66% of hinge verification time), and the remaining 5% of hinges take 3.0s (34% of hinge verification time) when the sufficient conditions fail. Hence, in practice, our approach achieves exact verification with reduced computation time.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "GplOBTePFk", "reviewer": "Reviewer_Ufq9", "summary": "The paper proposes for synthesizing (and verifying) Neural Barrier Certificates with ReLU activation functions.\nThe authors focus on continuous-time systems which are controlled via a control input u(t) and define a dynamical\nsystem as safe if for every state there exists a control output u(t) such that some unsafe region is never reachable.\nTo synthesize Neural Barrier Certificates, the authors build on characterization of ReLU Barrier Certificates by [15].\nIn particular, [15] observed that Relu NNs are piece-wise linear and it therefore suffices to check specific linearly constrained\nregions at the border of the region $\\mathcal{D}$ described by the barrier certificate.\nThe authors then extend prior work in two directions. First, they propose a technique for training ReLU Barrier Certificates\nin a manner that minimizes the number of different linearly constrained regions at the border of $\\mathcal{D}$.\nSecondly, the authors propose an optimized scheme for verification of the resulting constraints w.r.t. the NN.\n\nReferences cited below:\n- [R1] Bak, Stanley, et al. \"Improved geometric path enumeration for verifying relu neural networks.\" Computer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part I 32. Springer International Publishing, 2020.\n- [R2] Wang, Shiqi, et al. \"Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification.\" Advances in Neural Information Processing Systems 34 (2021): 29909-29921.", "questions": "(Q1) I would be really interested to hear something about (O2).\n  In a similar direction: I assume there is some limit on how often I have to choose control actions using the barrier certificate to ensure the dynamical system stays safe?", "limitations": "The limitations of the work become clear throughout the paper.", "rating": 7, "confidence": 3, "soundness": 4, "presentation": 3, "contribution": 3, "strengths": "(S10) The approach presented by the authors makes the work described in [15] much more applicable:\nAs shown in the experiments, both novel techniques improve the performance of the overall approach and push beyond what was analyzable using [15].\n\n(S20) The paper is mostly well-written and provides a good overview of the work.", "weaknesses": "Minor opportunities for improvement:\n\n(O1) In Section 4.1 the paper develops a new algorithm for enumerating linear NN regions along the border of $\\mathcal{D}$.\nI wonder how this technique materially differs from the branch exploration approaches used by branch-and-bound NN verification tools [R1,R2].\nFor example, geometric path enumeration [R1] also enumerates feasible linear regions.\nWhile I agree that this approach would probably not be directly applicable due to the additional constraints w.r.t. the border of $\\mathcal{D}$,\na conceptual comparison might help in making the paper better digestible to the NN verification community.\n\n(O2) For an audience less familiar with neural barrier certificates, it would be helpful to provide insights into how such an NN could be used\nto control a dynamical system in practice. I assume the barrier certificate can somehow be used to choose the correct control signal u at runtime, however, this correspondence is not entirely obvious to me.\n\n\nMinor notes:\n- Line 148: $\\not\\exists u$ makes the text harder to read, I would suggest writing this in english (similarly in other places)", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for suggesting R1 and R2. The branch-and-bound methods for neural network verification perform branch and bound on non-linear units, either in the propagation of spatial data structures as mentioned in R1, or bound propagation as done in R2. In these works, being able to verify in the decision space of size potentially up to $2^n$ (where $n$ is the number of activation units) is done through analyzing and taking advantage of the intrinsic structure of neural networks, thus quickly pruning out large infeasible combinations to achieve verifiability. In our work, once we have identified at least one point that belongs to the border of region $\\mathcal{D}$, we exploit the fact that the border region is connected and we quickly expand from this point to identify the entire border region, without the need to make decisions using branch and bound. In other words, we took advantage of the intrinsic structure of the control barrier function to quickly eliminate the need to search in regions that do not contain the border, as an analogy to how branch-and-bound methods in NN verification can prune out unnecessary search space in neuron space.\n\n\nWe also make the distinction that R1 and R2 are primarily concerned with verifying input and output relationships of neural networks, whereas the verification conditions in Proposition 1 involve nonlinear dynamical systems, which add another layer of complexity on top of NN verification problems.\n\nSafe action can be derived from a control barrier function as a safety filter as described in [1] and [2]. In particular, one may solve the following optimization:\n\n\n$$\\begin{split}\n&\\min_{u \\in \\mathcal{U}} ||u - \\pi_{nom}(x)||^2 \\\\\\\\\n&\\text{s.t.} \\\\;\\\\; L_f B(x) + L_g B(x)u \\leq -\\alpha (B(x))\n\\end{split}\n$$\n\nThe solution to this optimization problem provides a control $u$ that minimally deviates from the nominal control $\\pi_{nom}(x)$, while satisfying the descent condition defined by the control barrier function $B(x)$ in the constraint.\n\nThere is no limit on how to choose the control action filtered by the control barrier function, as a correct control barrier function forms a forward invariant set to ensure the safety of the system it describes.\n\n\n[1] Ames, Aaron, et al. Control Barrier Functions: Theory and Applications. 17th European Control Conference, ECC 2019, Naples, Italy, June 25-28, 2019, 3420–3431.\n\n[2] So, Oswin, et al. How to Train Your Neural Control Barrier Function: Learning Safety Filters for Complex Input-Constrained Systems. CoRR, abs/2310.15478.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:
We would like to thank the reviewers for providing detailed comments that have helped improve the quality of our manuscript. We have provided rebuttals to the comments of each reviewer. We have also attached a PDF file containing additional simulations requested by the reviewers. In this general rebuttal, we emphasize the main contributions of our paper:

1. We propose a hierarchical exact verification approach in which novel tractable sufficient conditions are verified first, and the more complex exact conditions are only checked if the sufficient conditions fail.
2. We propose a new regularizer for training the NCBF that attempts to minimize the number of activation sets at the boundary, and hence minimizes the number of nonlinear programs that must be solved by the verifier.

We would like to further highlight that our approach is not conservative. It provides exact guarantees of the safety properties of NCBF. While we utilize conservative over-approximations as a first step in the verification, the exact algorithms are used whenever the conservative over-approximations fail to return a conclusive result, i.e., either a proof of safety or a safety counterexample.

We look forward to answering further questions during the author-reviewer discussion period.

Meta-review: There is broad consensus among the expert referees that the paper should be accepted for publication. The authors are advised to take into account the detailed reviews as well as the clarifications provided in the rebuttal when revising the manuscript.
Decision: Accept (poster)