Efficiently Computing Local Lipschitz Constants of Neural Networks via Bound Propagation
Authors: Zhouxing Shi
Yihan Wang
Huan Zhang
J Zico Kolter
Cho-Jui Hsieh
Venue: NeurIPS 2022 Accept (2022)
Keywords: Lipschitz
verification
robustness

Abstract: Lipschitz constants are connected to many properties  of neural networks, such as robustness, fairness, and generalization. Existing methods for computing Lipschitz constants either produce relatively loose upper bounds or are limited to small networks. In this paper, we develop an efficient framework for computing the $\ell_\infty$ local Lipschitz constant of a neural network by tightly upper bounding the norm of Clarke Jacobian via linear bound propagation. We formulate the computation of local Lipschitz constants with a linear bound propagation process on a high-order backward graph induced by the chain rule of Clarke Jacobian. To enable linear bound propagation, we derive tight linear relaxations for specific nonlinearities in Clarke Jacobian. This formulate unifies existing ad-hoc approaches such as RecurJac, which can be seen as a special case of ours with weaker relaxations. The bound propagation framework also allows us to easily borrow the popular Branch-and-Bound (BaB) approach from neural network verification to further tighten Lipschitz constants. Experiments show that on tiny models, our method produces comparable bounds compared to exact methods that cannot scale to slightly larger models; on larger models, our method efficiently produces tighter results than existing relaxed or naive methods, and our method scales to much larger practical models that previous works could not handle. We also demonstrate an application on provable monotonicity analysis. Code is available at https://github.com/shizhouxing/Local-Lipschitz-Constants.


Efficiently Computing Local Lipschitz Constants of Neural Networks via Bound Propagation
Zhouxing Shi', Yihan Wang', Huan Zhang', Zico Kolter Cho-Jui Hsieh'
University of California, Los Angeles CCamegie Mellon University Bosch Center for Al zahi@cs. ucla. edu, yihanwangoos ucla. edu, huan@huan zkolterêcs. edu, chohsieh@ca ucla.
Abstract
Lipschitz constants are connected many properties of neural networks, such robustness, fairness, and generalization. Existing methods for computing Lipschitz constants either produce relatively loose upper bounds or are limited small networks. In this paper, we develop an efficient framework for computing the &o local Lipschitz constant of a neural network by tightly upper bounding the norm Clarke Jacobian via linear bound propagation. We formulate the computation of local Lipschitz constants with a linear bound propagation process on a high-order backward graph induced by the chain rule of Clarke Jacobian. To enable linear bound propagation, we derive tight linear relaxations for specific nonlinearities in Clarke Jacobian. This formulate unifies existing ad-hoc approaches such RecurJac, which can be seen as a special case of ours with weaker relaxations. The bound propagation framework also allows to easily borrow the popular Branch-and- sunch-andd-Bond (BaB) approach from neural network verification to further tighten Lipschitz constants. Experiments show that on tiny models, our method produces comparable bounds compared to exact methods that cannot scale to slightly larger models; larger models, our method efficiently produces tighter results than existing relaxed or naive methods, and our method scales to much larger practical models that previous works could not handle. We also demonstrate an application on provable monotonicity analysis. Code is available at https: //github. com/ Latca Consttnnns
Introduction
Lipschitz constants are important for characterizing many properties of neural networks, including robustness 4A
21. fairness 12] 25), generalization [3] and explanation [4]. Local Lipschitz constants, which only need to hold for small local region, more precisely characterize the local behavior a network. Intuitively they characterize how fast the output the network changes between any two input within the region.
IC 45
challenging to exactly and efficiently compute local Lipschitz constants. Naive approaches such as computing the product of the induced norm for all layers cannot capture local information and typically produce vacuous bounds. compute tight and exact local Lipschitz constants, Jordan & Dimakis !2Z! considered small ReLU networks (e.g., up to tens of neurons), by solving mixed-intee mixeedinteggrr programming (MIP) problem to bound the norm of Clarke's 's generalized Jacobian [ However, solving MIP is often too costly and cannot scale to slightly larger networks. On the other hand, RecurJac (59 (an improved version of Fast-Lip (5T) is a specialized recursive algorithm for bounding the Jacobian and computing local Lipschitz constants, which is also relatively efficient but the produced bounds are relatively loose. Moreover, most of the existing works on local Lipschitz constants only used small toy models and cannot feasibly handle larger practical networks.
36th Conference on Neural Information Processing Systems (NcurIPS 2022).

---

Recently, in the field of neural network verification, many methods are proposed to compute provable output bounds for neural networks [26 6
especially, linear bound propagation methods [52] Il are becoming very successful 49 61 because they are scalable and can be efficiently accelerated on GPUs. These methods propagate the linear relationship between layers, where nonlinearities in networks are relaxed into linear bounds. In this work, we ask the question if we can borrow these successful techniques from neural network verification to scale up the computation of local Lipschitz constants to larger and more practical networks.
II:
48 58
In this paper, we aim to efficiently compute relatively tight &o local Lipschitz constants for neural networks using the bound propagation framework. We formulate this problem as upper bounding the & norm of the Clarke Jacobian, and we formulate the computation for the Clarke Jacobian from a chain rule and its norm as a higher-order backward computational graph augmented to the original forward graph of the network. On the augmented computational graph, we generalize linear bound propagation to bound the Clarke Jacobian, and we therehy reformulate the problem of computing local Lipschitz constants under a linear bound propagation framework. On the backward graph, applying Clarke gradients in the chain rule is nonlinear and requires a linear relaxation. It is essentially formed by a group of functions and is different from single activation functions in regular neural network verification. We propose tight and closed-form linear relaxation for Clarke gradients with an optimality guarantee on the tightness, and thereby we efficiently bound the Clarke Jacobian with linear bound propagation. We also show that RecurJac is special case under our formulation where loose interval bounds instead of tight linear relaxation are used for nontrivial cases. Our formulation also allows us to develop scalable and flexible framework enhanced by progress from recent neural network verifiers using linear bound propagation. We demonstrate that we can further tighten our bounds by Branch-and-Bound when time budget allows, for a trade-off between tightness and time cost.
Experiments show that our method efficiently produces tightest Lo local Lipschitz constants compared to other relaxed methods, and is much more efficient than the exact MIP method. Moreover, our method scales to much larger models including practical convolutional neural networks (CNN) that previous works could not handle. We also demonstrate an application of our method for provably analyzing the monotonicity of neural networks.
2 Related Work
For neural networks, a loose global Lipschitz constant (upper bound) can be computed by the product of layer-wise induced norms 44. Based on this product, Virmaux & Scaman 4b considered the effect of activation and approximated upper bounds which, however, are not guaranteed; Gouk et al. [16] used power method for convolutional layers. LipSDP [ used semidefinite programming (SDP) to compute tighter bounds. These works all compute global Lipschitz constants which can be much looser than local Lipschitz constants they have to hold even for distinct input points and they cannot characterize the local behavior of neural networks.
We focus on local Lipschitz constants in this paper. On local Lipschitz constants, LipMIP 24 used mixed integer programming (MIP) to compute exact results. LipOpt [I5] used polynomial optimization but is limited to smooth activations not including the widely used ReLU. LipBaB 4
combined relatively loose interval bound propagation 20 35 17 with branch-and -nduuun-d- compute
exact local Lipschitz constants. All of these methods cannot scale to relatively larger models due to their computational cost. FastLip (5T] and its improved version RecurJac [59] used recursive procedures to bound the Jacobian, and ZLip (3 used zonotope abstract interpretation with a focus on generative models. While these methods are much more efficient, their bounds are relatively loose due to the use of strictly looser relaxations compared to ours. In contrast, compute Eoo local Lipschitz constants efficiently while our bounds are tighter than existing relaxed methods. Besides, there are also several other works on Lipschitz constants under different settings: Avant & Morgansen [2] derived layer-wise analytical bounds but only on a simplified definition for Lipschitz constants, which does not cover Lipschitzness in the entire local region; and Laurel et al. (2]) proposed a dual number abstraction method to bound the Clarke Jacobian but they focused on non -mooth perturbations that can be represented by a single scalar, while we consider high dimensional perturbations.
Lipschitz constants can also be used to train certifiably robust neural networks, by computing margins from Lipschitz constants 45 3] 21 enforcing I-Lipschitzness II
62
22 535 57], These methods

---

are competitive compared to certified training by directly bounding the output B35 17 60
39
50
but they are beyond the scope of this paper as we focus on pre-trained neural networks.
Background
3.1 ReLU Network
Suppose f(x) is K-way neural network classifier given a d-dimensional input x E R and then f(x) E IR For the simplicity of presentation, we mainly focus on feedforward ReLU networks, but our method can also be applied to general network architectures and activations as will be discussed in Section Suppose the network has layers, it takes input ho(x) = x and then computes
Vi E [n], (x) W W.h+-1(x)) + b,:
Vi E In - 1]. hx)x) (x) (x) 2n (x),
where E [ni] means 1 S n, (x) is the pre-activation output of the i-th linear layer with weight W; and bias b; and (x) the output after activation (-)). This formulation is compatible with CNNs since convolutional layers are also linear.
3.2 Lipschiz Constant
The (a, ()_issh-psscitzz constant of network f(x) over open set X' Rd is defined as:
lI((x)) - (x2)lla
I.0.0) (1,)= X1,x,XX, x
sup
(1)
xx x2/1a
If is smooth and (a, Bi-ipshhtt continuous over X, the Lipschitz constant can be computed by upper bounding the norm of Jacobian, i.e., I, (f, X) supxex V fx)) Since neural net- works with non-smooth ReLU activation are non-smooth functions, we consider Clarke Jacobian [ instead, which is defined the convex hull of lim;- fx(x;) for any sequence {x; 1 such that every fxx: is differentiable at x; respectively. We denote the Clarke Jacobian at x as (x)), and then
sup L (0 (f,2)= xEX, ((x))
[[(x)
(2)
Global Lipschitz constant, which considers the supremum over X = Rd, needs to guarantee Eq. (1 even for distant X1, X2, and thus it can be loose and cannot capture the local behavior of the network. We focus on Loo local Lipschitz constants, where X' = (Xy, <) == {xx ||x - X lo < <) is a small -ball -ball with radius around Xg. and take 3 = for the definition in Eq. (T.. While exactly computing Eq. 2 is possible for very small networks [24] 4. for slightly larger networks, we only expect compute guaranteed upper bounds for Eq. ① and Eq. Q and aim to make the upper bounds as tight as possible with an acceptable computational cost.
3.3 Backward Linear Bound Propagation
To bound the Clarke Jacobian, we will use linear bound propagation which is originally used for certifiably bounding the output of neural networks in neural network verification. We adopt backward bound propagation [58 52
41 [3 which typically propagates the linear relationship between the output layer to be bounded and all the previous layers it depends on, in a backward manner. Suppose want to compute certified bounds for output layer h, (x) w.r.t. all from small domain B (xp, c). Starting from the output layer, we take A, = I, and then (x) = (x). For every i E [m)) suppose (x(x) be bounded by linear functions w.r.t. h (x) parameterized by
P, P. 9 q, (the bounds element- hold):
P. P, - q, S hx(x) < P,h,-1(x) q.
(3)
Then for every = n1 1,... in order, A (x) can be recursively bounded by substituting hx()) with Eq. 3
(xhx(x)= & A c A = A P IAJ- & = [A.+ + AA.-gg (4)
3

---

Forward graph (original neural network computation)
2x
h2(x)
(x,,
hg04)
Av
Norm
J((K)
(x)
Backward graph (norm of Clarke Jacobian)
Figure 1: Illustration of our proposed framework where we formulate the computation for local
Lipschitz constants by augmenting the original computation graph of the neural network (forward graph) with an additional subgraph for computing the norm of Clarke Jacobian (backward graph). The backward graph relies on the pre-activation values (z (x). ... Zn-1 (x)) the forward graph to compute the Clarke gradient of activations. Linear relaxation for two categories of nonlincarities in the backward graph (nodes in purple), norm (I]J (x) and Clarke gradient (o'), are detailed in and Figure g We also perform branch-an aanechh-nd-bbund (BaB) to tighten the bounds by branching pre-activation nodes in the forward graph (nodes in green).
Figure Figure 2
where [:]+ stands for taking positive elements from the matrix vector, and vice versa for [:]- A stands for the coefficients of the linear relationship propagated from layer i to layer i- and c, is backward manner and accumulating (i (i [nz]], eventually bounds are propagated to the input layer h, (x) I Agx + Σ C₁ which directly represents the linear relationship between the output layer and x. We can eliminate from Agx to obtain the final bounds. When X B (Xo, c), for the j-th dimension of h, (x). we can use the fact that [An]i. x S [An]i.Xo e + |A))) where [Ao]j:: stands for the j-th row in Ag-
bias term produced this layer. By this recursive procedure
Parameters in Eq. 33 can be obtained by considering the relation between 1x(x) and 1x-1(x). We can first obtain bounds 1, S 24 (x) S u, using bound propagation by viewing 2; as the output layer. Then linear relaxation bounds activation ha (x) = (x)(x)) with linear functions of (x):
VI, S 2 (x) S Us (x)
I (z) S 8x;;(x) + E.
(5)
[īl are two lines bounding a ([=(x)];)) against input [x]]] We provide detailed derivation and illustration for ReLU in Appendix A.I Then to satisfy Eq. B we can take:
Intuitively, for the j-th neuron, [x, + راا and (x)] +
P. diag(s,) W., P. diag g. diag(s, )b + t, q. diag t.-
Interested readers can find more details of backward bound propagation the literature this work, we generalize this linear bound propagation to bound the Clarke Jacobian.
In
4 Methodology
We present our method in this section. We first formulate the local Lipschitz constant computation as a higher-order backward computational graph, and use bound propagation to obtain the bounds of the Clarke Jacobian. We discuss methods for tightly bounding nonlincarities in Clarke Jacobian, and we show that RecurJac [59] is a special case with looser interval bounds. Finally, we use Branch-and-Bound to further tighten the bounds.
4.1 Clarke Jacobian for ReLU Networks
In ReLU networks, the ReLU activation for single neuron is defined as (x) = max(z, 0} which is non-smooth x =0 We consider its Clarke gradient [X] denoted as (z): when < do (z) (0): when æ >> 0, (z) {1}; and when 0, do(x) ()) = [o, 1]. For the i-th layer (1 (1< < n). we use ((x((x)))) to denote the Clarke gradient of the j-th neuron and da (xx to denote the Clarke
gradient for all neurons in the layer. And we use a diagonal matrix (x(x) E (x))) to denote
Clarke gradient of neurons in the i-th layer layer, where (x)),, E do (a[[2 (x)];) Then chain rule
can be used to compute the Clarke Jacobian for the whole network 22
24
Denote Jx(x) E 0f(x) 8h

---

as Clarke Jacobian w.r.t. the (t-1)-th layer in the chain rule. We have J,.()) = Wa. and for all i [n- 11. we have
J((x) 0f(x) dh)-1(x:) { (X), J++1(x) E (x)
0f(x)
Ax(x) (0((2())))
(7)
Finally JI (x) E 0x( is a Clarke Jacobian of the entire network 24 Since f(x) E R and
a E IR,, we have (x) E Rxxd d As we aim to compute the fxc local Lipschitz constant, we upper bound (x)( (JI(x) E Of())) w.r.t. all x E X.
Given the forward pass computation of the original network, we can formulate a computational graph for [
ooo in a backward pass accordingly as shown in Figure [ We augment the original forward graph with backward graph, where the backward graph has a dependency on the pre-activation outputs of layers in the forward graph, due to A1, A2, An- We build the augmented graph by traversing the forward graph, similar automatic differentiation for neural network training. The formulation with a computational graph allows our method to easily generalize to different network
architectures given the existing bound propagation framework for general neural networks [53]]
We use the bound propagation framework described in Section 3.3 to upper bound [] (x) || On
the backward graph, when bounds are propagated to Jx),), similar A; and c; in Eq. A
A; to denote the coefficient matrix and è to denote the bias term for the backward graph, and then we have:
Vi [m], (x) S J(()),
Σ Cj-
Note that we have A, on the right of (x) rather than the left, since (x) multiplied on
needed for bounding the forward graph, we also need intermediate bounds L, S Jx(x) S U, (Vx E X') for the backward graph by starting bound propagation from (x) instead of [ (x) l| oe. These intermediate bounds are used in the linear relaxation for nonlinearities in the backward graph. There are particularly two categories of nonlinearities be tackled on the backward graph: 1 norm in [[J (x) 2) (ViE ( (n 11] in Eq. 7 which applies the Clarke gradient of ReLU on the later layer's Clarke Jacobian. We handle them in Section 4.2 and Section 3 respectively. Then bounds can
the right of (x) in Eq. 7 As intermediate bounds for 2, (x)
be propagated starting at | (x)]l to J1 22) (x)), Jn x in order. Bounds are eventually
propagated to J, (x) Eq. (8) with i n, where (x) can be substituted with W. a, and thereby
we obtain a final upper bound for [[J (x)]loo
4.2 Norm of Clarke Jacobian
The & norm of Clarke Jacobian is the first nonlinearity we would encounter during backward bound propagation, as it is the last node in the backward graph (see Figure [T. The norm is computed as [x) = maxisksk Σ [J [x)] where K rows in J (x) can be bounded separately, and after that we can aggregate results on K rows by taking the max. For the simplicity of the following
analysis, we assume K as we handle one row in J (x) at each time, but they can still be
batched in implementation. Then Clarke Jacobian (x(x) (i E [nl) and its bounds L;, U, can be viewed as row vectors, and we will use F-l, denote the j-th element.
By a tight linear relaxation for - as shown in Figure 5 in Appendix A.2 (only the upper bound is needed), we have the following bound for [ (x)]l=o
Proposition 1 (Linear relaxations for matrix || Il norm). For all x E X, suppose Vj [d], [LI S [J (x)], - [U1]j. and J, (x) is a row vector, we have a bound for its matrix ||. ol norm:
|J [x]( (x)x + Co.
U1}
Lb
[ily < [U,]
where (Aıl
[11} L
[oo; - (A,; + +Lbb]
0
Lily = [U1]
We prove it in Appendix D.I and this propagates bounds from the norm of Clarke Jacobian to J (x).
5

---

4.3 Clarke Gradient of Activation Functions
For each layer i [n - 1] in the chain rule for computing the Clarke Jacobian as Eq. 7 in addition to the fixed weight matrix W, there is J J++1(x
term, where (x is determined by pre- activation value (x) from the forward graph. For the j-th neuron in the layer, [J (x)],
x
When [u,] < 0 or [b] > 0, we have [A,(x)] = 0 and [A, (x) = respectively fixed, and then for these special cases (x)) already linear w.r.t. [J)+((x]] and thus linear relaxation is not needed. Otherwise, [J+41 (x (x))),()),, is nonlinear, since both (x)(()); and [A(x)]as may vary given different x E X. We thereby relax the nonlinearity [J:41 (x)] (x)x for [A, (x)x) = [0, 1].
As illustrated in Figure 2 the solid blue line and solid red line are the exact upper and lower bound
respectively for Jx+1(x) [ ( which are piecewise linear w.r.t [J)1(x)], When [[41] 2 0
or [U1+1l5 S 0, ( can be exactly bounded by linear functions w.r.t. [J++((x]]}=
{ - [J+1 (x))) S U+)1(x)]s when Le+1l 2 0, (x)م)) = [0. 1].
(9)
(x) S [Ja+ (x) S when [U S 0, [A, (x) [0, 1].
Intervel Bounds [Ours]
oiJ,,,(X) (x))
(x,,
J(xx
4
(x)),,(0))
(x,
-2-
2,00
Figure 3: Computation graph for bounding each Clarke gradient. It is the internal compu- tation for boxes in Figure [ Two ReLU nodes are inserted as per Proposition 2 In bound propagation, the a' node takes intermediate bounds from z; (x) to decide whether bounds are directly propagated from 1++1(x) (no re- laxation needed), or indirectly via o (J(+ and ( ++ (x)) (with relaxation), for each neuron respectively.
-3
-2
Figure 2: For neuron j in layer i, when [Ax(x)];
= [0. 1], we plot [],+1(X] (x)); as a group of functions w.r.t. (x)], (violet area). In this example, -1.5 S (x)]; linear relaxation (dashed blue and green lines) is much tighter than interval bounds (dashed green lines) by Zhang et al. 559
1.5. Our
The most nontrivial case appears when Letaly
< [U++]] where exact bounds for [J++1 (x)) are nonlinear given the input region. We relax the exact bounds into linear bounds that can handled by linear bound propagation. We observe that the exact upper bound essentially ReLU function of J.+1 (x) (solid blue line in Figure 2) and the exact lower bound can be viewed as ReLU function flipped both horizontally and vertically (solid line in Figure 2h. Formally, we
have:
Proposition 2 (Exact lower and and upper bounds for the Clarke gradient of a ReLU neuron). For the j-th neuron in layer i(i E(EElp [n - 1J), if (A, (x)li = 1]. we have:
[x++(x) 2 min min((J+11(x), 0}, (x))())A,(x)) S max (ax(([+4(x)))))) 0}. which can be rewritten using ReLU activation:
(10)
min [1+1 (x)], 03 -o
max (x)],, 0) o(J+((
(11)
Its correctness can be easily verified by considering the sign of [J (x)l; as shown in Appendix D.2
We then decompose (x),(()),,()) into two ReLU activations (Eq. as illustrated in Figure
ReLU can be further relaxed by Eq. (). as derived in Appendix D.3 which yields:
Proposition 3 (Linear relaxations for Clarke Jacobian of a ReLU neuron). For the j-th neuron in the
i-th layer (i E [n 11), given (x) [o, 1] and [Ly $ [J++((x)], S [U++1]5- we have the following relaxation:
[J+1(x) 2
+ E. 1b, (x))) S B [J+z [x)]; + E

---

-01-UU+11 (aaul))++((l00 +o(-(Latl))
where
[+41l E Li+tls - a( -Li++
[
Litils
o [+
[Ttily - (4 (LL+1lg))
[0 10,+
L+
The linear relaxation in Proposition 5 corresponds to dashed blue and red lines shown in Figure 2 for the relaxed upper bound and lower bound respectively. And Eq. is special case for the relaxation Proposition 3 the following theorem, we show that relaxation Proposition is the tightest
linear relaxation:
Theorem 4 (Optimality of linear relaxations for the Clarke gradient of a ReLU neuron). For the j-th neuron the i-th layer (i [n 1),, and any linear bound coefficients s, t,, 3, satisfying
WJE [Lttlls ( e 1). &J + (x) 3J +1, (12)
((),(x))s
we show that they produce looser relaxations:
(s, t) * (15, (((s))))
= M[L+
sJ + < 1 + faml
(s, 2) + (1++1 (tr+)ls)
[J<tals<J<(U.. 3J +
[ J + [t.tly
where 11 ززري [5 11
1s are defined in Proposition
This theorem, proved in Appendix D.4 states that our proposed linear relaxation is provably tighter than any other valid linear relaxation. While there are previous works tightening the linear relaxation for activation functions [58] 6EL 154, we consider the optimal linear relaxation for a group of functions (as shown in Figure 2 instead of a single activation function, and our relaxation closed-fon fooed-fommm with a provable optimality, without gradient-base based optimization
4.4 Connections to RecurJac
While RecurJac is recursive algorithm specialized for local Lipschitz constants and it was not related to bound propagation in the original paper, we find that is essentially a special case under formulation with linear bound propagation, but it uses looser interval bound relaxation instead of our tight linear relaxation proposed in Proposition propagation is also a special case of linear bound propagation, but interval bounds use relaxation with zero slope only instead of general non-zero slopes). Figure 2 shows a nontrivial case where [0. 1]. RecurJac takes interval bounds the horizontal
2 and Proposition (note that interval bound
[L+1l 0 < [U,+1]5 and (x),, green dashed lines with a zero slope, and the interval bounds are looser than our linear relaxation with non-zero slopes, i.e., the gap between upper and lower bounds is larger. In Appendix E show that if we use interval relaxation when [Ls+ i| < 0 < [U,- our framework will be equivalent to RecurJac. Compared to RecurJac, propagation but also produce tighter results.
only have more general formulation with linear bound
4.5 Branch and Bound
Formulating the backward computational graph also allows to utilize recent progress in linear bound propagation for neural network verification, to further tighten the results. In neural network verification, Branch-and- Bound (BaB) has been used to compute tighter bounds 226 5. 4 54
49 by branching activations or input and then bounding each smaller subdomain respectively. We also utilize BaB to tighten our bounds when time budget allows.
We denote Co = {l,, u1). (l2, uz), -. (L, un-1)} as the domain of all pre-activation bounds of ReLU neurons in the forward computational graphs before BaB. We use C' to denote pool of domains that we currently have, and initially C = (Co). BaB aims to recursively split domains in C into smaller subdomains C1, C2 where Co C, UC ...,, and bounds for each subdomain can be computed respectively using bound propagation, as linear relaxation can generally be tighter with smaller domains.
At each iteration, we take domains in C with loosest bounds, where B is the batch size for BaB. For each domain, we choose a layer and ReLU neuron j in layer on the forward graph, such that the
7

---

neuron has uncertain Clarke gradient (1:); < 0 (u: We branch this domain into two subdomains by branching ([b]g- (u]];) into (1+1). and (é, [1:])) respectively, where é is a sufficiently small value (e.g,, 10 100-), )) so that the Clarke gradient for the branched neuron becomes certain in each subdomain (0 and 1 respectively) with other neurons unchanged. We compute the bounds for the new subdomains, and we repeat this process until reaching time limit or there is no domain left to branch. Finally, the bound of the domain with the loosest bound in C is the tightened result.
We use a heuristic score decide which neuron branch for a given domain, by estimating the potential improvement to the bounds [6. For branching a ReLU neuron on the forward graph, we estimate the potential improvement on the backward graph. Suppose neuron j in layer i is branched, we estimate the gap between the lower and upper bound in the liner relaxation, as the gap can be closed after the branching. We estimate the gap (the gap between the blue dashed line and the red dashed line in Figure 2 as ([U;+1] 11)+ and we multiply it by coefficient [Ag]] from the bound propagation as the heuristic score. We thereby branch neurons with highest scores.
5 Experiments
In the experiments, we focus on evaluating the tightness of lo local Lipschitz constant bounds and the computational cost. There are three parts: 1) We compare the tightness and efficiency relatively small models and synthetic data, to accommodate slower basclines; 2) We also use practical image datasets with larger models; 3) Finally, we demonstrate application of our method on analyzing the monotonicity of neural networks. Additional experimental details are provided in Appendix g
Baselines We compare our methods to the following baselines: NaiveUB multiplies the induced norm of each layer, which can scale to arbitrarily large models but the bound is often vacuous. LipMIP 24 computes exact and tightest local Lipschitz constants using MIP but can only work for tiny models. During the process of solving MIP, an upper bound of the result may be available and is gradually improved, and thus for models that LipMIP cannot finish within a time budget, we report the upper bound obtained at the timeout. LipSDP I3
computes upper bounds of &g local Lipschitz constants using SDP, and we convert their & results into upper bounds for the loo by vd factor. Since LipSDP by itself does not support the loo case which may not be the intended use of LipSDP, the results converted from the &g case are for reference only. LipBaB 4 uses loose interval bounds with branch-and-bound JecurJaa (59] is a recursive algorithm computing relaxed local Lipschitz constants which can be seen as special case of ours with weaker relaxations. The baselines except NaiveUB do not support CNN in their implementation, and we convert the CNN models to equivalent MLP models for these baselines.
Table I: Local Lipschitz constant values and runtime (seconds) on MLP and CNN models with growing width for a 16-dimensional synthetic input data point. Smaller values are tighter results. Width for MLP stands for number of neurons in each hidden layer, and width for CNN stands for number of filters in each convolutional layer. "C" and "F" in the model names for CNNs denote the number of convolutional layers and fully-connected layers respectively. We set timeout of 1000s for LipMIP and LipSDP, and 60s for BaB. +** denotes that we report the upper bound LipMIP returns at timeout, and "_" means LipSDP cannot return upper bound at timeout.
Layer MLP
CNN-2CIF Widh= Runtime
Method
Width=32
Width=61
Width=128
Width=l Runtime
Widht=16 Runtime
Value
Runtime
Value
Runtime
Value
Runtime
Value
Value
NaiveUB
24.31
0.05
33.02
0.01
49.39
0.00
24.38
0.00
39.99
0.01
$1.68
0.03
LipMIP
12.13
16.25
102.64
1,000.05*
456.89
1.000.12*
9.54
1,000.08*
57.88
1,000.17
628.91
1.000.40*
LipSDP
11.01
27.27
11.03
729.92
LipBaB
12.13
2.92
30.59
63.16
73.71
60.98
5.39
61.62
15.34
61.43
36.40
81.82
Recurlne
12.38
17.40
20:25
17.07
47.23
16.66
5,02
16:21
9.02
16.73
38.19
16.38
(wle BaB)
12.28
6.42
35.66
4.69
7.29
8.41
7.40
7.29
Ours (w/ BaB)
12.13
8.13
16.30
13.57
28.69
60.10
4.69
7.39
8.19
$2.29
28.6
60.1
5.1
Comparison on Synthetic Dataset
We follow Jordan& & Dimakis [Z4 and train several small models on a synthetic dataset. We compare different methods on models with varying width shown in Table [ and we also show results with varying depth and in Appendix B.T Some of these models are already large for LipMIP and we set time limit of 1000 seconds. For our BaB, we stop further branching after 60 seconds.
8

---

Without BaB, our method is very efficient while it already outperforms the baselines on tightness except for LipMIP on the smallest MLP. Compared to LipMIP, for the smallest MLP on which LipMIP does not timeout, our result without BaB is very close to but larger than their exact result. This smallest model serves as a sanity check to validate that our results should be no smaller than LipMIP's exact results. For other relatively larger models, LipMIP cannot produce exact results within the timeout and our result is much tighter than the upper bounds by LipMIP after 1000 seconds. And LipSDP fails to yield results within the timeout on many models. Although LipBaB has BaB to tighten the bounds, their results are still loose within the time budget, since using loose interval bounds in their BaB is inefficient. RecurJac is relatively efficient baseline but still returns looser bounds compared to our method with tight linear relaxation. Our BaB further improves the bounds and consistently produces tightest results within reasonable time budget.
5.2 Comparison on Image Datasets
Table 2: Average local Lipschitz constant values and runtime (seconds) on MNIST. The Lipschitz constants are evaluated on the first 100 examples in the test set. We set a timeout value of 120s for LipMIP and 60s for BaB. "*" denotes that we report the upper bound LipMIP returns at timeout, and "_" means LipMIP and LipBaB cannot return any valid upper bound at timeout on the CNN model.
3- layer MLP
CNN CNN-2C2F
Methed
Value
Runtime
Value
Runtime
NaiveUB
3,257.16
0.00
80,239.62
0.00
LipMIP
14,218.991 .9*
120.51
LapBaB
947.69
Recurlac
1,091.31
0.22
12,514,55
115.43
Ours (w/o BaB)
688. 15
4.95
5,473.03
8.21
Ours
397.25
52.23
5,458.84
60.04
Table Average local Lipschitz constant values and runtime (seconds) on CIFAR-10 and Tinylma- geNet. The Lipschitz constants evaluated on the first 100 examples in the test set. RecurJac's original implementation cannot handle large models here and its results are obtained by supporting its relaxation in our implementation.
Dataset Model
CIFAR-10 10
TinyImageNet
CNN-2C2F
CNN-4C2F
CNN-2C2F
CNN-4C2F
NaiveUB
1707252.88
365293440.00
1512185.25
87148664.00
Recurlac
79275.44
12502332.00
24031.58
714189.12
Value (ours)
18638.14 14
1049447.88 88
4556.61
25096.26
Runtime (ours)
11.17
29.79
95.42
137.04
Table 4: Percentage of examples which the predicted confidence for high income level is monoton- ically increasing (1) or decreasing (L) w.r.t. each feature, by Recurjac and our method respectively.
Method
Monatonicity
Age
Education num
Capital gain
Capital loss
Hours per per-week
32%
55%
0%
4%
95%
RecurJac
0%
0%
0%
0%
40%
58%
5%
98%
Ours
0%
0%
0%
0%
0%
To further evaluate the scalability of different methods to relatively large models, we then conduct experiments on image datasets including MNIST (30], CIFAR-10 (7],, and Tiny [9]. We use 3-layer MIP and 4-layer CNN on MNIST, and we use 4-yer and 6-yayer CNN models on CIFAR-10 10 and TinyImaget Imageeee.... All the models here are too large for LipSDP. LipMIP and LipBaB can only handle the MLP model on MNIST, and they cannot return any valid upper bound for the CNN models within a reasonable time budget. RecurJac can handle the CNN model on MNIST, but other CNN models CIFAR-10 and TinylmageNet are still too large for RecurJac after converted to equivalent MLP models. In contrast, our formulation with linear bound propagation allows us to utilize the efficient bound propagation for convolutional layers from Xu et al. [53] Since RecurJac is a special case under our formulation, we implement RecurJac's loose relaxation to obtain results for Recurlac CNN models.
We show results on MNIST in Table 2 Our results are much tighter compared to the baselines even do not enable BaB, and BaB can further tighten results. On CIFAR- 10 and Tiny

---

do not enable BaB on to save time cost on relatively larger models, and we show results in Table 3 Our method can scale to these larger CNNs that previous works could not handle. And our results are much tighter than UB and also RecurJac reimplemented in bound propagation. We present additional results on models with different random initialization in Appendix B.2
5.3 An Application on Monotonicity Analysis
We further use an application to demonstrate that our method can be used to verify the monotonicity of neural networks. Given network, we aim verify whether the network's output monotonic function w.r.t. each input feature. Monotonicity can be preferred properties in some real-world + this experiment, we adopt the Adult dataset [5]. with a binary classification task about predicting income level. There are only several continuous features, and we aim to check the monotonicity of income level w.r.t. age, education level, capital gain, capital loss, and hours per week. We train an MLP model and verify its monotonicity on the first 100 test examples, Signs of Clarke Jacobian can be used to check monotonicity 37,, and we achieve it by checking the bounds of Clarke Jacobian. For each continuous feature j. we set an input domain X; where only this particular feature can be varied between the minimum and maximum possible values in the dataset, while we keep other features fixed. And then we obtain bounds on the Clarke Jacobian of the output class for high income level, as L1 S (x(x)= < U, (Vx E X2)- Then if [L]] > O, the predicted confidence on high income level is monotonically increasing w.r.t. feature j. and vice versa. We count the percentage of examples that satisfy each type of monotonicity respectively. We show results high income level is monotonically increasing w.r.. age,
scenarios 40
in Table E The predicted confidence education number, and hours per week on at least part of the examples, which is reasonable. On the other hand, the models learn little monotonicity capital gain or loss features. Compared to RecurJac, ac, our method verifies more monotonicity. We expect the gap to be larger when the models and datasets are larger.
6 Conclusion
In this paper, we propose an efficient framework to compute tight &oo local Lipschitz constants for neural networks by upper bounding the norm of Clarke Jacobian, and we formulate the problem with linear bound propagation. We model the computation for the Clarke Jacobian as a backward computational graph and conduct linear bound propagation the backward graph. We propose tight linear relaxation for nonlinearities in Clarke Jacobian with guarantees on the optimality. And we further tighten bounds with branch-and-bound when time budget allows. Experiments show that our method efficiently produces much tighter results compared to existing relaxed methods and can scale larger convolutional networks on which previous works cannot handle. We also use our method to analyze the monotonicity of neural networks as a potential application.
Limitations There several limitations in this work and challenges for future works. It is still difficult for the proposed method to scale to deeper neural networks such as ResNet (1] with tens of convolutional layers ImageNet (TO). It is also a common challenge in neural network verification, where efficiency and the tightness of certified bounds can be very limited on deep models. Besides, we have only focused on foo local Lipschitz constants in this paper but not other norms. Linear bound propagation computes certified bounds for each neuron respectively and thus aligns better with fxx norm. Bounds may become significantly looser if is applied to other norms such as & norm. Previous state-of- off-the-rt works (24]
59 [3] on local Lipschitz constants did not consider both E. norm and &g norm simultaneously either. Handling other norms challenge for future works. Moreover, in addition to verifying pre-trained models and computing local Lipschitz constants, we have not utilized the proposed method to train neural networks with stronger certified guarantees on Lipschitz constants or robustness, and it remains challenging for future works to better align verification and training.
Funding Disclosure
This work is supported in part by NSF under IIS-2008173, IIS-2048280 and by Army Research Laboratory under W91 NFF20-2-0158. Huan Zhang is supported by a grant from the Bosch Center for Artificial Intelligence.
10

---

References
[1] Anil, C., Lucas, J., and Grosse, R. B. Sorting out lipschitz function approximation. In International Conference Machine Learning, volume 97 of Proceedings of Machine Learning Research, pp. 291-301, 2019.
[2] Avant, T. and Morgansen, A. Analytical bounds on the local lipschitz constants of relu networks. arXiv preprint arXiv:2104. 14672, 2021.
[3] Bartlett, L., Foster, D. J., and Telgarsky, M. Spectrally normalized margin bounds for neural networks. In Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, pp- 6240-6249, 2017.
[4] Bhowmick, A., D'Souza M., and Raghavan, G. S. Lipbab: computing exact lipschitz constant of relu networks. In International Conference Artificial Neural Networks, pp. 151-162, 2021.
[5] Blake, C. Uci repository of machine learning databases. http://www. ics, uci. edu/ mlearn/ML- Repository, html, 1998.
[6] Bunel, R., Turkaslan, I, Tomr, P. H. S., Kohli, P., and Mudigonda, P. K. A unified view of piecewise linear neural network verification. In Advances in Neural Information Processing Systems, pp. 4795 2018.
[7] Bunel, R., Mudigonda, P., Turkaslan, I., Torr, P., Lu, J., and Kohli, P. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21 (2020), 2020.
[8] Clarke, H. Generalized gradients and applications. Transactions of the American Mathemati- cal Society, 205:247-262, 1975.
[9] Daniels, H. and Velikova, M. Monotone and partially monotone neural networks. IEEE Transactions on Neural Networks, 21(6))9069917, 2010.
[10] Deng, J., Dong, W., Socher, R., L., L.,, Li, K., and Li, Imagenet: A large-scale hierarchical image database. In The IEEE Conference on Computer Vision and Pattern Recognition (CVPR), pp. 248-255, 2009.
[11] Dvijotham, K., Stanforth, R., Gowal, S., Mann, T. A., and Kohli, P. A dual approach to scalable Phirty-Fourth Fourth Conference on Uncertainty in Artificial Intelligence, UAI 2018, Monterey, California, USA, August 6-10, 2018, pp. 550-559, 2018.
verification of deep networks. In Proceedings of the Thirty-
[12] Dwork, C., Hardt, M., Pitassi, T., Reingold, O., and Zemel, R. Faimess through awareness. In Proceedings of the 3rd innovations in theoretical computer science conference, pp. 214-226, 2012.
[13] Fazlyab, M., Robey, A., Hassani, H., Morari, M., and Pappas, G. J. Efficient and accurate estimation of lipschitz constants for deep neural networks. In Advances in Neural Information Processing Systems, pp. 14423-11434 2019.
[14] Fel, T., Vigouroux, D., Cadène, R., and Serre, T. How good is your explanation? algorithmic stability measures to assess the quality of explanations for deep neural networks. In Proceedings of the IEEE/CVF Winter Conference on Applications of Computer Vision, pp. 720-730, 2022.
[15] Gómez, F. L., Rolland, P., and Cevher, V. Lipschitz constant estimation of neural networks via sparse polynomial optimization. International Conference on Learning Representations, 2020.
[16] Gouk, H., Frank, E., Pfahringer, B., and Cree, M. Regularisation of neural networks by enforcing lipschitz continuity. Machine Learning, 110(2):393-416, 2021.

---

[17] Gowal, S., Dvijotham, K., Stanforth, R., Bunel, R., Qin, C., Uesato, J., Mann, T., and Kohli, P. On the effectiveness interval bound propagation for training verifiably robust models. arXiv preprini arXiv: 1810. 12715, 2018.
[18) He, K., Zhang, X., Ren, S., and Sun, J. Deep residual learning for image recognition. In The IEEE Conference on Computer Vision and Pattern Recognition (CVPR), pp. 770-778, 2016. doi: 10.11099C2..2006..99
[19] Hein, M. and Andriushchenko, M. Formal guarantees on the robustness of classifier against adversarial manipulation. In Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, 2017.
CA, USA, pp.
[20] Hickey, T., Ju, Q., and Van Emden, M. Interval arithmetic: From principles to implementation. Journal of the ACM (JACM), 48(5):1038-1066 2001.
[21] Huang, Y., Zhang, H., Shi, Y., Kolter, Z., and Anandkumar, A. Training certifiably robust neural networks with efficient local lipschitz bounds. In Thirty- Conference on Neural Information Processing Systems, 2021.
[22] Imbert, C. Support functions of clarke's generalized jacobian and of its plenary hull. Nonlinear Analysis: Theory, Methods and Applications,
2002.
[23] Jordan, M. and Dimakis, A. Provable lipschitz certification for generative models. In Interna- tional Conference Machine Learnin, pp. 5118 1-26. PMLR, 2021.
[24] Jordan, M. and Dimakis, A. G. Exactly computing the local lipschitz constant of relu networks. In Advances in Neural Information Processing Systems, 2020.
[25] Kang, J., He, J., Maciejewski, R., and Tong, H. Inform: Individual fairness on graph mining. In Proceedings of the 26th ACM SIGKDD International Conference on Knowledge Discovery & Data Mining, pp. 379-389, 2020.
[26] Katz, G., Barrett, C., Dill, D. L., Julian, K., and Kochenderfer, M. J. Reluplex: An efficient smt solver for verifying deep neural networks. In International Conference on Computer Aided Verification, pp. 97-117, 2017.
[27] Krizhevsky, A., Hinton, G., et al. Learning multiple layers of features from tiny images. Technical Report TR-2009, 2009.
[28] Laurel, J., Yang. R., Singh, G., and Misailovic, S. A dual number abstraction for static analysis of clarke jacobians. Proceedings of the ACM on Programming Languages, 1-POPL):1-30, 2022.
[29] Le, Y. and Yang, X. Tiny imagenet visual recognition challenge. CS 231N, 2015.
[30] LeCun, Y., Cortes, C., and Burges, C. Mnist handwritten digit database. ATT Labs [Online]. Available: http://yan.lecunn.cm httm////ccm.omm//////iiissst 2, 2010.
[31] Leino, K., Wang, Z., and Fredrikson, M. Globally-robust neural networks. In International Conference on Machine Learning, volume 139 of Proceedings of Machine Learning Research, pp. 6212-6222, 2021.
[32] Li, Q.. Haque, S., Anil, C., Lucas, J., Grosse, R. B., and Jacobsen, Preventing gradient attenuation lipschitz constrained convolutional networks. Advances in Neural Information Processing Systems, pp. 15364-15376, 2019.
[33] Liu, X., Han, X., Zhang, N., and Liu, Q. Certified monotonic neural networks. In Advances in Neural Information Processing Systems, 2020.
[34] Lyu, Z., Ko, C., Kong, Z., Wong, N., Lin, D., and Daniel, L. Fastened CROWN: tightened neural network robustness certificates. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, pp. 5037-5044, 2020.
12

---

[35] Mirman, M.. Gehr, T., and Vechev, M. T. Differentiable abstract interpretation for provably robust neural networks. In International Conference on Machine Learning, volume 80 of Proceedings of Machine Learning Research, pp. 3575-3583, 2018.
[36] Ryou, W., Chen, J., Balunovic, M., Singh, G., Dan, A., and Vechev, M. Scalable polyhedral verification of recurrent neural networks. In International Conference on Computer Aided Verification, pp. 225-248, 2021.
[37] Schaible, S. et al. Generalized monotone nonsmooth maps. Journal of Convex Analysis, 3: 195-206, 1996.
[38] Shi, Z.., Zhang, H., Chang, K.-W., Huang, M., and Hsich, C.-J. Robustness verification for transformers, In International Conference on Learning Representations, 2019.
[39] Shi, Z., Wang, Y., Zhang, H., J., and Hsich, C.-J. Fast certified robust training with short warmup. Advances in Neural Information Processing Systems, 34, 2021.
[40] Sill, Monotonic networks. Advances in neural information processing systems, 10, 1997.
[41] Singh, G., Gehr, T., Püschel, M., and Vechev, M. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages, 3(POPL):41, 2019.
[42] Singla, S. and Feizi, S. Skew orthogonal convolutions. In International Conference on Machine Learning, volume 139 of Proceedings of Machine Learning Research, pp. 9756-9766, 2021.
[43] Sivaraman, A., Farnadi, G., Millstein, T. D., and den Broeck, G. V. Counterexample-gune guided learning of monotonic neural networks. In Advances in Neural Information Processing Systems, 2020.
[44] Szegedy, C.,, Zaremba, W., Sutskever, I,, Bruna, J., Erhan, D., Goodfellow, I. J., and Fer- gus, R. Intriguing properties of neural networks. In International Conference on Learning Representations, 2014.
[45] Tsuzuku, Y., Sato, I., and Sugiyama, M. Lipschitz-margin training: Scalable certification of perturbation invariance for deep neural networks. In Advances in Neural Information Processing Systems, pp. 6542-6551, 2018
[46] Virmaux, A. and Scaman, K. Lipschitz regularity of deep neural networks: analysis and efficient estimation. In Advances in Neural Information Processing Systems, pp. 3839-3848, 2018.
[47] Wang, S., Pei, K., Whitehouse, J., Yang, J., and Jana, S. Efficient formal safety analysis of neural networks. In Advances in Neural Information Processing Systems, pp. 6369-6377 2018.
[48] Wang, S., Pei, K., Whitehouse, J., Yang. J., and Jana, S. Formal security analysis of neural networks using symbolic intervals. In 27th (USENIX) Security Symposium (f (/USENIX) Security 18), pp. 1599-1614, 2018
[49] Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, C.-J,, and Kolter, J. Z. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. Advances in Neural Information Processing Systems, 34:29909-29921, 2021.
[50] Wang, Y., Shi, Z., Gu, Q., and Hsieh, C.-J. On the convergence of certified robust training with interval bound propagation. International Conference on Learning Representations, 2021.
[51] Weng, T., Zhang, H., Chen, H., Song, Z., Hsieh, C., Daniel, L., Boning, D. S., and Dhillon, I. S. Towards fast computation of certified robustness for relu networks. In International Conference on Machine Learning, volume 80 of Proceedings of Machine Learning Research, pp- 5273-5282, 2018
[52] Wong, E. and Kolter, J. 7. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International Conference on Machine Learning, volume 80 of Proceedings of Machine Learning Research, pp. 5283-5292, 2018.
13

---

[53] Xu, K., Shi, Z., Zhang, H., Wang, Y., Chang, K., Huang, M., Kailkhura, B., Lin, X., and Hsieh, C. Automatic perturbation analysis for scalable certified robustness and beyond. In Advances in Neural Information Processing Systems, 2020.
[54] Xu, K., Zhang, H., Wang, S., Wang, Y., Jana, S., Lin, X., and Hsieh, C. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In International Conference Learning Representations, 2021.
[55] Zhang, B., Cai, T., Lu, Z.., He, D., and Wang, L. Towards certifying I-infinitt robustness using neural networks with l-inf-dist neurons. In International Conference on Machine Learning, volume 139 of Proceedings of Machine Learning Research, pp. 12368-12379, 2021.
[56] Zhang, B., Jiang, D., He, D., and Wang. L. Boosting the certified robustness of l-infinity distance nets. In International Conference on Learning Representations, 2021.
[57] Zhang, B., Jiang, D., He, D., and Wang, I.. Rethinking lipschitz neural networks for certified l-infinity robustness. Advances Neural Information Processing Systems, 35, 2022.
[58] Zhang, H., Weng, T., Chen, P., Hsich, C., and Daniel, L. Efficient neural network robustness certification with general activation functions. In Advances in Neural Information Processing Systems, pp. 4944-4953, 2018.
[59] Zhang, H., Zhang, P., and Hsieh, C. Recurjac: An efficient recursive algorithm for bounding jacobian matrix of neural networks and its applications. In The Thirty-Third AAAI Conference on Artificial Intellience, pp. 5757-5764, 2019.
doi: 10. 1609/aa0iia..... 03310113301133333
[60] Zhang, H., Chen, H., Xiao, C., Gowal, S., Stanforth, R., Li, B., Boning, D. S., and Hsieh, C. Towards stable and efficient training of verifiably robust neural networks. International Conference Learning Representations, 2020.
[61] Zhang, H., Wang, S., Xu, K., Li, L., Li, B., Jana, S., Hsieh, C.-J,, and Kolter, J. Z. General cutting planes for nound-propagation--oe neural network verification. Advances in Neural Information Processing Systems, 2022.
14

---

Checklist
1. For all authors...
(a) Do the main claims made in the abstract and introduction accurately reflect the paper's
contributions and scope? [Yes]
(b) Did you describe the limitations of your work? [Yes]
(c) Did you discuss any potential negative societal impacts of your work? [N/A] Our work will enable potential users to better verify and understand the properties of neural networks, for more reliable and trustworthy deployment in the future. We did not find any negative social impact.
(d) Have you read the ethics review guidelines and ensured that your paper conforms to them? [Yes]
2. If you are including theoretical results...
(a) Did you state the full set of assumptions of all theoretical results? [Yes]
(b) Did you include complete proofs of all theoretical results? [Yes]
3. If you ran experiments..
(a) Did you include the code, data, and instructions needed to reproduce the main experi- mental results (either in the supplemental material or URL)? [Yes]
(b) Did you specify all the training details (c.g.. data splits, hyperparameters, how they were chosen)? [Yes]
(c) Did you report error bars (e.g., with respect to the random seed after running exper- iments multiple times)? [N/A] There is no randomness our computation for local Lipschitz constants.
(d) Did you include the total amount of compute and the type of resources used (e.g., type of GPUs, internal cluster, or cloud provider)? [Yes]
4. If you are using existing assets (e.g., code, data, models) or curating/releasing new assets...
(a) your work uses existing assets, did you cite the creators? [Yes]
(b) Did you mention the license of the assets? [Yes]
(c) Did you include any new assets either in the supplemental material or as a URL? [Yes]
(d) Did you discuss whether and how consent was obtained from people whose data you'l 're using/curating? [Yes]
(c) Did you discuss whether the data you are using/curating contains personally identifiable information or offensive content? [Yes]
5. If you used crowdsourcing conducted research with human subjects...
(a) Did you include the full text of instructions given to participants and screenshots, applicable? [N/A]
(b) Did you describe any potential participant risks, with links Institutional Review Board (IRB) approvals, if applicable? [N/A]
(c) Did you include the estimated hourly wage paid to participants and the total amount spent on participant compensation? [N/A]
15


Reviews:
[{"review_id": "pL2Kf8e8nGK", "reviewer": "Reviewer_LzFR", "summary": "The paper presents a novel method to compute upper bounds to the local Lipschitz constant of a neural network, by using linear bound propagation to bound the norm of the Clarke Jacobian of the network. The authors demonstrate that the proposed approach computes tighter bounds than the state-of-the-art in reasonable time on synthetic networks, and on networks trained for popular image datasets. Finally, the method is tested on monotonicity analysis, as an example application.", "questions": "- It would be interesting to compare the presented branching strategy against existing strategies proposed in the context of network verification, such as input splitting or FSB from https://arxiv.org/abs/2104.06718, which was notably applied in beta-CROWN\n\n- Given that it relies on similar techniques, RecurJac should trivially support convolutional layers. Implementing this support would provide a fairer comparison.\n\n- It would be interesting to see whether the baselines yield any different results in Table 4, for the monotonicity analysis.", "limitations": "The authors adequately discuss the limitations of their work. However, it would be better for the reader to have them condensed in a section in the appendix.", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "The authors make a more careful use of linear bound propagation techniques in the context of estimating a network's local Lipschitz constant, resulting in tighter bounds than the state-of-the-art estimators in reasonable time. Furthermore, the algorithm supports branching to tighten the bounds, and a custom branching strategy is presented, which appears to work well in the considered experimental settings. While the approach is not entirely original, and it draws on existing techniques (such as RecurJac), it is clearly presented and effective. I believe it might be of interest to the community.\n\nFor what concerns the weaknesses, the experimental section is somewhat limited, as it mostly relies on small and synthetic networks. It would be interesting to test the algorithm on larger networks, and possibly on neural network verification, as for instance done by the RecurJac authors. At that point, I would be curious to see how Lipschitz-based algorithms compare with common incomplete verifiers (especially those based on optimized linear bounds such as alpha and beta-CROWN). Analogously, it would be interesting to see an extension of section 4.2 on l_2 norm (which bounding algorithms for Lipschitz constants routinely support).", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "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": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "YoT-QEX-10", "reviewer": "Reviewer_2723", "summary": "This paper extends existing Clarke Jacobian estimation from interval bounds to the linear relaxation. The authors further apply the branch-and-bound method to tighten the estimation when the time budget allows. The experiments show that the linear-relaxed Clarke Jacobian with branch-and-bound produces more precise results than selected benchmarks. The authors also use the monotonicity analysis as an application of Clarke Jacobian.", "questions": "1. My experience with (interval)-Clarke Jacobian is that it provides very loose result in the $\\ell_2$-case. The $\\ell_2$ matrix norm (largest singular value) computation is also very different from $\\ell_\\infty$-norm. As a result, section 4.2 would be very different in the $\\ell_2$-case. I do not know how much the improvement brought from linear bound propagation would be in the $\\ell_2$-case. If this work only applies to $\\ell_\\infty$ and $\\ell_1$ (linear constraint) perturbation space, please be upfront in the abstract or intro; otherwise, please provide some comparison with LipSDP in the $\\ell_2$-case.\n2. Optimality result: The optimality result of CROWN has been shown in [2]. The linear constraint propagation provided in this paper appears very similar to CROWN, except this work is for the backward Clarke Jacobian analysis. Why is Theorem 4 not a corollary of the theorem in [2], given Propositions 2 and 3?", "limitations": "No major concerns. One suggestion for paper writing: please use other graphical features than colors to distinguish different parts of the plot. This is not friendly for color-blind readers or black and white printers.", "rating": 4, "confidence": 4, "soundness": 2, "presentation": 2, "contribution": 2, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths:\nThis work provides tighter estimation of Clarke Jacobian norm estimation, which has practical benefits for the local Lipschitz constant evaluation. Local Lipschitz constant is an essential mathematical property of the neural network in an input region.\n\nWeaknesses:\n1. This work is incremental. Tightening neural-network certification from interval bounds to linear relaxation has been studied in a number of works, for example, [1] and [2]. The branch-and-bound method has also been used to compute the Lipschitz constant of neural networks [3]. This work brings little new insight or understanding to neural-network certification. The benefit is mostly practical from compiling known methods together, which is not surprising.\n2. Line 179 mentions that in this paper, the authors mainly consider $\\ell_\\infty$-norm *for simplicity*. I doubt whether this is *for simplicity* or linear relaxed Clarke Jacobian is only able to handle linearly constraint perturbation space in practice (see the Questions section below).\n3. The evaluation has doubts. The first part is related to 2. LipSDP is designed to compute Lipschitz constant with respect to $\\ell_2$ perturbations. Scaling the result of LipSDP for $\\ell_2$ perturbations seems an unfair comparison to LipSDP, unless the authors make it clear this work does not apply to $\\ell_2$ perturbations. The second part is for the monotonicity analysis. The authors provide some numbers from experiments, but there is no justification on how good the result is.\n\n[1]Zhang, H., Weng, T., Chen, P., Hsieh, C., and Daniel, L. Efficient neural network robustness certification with general activation functions. In Advances in Neural Information Processing Systems, pp. 4944–4953, 2018. URL https://proceedings.neurips.cc/paper/2018/hash/d04863f100d59b3eb688a11f95b0ae60-Abstract.html.\n\n[2]Lyu, Z., Ko, C., Kong, Z., Wong, N., Lin, D., and Daniel, L. Fastened CROWN: tightened neural network robustness certificates. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020, pp. 5037–5044, 2020. URL https://aaai.org/ojs/index.php/AAAI/article/view/5944.\n\n[3]Bhowmick, A., D’Souza, M., and Raghavan, G. S. Lipbab: computing exact lipschitz constant of relu networks. In International Conference on Artificial Neural Networks, pp. 151–162. 332 Springer, 2021.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "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": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "MQrmpkFizit", "reviewer": "Reviewer_jXRD", "summary": "This work presents a method to efficiently compute upper bounds for the Local Lipschitz constant of ReLU networks. In short, Interval Bound Propagation techniques are applied to the backward computational graph, which yields an upper bound on the norm of the\nClarke Jacobian of the network, which constitutes an upper bound for the Local Lipschitz constant. Careful consideration of the bounds for well-known activation functions provide tighter results over previous baselines. Such improvements are confirmed on experiments using MLPs and Convolutional networks trained on MNIST/CIFAR10/TinyImagenet.\n\n*** after rebuttal ***\nAuthors have addressed my main concerns. I am inclined to increase my score.", "questions": "1. Isn't RecurJac precisely an application of Interval Bound Propagation on the backward computational graph of the network (the Jacobian)? Could you expand and clarify the differences between your approach an RecurJac?\n2. Could you clarify which \"Chain rule\" are you using for composition of non-differentiable functions?\n3. Do you have new experimental results with confidence intervals, that you could add to the tables?", "limitations": "No negative societal impact. The main limitation is the cost of Branch-and-bound which the authors somehow address by providing an option to use the method without BaB.", "rating": 7, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "**Originality**: I think the main weakness is in this front, as to me the contribution is not clear. The authors claim that their contribution is to \"generalize existing bound propagation methods originally used for NN verification, to a higher order backward computational graph for bounding the Clarke Jacobian\". However, to me it appears that [B] precisely does that, with the caveat that their results are for differentiable activation functions, when the notion of Clarke Jacobian is just the normal Jacobian function. As such, I believe that this work rather adapts the technique in [B] to the setting of non-differentiable activation functions like ReLU, together with a more careful approach that provides tighter bounds in some cases, compared to the methods in [B]. This should be clarified by the authors and if it is the case, the claims should be toned down. In summary, I believe that applying Interval Bound Propagation techniques to the Jacobian (which is the backward computational graph) is already done in [B], although in a slightly different setting.\n\n**Quality and Clarity**: The paper is in general well-written and easy to follow, and the bibliography appears all of previous related work. The differences with most previous works are clearly explained, again with the exception of RecurJac [B], where I believe the authors should expand. Also in line 151 the authors claim \"Chain rule can be used to compute the Clarke Jacobian for the whole ReLU network\", however it is well known that the notion of \"Chain rule\" is more complicated when dealing with non-smooth compositions, I would like the authors to clarify which \"Chain rule\" are they talking about. See for example Theorem 4 in [A].\n\n**Significance**: I believe it is important to extend the method in [B] to the case of non-smooth activations, as activations like ReLU and LeakyReLU are commonly used in practice despite the fact that they do not have a \"normal\" gradient at all points. Moreover, **Theorem 4** in this work is a tightness result which implies that the relaxation presented in this work is the tightest possible, which is an important step in this line of research. However, related to my main criticism of the work, if indeed the idea of applying interval bound propagation to the backward computational graph is already present in [B], the method presented here would be more of a refinement of a previous method rather than a completely different approach, which is less significant.\n\nIn the experiments it is not clear why RecurJac is used despite it being tailored for differentiable activation functions, can the authors clarify if using RecurJac for non-smooth activation functions still provide a valid upper bound for the norm of the Jacobian? Another issue with the experiments is a lack of confidence intervals. Because the networks used are a result of a stochastic process (SGD) there might be differences due to randomness, and without confidence intervals it is hard to assess if the improvement is significant. For example the method LipBAB achieves a runtime of 2.92 for MLPs of width 32 and 4 layers, which is much faster than the method presented here, while providing a Lipschitz constant as good. However in other cases it is considerably slower and provides worse bounds. Adding confidence intervals could possibly let the authors conclude if their method is **consistently outperforming the baselines**.\n\nNevertheless,their method (without Branch-and-bound) appears to be consistently faster and more scalable than RecurJac. \n\n**References**\n[A] Support functions of Clarke's generalized jacobian and of its plenary hull. Cyril Imbert.\n[B] RecurJac: An Efficient Recursive Algorithm for Bounding Jacobian Matrix of Neural Networks and Its Applications, Huan Zhang, Pengchuan Zhang, Cho-Jui Hsieh, AAAI 2019", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "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": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}]

Author rebuttal:

Decision: Accept