SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
Authors: Hong-Ming Chiu
Hao Chen
Huan Zhang
Richard Y. Zhang
Venue: ICML 2025 spotlightposter (2025)
Keywords: neural network verification
convex optimization
semidefinite programming
Primary area: deep_learning->robustness

Abstract: Neural network verifiers based on linear bound propagation scale impressively to massive models but can be surprisingly loose when neuron coupling is crucial. Conversely, semidefinite programming (SDP) verifiers capture inter-neuron coupling naturally, but their cubic complexity restricts them to only small models. In this paper, we propose SDP-CROWN, a novel hybrid verification framework that combines the tightness of SDP relaxations with the scalability of bound-propagation verifiers. At the core of SDP-CROWN is a new linear bound---derived via SDP principles---that explicitly captures $\ell_{2}$-norm-based inter-neuron coupling while adding only one extra parameter per layer. This bound can be integrated seamlessly into any linear bound-propagation pipeline, preserving the inherent scalability of such methods yet significantly improving tightness. In theory, we prove that our inter-neuron bound can be up to a factor of $\sqrt{n}$ tighter than traditional per-neuron bounds. In practice, when incorporated into the state-of-the-art $\alpha$-CROWN verifier, we observe markedly improved verification performance on large models with up to 65 thousand neurons and 2.47 million parameters, achieving tightness that approaches that of costly SDP-based methods.

SDP-CROWN:
Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
Hong-Ming Chiu
Hao Chen
Huan Zhang'
Richard Y. Zhang'
Abstract
Upper bound verilied accuracy Verified accuracy
100%
Neural network verifiers based on linear bound propagation scale impressively massive mod- els but be surprisingly loose when neuron coupling is crucial. Conversely, semidefinite pro- gramming (SDP) verifiers capture inter-neuron coupling naturally, but their cubic complexity restricts them to only small models. In this paper, we propose SDP-CROWN, a novel hy- brid verification framework that combines the tightness of SDP relaxations with the scalabil- ity of bound- propagation verifiers. At the core of SDP-CROWN is new linear derived via SDP principles that explicitly captures 62- norm-based inter-neuron coupling while adding only one extra parameter per layer. This bound can be integrated seamlessly into any linear hound-propaggtionn pipeline, preserving the in- herent scalability of such methods yet signifi- cantly improving tightness. In theory, that our inter-neuron bound can be up to factor of /n tighter than traditional per-neuron bounds. In practice, when incorporated into the state-of- the-art a-CROWN verifier, we observe markedly improved verification performance large mod- els with up to 65 thousand neurons and 2.47 million parameters, achieving tightness that ap- proaches that of costly SDP-based methods.
80%
72
72.5%
72.5%
72.5%
72.5%
72.5%
60%
40%
47.5
20%
0%
2.5%
5.0%
6.0%
a-CROWN 8-CROWN
BICCOS
LipNaive work
Figure 1: Verification of the ConvLarge network on the CIFAR-10 dataset (six convolutional layers + three fully connected layers, =2.47M parameters and 65k neu- rons) under & adversaries. State-of-the-art bound prop- agation algorithms a-CROWN, 3-CROWN and BICCOS yield surprisingly loose relaxations under &g adversaries (verified accuracy 2.5%, 5.0% and 6.0%, respectively) at high cost (up to 289s per example). A naive Lipschitz base- line, which multiples per-layer & Lipschitz constants di- rectly ("LipNaive"), outperforms them (47.5% verified ac- curacy) with negligible runtime. In contrast, our proposed method achieves striking 63.5% verified accuracy while keeping runtime moderate (73s). See Section 6. for perimental details; note that the model is too large to be verified with traditional SDP methods.
prove
ification methods, linear bound propagation based ap- proaches (Zhang al., 2018; Wang et al., 2018; Wong & Kolter, 2018; Dvijotham et al., 2018; Singh et al., 2018; 2019; Xu et al., 2020) have emerged as the dominant ap- proach due to their effectiveness and scalability. The core idea is to construct linear functions that provide pointwise upper and lower bounds for each nonlinear activation func- tion and recursively propagate these bounds through the network. This method has proven particularly effective in certifying robustness against form perturbations, where individual input features are perturbed within fixed limits. Notably, many highly ranked verifiers in VNN- COMP verification competition rely on bound propagation due to its success in scaling to large networks (Brix et al., 2023; 2024).
1. Introduction
Neural network verification is critical for ensuring that models deployed in safety-critical applications adhere to robustness and safety requirements. Among various ver-
'Department of Electrical and Computer Engineering, Uni- versity of Illinois at Orbana-Champala to: Hong-Ming Chiu fannhhu2@illiniis.com Correspondence <haoc8 weleeeiiliiinccecc edu>, Huan Zhang <huan @ mman-zhang.com Richard Zhang <ryz@ eduu..
Hao Chen
Proceedings of the 1nnd International Conference Machine Learning, Vancouver, Canada. PMLR 267, 2025. Copyright 2025 by the author(s).

---

SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
Despite this success, bound propagation performs surpris- ingly poorly under f2-norm perturbations, as shown in Fig- ure 1. Unlike -nomm perturbations, which treat each neuron independently, f2-norm perturbations impose inter- neuron coupling. This coupling introduces dependencies between neurons that bound propagation, designed to han- dle features individually, cannot effectively capture. As a result, it often produces loose and overly conservative out- put bounds. The fz-norm setting is critical not only as benchmark for evaluating neuron coupling (Szegedy et al., 2014) but also for verifying real-world adversarial exam- ples, such as semantic perturbations, which are commonly modeled using fz-norm perturbations applied through gen- erative layers (Wong& & Kolter, 2021; Barrett et al., 2022).
1.1. Related work
To the best of our knowledge, this work is the first to ap- ply SDP relaxations to efficiently tighten the linear bound propagation under lz fo-mo perturbations.
SDP relaxation is the preferred approach for neural net- work verification against 42-norm perturbations. Due to its ability to capture second-order information, SDP-based methods provide tight verification under & adversaries (Chiu & Zhang, 2023). Several extensions have been pro- posed to further tighten the SDP relaxation by introduc- ing linear cuts (Batten et al., 2021) and nonconvex cuts (Ma & Sojoudi, 2020), and to accommodate general ac- tivation functions (Fazlyab et al., 2020). However, SDP relaxation does not scale to medium-to-large scale models. Even with state-of-the-art SDP solvers and hardware accel- eration (Dathathri et al., 2020; Chiu & Zhang. 2023), they remain computationally prohibitive for models containing more than 10 thousand neurons.
To overcome this limitation, semidefinite programming (SDP) methods (Raghunathan et al., 2018; Dathathri et al., 2020; Fazlyab et al., 2020; Anderson et al., 2021; New- ton & Papachristodoulou, 2021; Chiu & Zhang, 2023) have been developed to explicitly model inter-neuron dependen- cies. These methods optimize over a dense n X n coupling matrix, yielding significantly tighter bounds compared to bound propagation. However, their cubic (nz) time com- plexity restricts their application relatively small models, and renders them impractical for realistic neural networks.
In addition to SDP relaxation, bound propagation methods (Zhang et al., 2018; Singh et al., 2018; 2019; Wang et al., 2018; Dvijotham et al., 2018; Hashemi et al., 2021; Xu et al., 2020; 2021) for certifying l2 adversaries can be tight- ened using branch-and-bound procedure (Wang et al., 2021; De Palma et al., 2021; Ferrari et al., 2022; Shi et al., 2025) by splitting unstable ReI.U neurons into two subdo- mains, or by introducing nonlinear cutting planes (Zhang et al., 2022; Zhou et al., 2024) to capture the shape of &z adversaries. These methods have proven effective when the f--norm perturbation is small, as there are relatively fewer unstable neurons. However, they can become inef- fective for larger perturbations, and can completely fail, as demonstrated in Figure 1.
To bridge the gap between scalability and tightness, we introduce SDP-CROWN, a hybrid verification framework that combines the tightness of SDP with the efficiency of bound propagation. At the core of our framework is a lin- ear bound derived through SDP principles that efficiently incorporates --anor--based inter-neuron dependencies. A key feature of our bound is that it introduces only sin- gle new parameter per layer, in contrast to traditional SDP methods, which require n² parameters per layer of n neu- rons. As a result, our bound preserves the scalability of existing bound propagation methods. It can be seamlessly integrated into existing linear bound propagation verifiers such as CROWN and a-CROWN, hence significantly tight- ening it for & perturbations.
Alternativlly, & adversaries can be certified by lower bounding the robustness margin (2) using the network's global Lipschitz constant. To estimate this constant, (Fa- zlyab et al., 2019) solve the Lipschitz constant estimation problem using SDP relaxations; (Huang et al., 2021; Leino et al., 2021; Hu et al., 2023) incorporate Lipschitz upper bound during training; and (Li et al., 2019; Trockman & Kolter, 2021; Singla & Feizi, 2022; Meunier et al., 2022; Xu et al., 2022; Araujo et al., 2023) design neural network architectures that are provably I-Lipschitz. While these methods perform well on networks with a small global Lip- schitz constant, verifying robustness based solely on the Lipschitz constant can still be overly conservative, as illus- trated in Figure 1.
In theory, we prove that our proposed inter-neuron bound can be up to vn times tighter than the per-neuron bounds commonly used in scalable verifiers. In practice, when in- corporated into the a-CROWN verifier, we find that SDP- CROWN significantly improves verification performance, achieving bounds close to those of expensive bDseb methods while scaling to models containing over 65 thou- sand neurons and 2.47 million parameters. Our extensive experiments demonstrate that SDP-CROWN consistently enhances lg robustness certification rates across various architectures without compromising computational effi- ciency, making it well-suited for large-scale models where traditional SDP methods fail to scale.
1.2. Notations
We use the subseript x; denote indexing. We use 1 to denote a column of ones. We use O to denote elementwise multiplication. We use e to denote i-th standard basis vec-
2

---

SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
tor. We use X = 0 denote X being positive semidefinite. We use . denote the elementwise absolute value, and ||- llp to denote the vector Ep norm.
Similarly, the SDP relaxation of (2 p) is given by
n
Σ
U 2(1 ve).;; + Vi +
S p²:
2. Preliminaries
(4)
8
U/2 4,2 0, u 2 0,
U;
0
=
0.
2.1. Problem deseription
1/
VJ
Consider the task of classifying a data point x E I" as be- longing to the i-th of q classes using a N N-layer feedforward neural network/ f IR"h - R The network aims to gen- erate prediction vector that takes on its maximum value at the i-th element, i.e., ef f(x) > eÿ (x) for all incorrect labels j * We define the neural network fxx 2(N)
The SDP relaxation of (2) can be derived via (3) and (4). While SDP relaxations are typically tighter than most other convex relaxation methods, existing approaches solve the SDP relaxation via interior point method (Brown et al., 2022) or low-rank factorization method (Chiu & Zhang, 2023). Those methods incur approximately cubic time complexity and are not scalable to medium-scad models.
recursively as
(x) = (R), 2(k) = (+1))
(0))
(1)
for h E (1,2..... N) where RcLU(x)= = max rr. 0} and (Kk denote weight matrices. Without loss of generality,
3. Looseness of bound propagation for 2--norm perturbations
we ignore biases.
Linear bound propagation is one of the state-of-the-art ap- proaches for finding upper and lower bounds on (2). In this section, we explain why the approach can be unusu- ally loose when faced with an & perturbation set like X (2 p). which is the classic example when inter- neuron coupling strongly manifests. For simplicity, we fo- cus on finding lower bound for (2).
Given input å of truth class i, the problem of verifying the neural network f to have no adversarial example x as á mislabeled as the incorrect class # i can be posed as:
d = min cT fxx s.t. (1),
(2)
x
where c = 6; ey and X is a convex input set that models the adversarial perturbations. Popular choices include the elementwise bound
At a high level, all bound propagation methods solve (2) by defining a set of linear relaxations x + gxx + h that pointwise lower bound the original function ef f(x) across the input set N. as in
Boc (ē,
($, p) = {x| |x - 2.l S òe for all i}
and the le norm ball
L(X) (1), o ((x) o² x + for all E X
(2 p) {x| | $112 S p}:
where á E R is a center point, and أ E Rn" and p E IR are the radii. The resulting vector d E R2 is a robustness margin against misclassification. If d 2 0 over all of its elements, then there exists no adversarial example x within a distance of p that can be misclassified.
The linear relaxation corresponding to each hg L(X) can be minimized to yield a valid lower bound on the original problem
(2). This bound can be further tight- ened by optimizing over the linear relaxations themselves:
min oJ (²((x)) zEX
max min g² x + h. (g.A)E22 DE
2.2. Semidefinite programming (SDP) relaxation
In fact, one can show by a duality argument that the bound above is in fact exactly tight, i.e. the inequality holds with equality. Unfortunately, the set of linear relaxations (X)) is also intractable to work with.
Semidefinite relaxation is a convex relaxation method to compute lower bounds on (2). In this work, we focus our attention on the SDP relaxation used in Brown et al. (2022)
that utilizes the positive/negative splitting of the preactiva- tions u; Ti. straints V; ReLU((z) as
Instead, all bound propagation methods work by con- structing parameterized families of linear relaxations æ + g(a)TT h(a)) for 0 I < 1 that provably satisfy (g(a), h(a)) (X).. The tightest bound on (2) that could be obtained from the family of relaxations then reads
to rewrite the equality con-
x Uii U&u;- = 0, u, 200
0 2 0.
Adding [1 u, v.] I un v.] > 0 and relaxing Uj = uf and V, oi yields the SDP relaxation of the ReLU activation
min e- eT((x) 2 max min g(a)T x + M()) wEx
(5)
DEX
1 u,
U/
rz Use 2 2 0, 2 0,
M4
U
0
2 0.
(3)
Note that the inner minimization is a convex program that can be efficiently evaluated for many common choices of
0
V.
3

---

SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
X', such as the elementwise bound any lp norm ball. In practice, the parameter can be maximized via projected gradient ascent selected heuristically in Zhang et al. (2018).
4. Proposed method
Our core contribution in this paper is a high-quality family of linear relaxations I + g + h(g. A) for g E I= and
À 2 0 that provably satisty the following
The tightness of the heuristic bound in (5) is critically driven by the quality of the parameterized relaxations æ + g(a)"= + h(a). The core insight of bound propagation methods is that high-quality choice of g(a), h(a) satisfy- ing the following
f(x) of g + A(g, for all I B2 p).
Notice that our relaxation is constructed directly from the f--norm ball, i.c. (g. hig, A)) E ( which addresses the looseness of (6) we did not relax the εg-norm ball into -nomm box. Due to space constraints, we explain our construction only for the special case of f(x) = ReLU(z), while deferring the general case to the Appendix B.
(()) 2 g(a)a x h(a) for all x E (o, P)
can be constructed using the triangle relaxation of the ReLU activation, alongside forward-backwant pass through the neural network; we refer the reader to the Ap- pendix B for precise details. When the input set is indeed an -oom box X' = Bxo (tt P). Salman et al. (2019) showed that this choice of (g(a), h(a)) E L (#. p)) is essentially optimal per-neuron. This optimality provides a long-sought explanation for the tightness of bound prop- agation under an Lo adversary.
One particle aspect of our construction is to take linear re- laxation from bound propagation cf f(x) 2 g(a)"==h(a) for the box B ( p1) the offset h(g(a), X) 2 h(a) while ensuring that it re- mains valid for the ball p). In analogy with Salman et al. (2019), we prove in Section 5 that this choice of h(g(a), A) is essentially optimal when â = O, and can therefore yield at most a factor of v reduction in con- servatism for X (2 p). At the same time, our new method adds just one parameter À 0 per layer, so it can be seamlessly integrated into any bound propagation ver- ifier with negligible overhead. Integrating this technique into the a- a-CROWN verifier, we provide extensive compu- tational verification in Section 6 showing that our method significantly improves verification performance. The main theorem of our work is summarized below.
B2(4, p), and then tightening
However, when the input set X' is not an lxo box, bound propagation requires relaxing the input set X C (d, P) for the purposes of constructing g(a)), h(a). The resulting bound on (2) is valid by the following sequence of inequalities
min of f(()) #EX
max min g r + (x) SE
max (e B (R. ZEX
min g x + h
(6)
Theorem 4.1. Given e, à E R" and p 2 0. The following holds
max min g(a)" + h(a). ogogiaEX x
t ReL.U()) 2 g" x + (g.A) for all a E &B2(i, p)
The problem is that a loose relaxation (R, 2 X
for any x 0 and g E R² where
causes a comparably loose relaxation (B (.: p)) C
(x) in (6), hence introducing substantial conservatism to the overall bound.
- h(g.2) = 1 ( (Nl -| + 3 110g 2)13
1
The above explains the core mechanism for why bound propagation tends to be loose for an la adversary. The problem is that the tightest -nom box to fully contain a given norm ball satisfies the following
and
delg, A) = minn(: - - Xo Di + XZ;, 0}.
Let us explain how Theorem 4.1 can be used to lower bound the attack problem (2) in the special case of f(x) = ReLU(z) and X' = B2 p). First, we use the standard bound propagation procedure to compute linear relaxations x + g(a)"= x + h(a²) that provably satisfy (g(a), h(a)) e ( (0, p1)) for 0 S a < 1. Then, we replace h((a) with the new choice h(g(a), A) specified in Theorem 4.1 to ensure that (o(a), Mg(a), A)) E L(B (2;, p)) for X 2 0. Both a and À can then be optimized to provide a tighter re- laxation. We note that the attack problem can also be lower bounded by directly optimizing over g and À 2 0 (by treat- ing a as unconstrained variables), and Theorem 4.1 can be
x= B2 S (2, 1p).
However, there are attacks in the box x E {+p)" C (ā, 1p) with radii || - 2||2 = T that are a factor of vn larger than the radius p of the original ball. Ac- cordingly, relaxing the 22-norm ball into loo -nom box can effectively increase the attack radius by a factor of vn. Hence, the resulting bounds on (2) can also be factor of vn more conservative.
4

---

SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
extended to handle more general input set X' such an el- lipsoid. We provide more details for these extensions in the Appendix C.
for i I,..., n. For 2 x 2 matrix X, note that X > 0 holds if and only if det(X) 2 0 and diag (X) 2 0. Apply- ing this insight yields second-order cone programming (SOCP) problem
In the remainder of this section, we provide proof of The- orem 4.1.
(A(p 11+11) + 1²
max A,e,t,
4.1. Proof of Theorem 4.1
S.t. Ap4 2 (q - 9: - 5; Xt,))
(8)
Given any c.g E IR" the process of finding the tightest possible h such that ef (eI.U(x)) 2 gfxx + h holds within within (2 p) admits the following generic problem
Au4 2 (g: - 1, + Xd:)²
λ 8 2 0, 1 0, p=0. 0,
for i= == detailed derivation for the dual problem (8) to the Ap- pendix D. We are now ready to prove Theorem 4.1.
I....,,n. n. Due space constraints, we defer the
min c" ReLLU(x) mER"
- g"
s.t.
1 2 p². (7)
Applying the positive/negative splitting x = where u, and O 0 yields the following
Proof. Given any c, E RR.. Let ý = p² | ag =
min u
cuu g v)
Q; 9: Ad; and b, = 9s + Adz, Fixing any X 2 0 and optimizing in (8) yields
s.t. ||u1| 2(u - a + 10112 sp²² -1121
max {(a: 2;)2, (b; (.)
u 2 0,
v 0 u v O.
max X,8,120
-
Ap +
Though (7) is nonconvex due to the product of the two variables u and v, tight lower bound can be efficiently approximated via SDP relaxation described in (3) and (4). The SDP relaxation of (7) reads:
1
min {az, bi, 03²
max X20
Ap +
2
A
max h6g A) A20
d'u c-u- - 9" (u- - u)
min U.ERU.VRR"
where the first equality follows from min - -;)² = min 0}2 and min;,206;; - t,)² = min b, 032, and max (a,, 032, min(b, 0}2] = minfa,, by. 032 for any a, b, E R. Since h(g, A) is a lower bound on (7) for any A 2 O, have ef (eL 2 of x + h(g, for all
s.t.
(U + ++
2(u 2(u-o) -11112
u 1200 0,
V 220 0,
1 u 01
Ug
U3
2 0 for I,...,n. n.
0/
V.
B2 p) for any g R" X 0.
The SDP relaxation can be further simplified by applying Theorem 9.2 of (Vandenberghe & Andersen, 2015):
5. Tightness analysis
min U,
cuu ("(u-z)) v)
In this section, we provide theoretical analysis on the tightness of our SDP relaxation in the special case where f(x) = ReI.U(x)) and ê = O. We show that our SDP relax- ation (8) exactly tight this case and guarantees at most factor of v improvement over bound propagation when computing linear relaxation within (2 p). We begin by characterizing the linear relaxation from bound propaga- tion x + g(a)²xx + M(()) for the box x E B (0, p1) 2 (2 p) below.
s.t.
(U + 1)"1 1 -2(u 22uu-))u " S p²
11:1
u u20,
v 2 0,
ū+0 -+ū=10 ū=
ū; U4
0
0
20
0
U.]
0
for i = 1,....,,, Let X E R denote the dual variables of the first inequality constraints and 8, 9 E R² denote the dual variable for u 2 0, v 2 0 and ū + ē- = 1, respectively. The Lagrangian dual is given by:
Lemma 5.1. Given e E T and p > 0, the bound
1 g(a) 2 minfc, 0} + a C max(c,0). h(a) -pll min(g(a), 0311
(X(2²
| 1''1)
max.
A.
C - Ai;- - -8;
s.t.
2 0,
C - 9i Xi; 8i
A
satisfies
H4
9t + X²; t1]
2 0,
t. ReLU(x)) 2 g(a)"xx h(a) for all x E B Boc (1,
Di + X6: - 1
X
A 1 0, 1200 0, t2 0 1 0,
for any 0sa51.
5

---

SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
Linear relaxation from bound propagation
Linear relaxation from our method
[ar = Re]U(n) ReLU(2))
[(r
ReLU(m) ReLU((z))
-0.5
-0.5
-1.
-1.5
22
0.5
0
0.5
-0.5
422
-1
2/2
-1
T1
Figure 2: Comparing linear relaxations within fg-norm ball from our method and bound propagation. Consider task of finding a linear relaxation of f(x = - ReLU(x)) - ReLU(<x2) on (2, 1). (I.fft.) Bound propagation finds the tightest possible linear relaxation on Bx (0, 1), however, such relaxation is not the tightest on (2 1). (Right.) Our
method finds the tightest possible linear relaxation on (0, 1), which is tighter than bound propagation by a factor of /2.
Proof. Notice that a,x; I (e,UU(;;) S 1 for any
propagation when ă = 0, which we provide simple illus- tration in Figure 2.
0 I < 1. Therefore, we have g(a) minffe, 0} +
@ [e and h((a) = Ei= 2 min(e; 0} E min( = pll min (()
Finally, we show that our SDP relaxation (8) is exactly tight in the following Theorem, i.c. both (8) and (7) attain the same optimal value. Therefore, the choice of h(g(a), X) optimal.
In the following Theorem, we show that our method yields Mg((), A) -pll min(g(a), 0HI/2 when À 2 is chosen optimally. On the other hand, the linear relaxation from bound propagation yields h(a) -ll mi))g(a), 0}Ilı I h(g(a), A) in Lemma 5.1, which is looser than our method by at most factor of Vn.
Theorem 5.3. Given c E R and p > 0. The following holds
-pll mil(minnc- 9.9, 9,1l min c ReLU(x)) 9
| 25P
Theorem 5.2. Given T and p > O. The following holds
for any g R
ReL.UU()) 2 nd - mi 9, 0}112
Proof. Applying the positive/negative splitting x = u where u, U. 2 and u O v = 0 yields
for all x E P), for any E R
Σ (G - (G-g:)u + g.vs s.t. MQ
min 1,020
Σ + =
Proof. Setting f = 0 in h(g. X) and optimizing over X 0 yields
For each i, we substitute a variable y; according to the fol- lowing three cases. Case 1: c; 9: S min(g,,0 0}, we have ut 2 and of = 0; therefore we set y/i w;- Case 2: g. S min : gi, 0}, we have u, and of 2 0: there- fore set y/1 us Case 3: 0 S min It. 9: we have " of = 0; therefore we simply let > 0. Substituting each yi yields
App + min {c- 9.9. 0
max X
2
pll min {c- 9, .1, 0} 1
where the equality follows from 2vab min az bb/o for any b 2 0.
We obtain (((()), X) = - min(g(a), 12 by substitut- ing g = (a) Theorem 5.2. Notice that min (g(a),0) 0] min(c g(a), (a), from Lemma 5.1. Theorem 5.2
min Σ y minfc; (c: - 9:. 0r.9r.0) 0} s.t. l1 S p.
guarantees at most factor of v improvement over bound
which attains optimal value pll minfc 9. 9.9, 0l.
6

---

SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
Table I: Verified accuracy under 42-norm perturbations. We report the verified accuracy (%) for 200 images. For each method, we also report the average verification time (in seconds or hours), except for LipNaive and LipSDP, where we report the total time for computing the Lipschitz constant. The upper bound on verified accuracy is estimated using projected gradient descent. A dash "_" indicates the model could not be evaluated due to excessive computational time.
Upper Bound
SDP-CROWN (Ours)
GCP-CROWN
BICCOS
R-CROWN
a-CROWN
LipNaive
LipSPP
I.PAIl
BM-Fall
(split=2)
(no split)
MNIST Model'
MLP
54%
32.5% (2.5s)
41% (173s)
38% (198s)
36% (302s)
1.5% (1.26)
29% (0.02s)
29.5% (19%)
30.5% (62s)
9% (75s)
53% (0.36)
Con-Small
84.5%
81.5% (12s)
19.5% (2A8k)
17% (265k)
16% (257k)
0% (17s)
77.5% (0.1
78% (875%)
78.5% (0.99)
10% (0.61)
Conv
84%
79.5% (88s)
0% (309s)
0% (3046)
0% (307s)
0% (666)
77% (1s)
CIFAR-10 Model!
CNN-A
55.5%
49% (12s)
20% (210s)
20% (2246)
20% (201s)
7.5% (3.86)
39% (0.2s)
39% (1.7h)
CNN-B
59.5%
49.5% (16s)
3% (290s)
3% (302s)
3% (1936)
0% (8.75)
33% (0.36)
CNN-C
47%
42.5% (10s)
35.5% (964)
36% (101s)
35.5% (633s
24.5% (5.86)
36.5% (0.2s)
37% (0.5h)
38.55 (1h)
24.5% (0.3h)
ConvSmall
52.5%
43.5% (9s)
18% (225s)
18% (220s)
17.5% (146s)
6% (4.4s)
33% (0.2s)
33.5% (1.2h)
ConvDeop
50.5%
46% (25s)
31% (1386)
31.5% (135%)
30.5% (1335)
22.5% (9.2s)
39.5% (0.36)
39.5% (1 91)
ConeLarge
72.5%
63.5% (736)
6% (286s)
6% (2826)
5% (2894)
2.5% (47s)
47.5% (1.2x)
1 'The Ey-norm perturbation is set to be
0.3 for both ConvSmaal and ConvLarge. |The Ey-norm perturbation is set to be 8/255 for ConvLarge, and = 24/255 /255 for all the other models.
1.0 for MLP. and
For the general case with å * 0 and network f(x) de- fined in (I), the improvement of our method cannot be ana- lyzed analytically; instead, we present empirical validation in Section 6.3 to show that our method can be tighter than bound propagation in general settings.
LipNaive, a verifier estimates the Lip- schitz upper bound using the Lipschitz constant of each layer (as in Section 3 of Gouk et al. (2021)); and LipSDP (Fazlyab et al., 2019), a verifier estimates the Lipschitz up- per bound based on solving SDP relaxations of the Lips- chitz constant estimation problem. Specifically, LipNaive lower bounds c. f(r) within Bz p) through c² f(x) 2 of f(i) p. |ce ( |12 (11221112-- (/|2....([(((())) [|2 where W|ll denotes the spectral l2- no-mo of a matrix W.
Lipschitz constant:
6. Experiments
||W(())
In this section, we compare the practical performance of our proposed method against several state-of-the-art neural network verifiers for certifying l adversaries. The source code of our proposed method is available at https:: http::://githbb.../ com. com/Hong Hong-oooog-oo Mliogg-iing///oo/o / SDP-CROWN.
Finally, we compare SDP-CROWN against the following verifiers based on directly solving convex relaxations of the verification problem (2): LP-All (Salman et al., 2019), a verifier solves LP relaxation of (2) that uses the tightest possible preactivation bounds found by recursively solving LP problems for each preactivation; and BM-Full (Chiu & Zhang, 2023), a verifier solves an SDP relaxation of (2) that uses the same preactivation bounds in LP-AIl. For LP-All and BM-Full, we use the normr as the input constraint, as in x E By p). The complexity of BM-Ful and LP-All is cubic with respect to the number of preactivations, and therefore they are not scalable to most of the models used in our experiment.
Methods. SDP-CROWN denotes our proposed method. The implementation details for SDP-CROWN can be found in Appendix B. We compare SDP-CROW against the fol- lowing verifiers based on bound propagation: a-CROWN (Xu et al., 2021), a bound propagation verifier with gradient-optimized bound propagation; 3-CROWN (Wang et al., 2021), a verifier based on a-CROWN that can additionally handle split constraints for ReLU neurons; GCP-CROWN (Zhang et al., 2022) and BICCOS (Zhou et al., 2024), verifiers based on 3-CROWN that can ad- ditionally handle general cutting plane constraints. Since GCP-CROWN and BICCOS use mixed-integer program- ming (MIP) solvers to find cutting planes, we add the fz- norm constraint into the MIP formulation of (2), so that all cutting planes generated from the MIP will consider the 22-nrmm constraint rather than the enclosing -orm con- straint. We defer the detailed hyperparameter settings for bound propagation methods to the Appendix A.
Setups. All the experiments are run on a machine with a single Tesla V100-SXM2 GPU (32GB GPU memory) and dual Intel Xeon Gold 6138 CPUs.
Models. All the model architectures used in our experi- ment are taken from Wang et al. (2021) and Leino et al. (2021). To ensure non-vacuous fy-norm robustness and make meaningful comparisons across different verification methods, we retrain all models to have small global Lip- schitz upper bound while keeping their model architecture unchanged. We defer the detailed model architecture and the training procedure to the Appendix A.
We also compare SDP-CROWN against the following ver- ifiers based on estimating an upper bound on the global
7

---

SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
MLP (MNIST)
ConvSmall (CIFAR-10)
ConvLarge ( (CIFAR-10)
0.10
0.38
0.66
1.44
0.02
0.14
0.24
0.740.01
1.40
2
3-
2-
0
1
-2
0
-2
-1-
Upper Bound
CRO-CROWN
-
Upper Bound SDP-CROWN
-2
Upper Bound
4
U-CROWN
-3
SDP-CROWN
LipNaive
-8
C-CROWN
a-CROWN
-4
LP-AIl
LipNaive
LipNaive
-5
0.5 Ey-norm perturbation
1.5
0.5
1.5
0.05
0.1
0.15
0.2 0.25 0.3
fy-norm perturbation
e--norm perturbation
Figure 3: Lower bounds on the robustness margin under f--norm perturbations. We compare the lower bounds on (2) computed from SDP-CROWN, a-CROWN, LipNaive and LP-All. The lower bounds are averages over 90 instances of (2). The upper bound on (2) is estimated projected gradient descent (PGD). The numbers in the figure indicate the fz-norm perturbation level at which each lower bound crosses zero Note that robustness verification is only meaningful in the interval where the PGD upper bound remains positive. (I.eft.) Small-scale model MLP (MNIST). (Middle.) Medium- scale model ConySmall (CIFAR-1O). (Right.) Large-scale model ConvLarge (CIFAR-10).
6.1. Robustness verification for neural networks
vative, even for networks trained to have a small Lipschitz constant. For LipSDP, networks are divided into subnet- works when evaluating the Lipschitz constant: split=1 in- dicates single-layer subnetworks, split=2 denotes two-layer subnetworks, and no split means the full network is evalu- ated directly. We ignore reporting split=1 for LipSDP as it only marginally improves over LipNaive.
We compare the verified accuracy of SDP-CROWS against -tate-of-the-art verifiers on models trained on the MNIST and CIFAR-10 datasets. In each case, we fix the fz-norm perturbation P and compute verified accuracy using the first 200 images in the test set. Here, the verified accuracy de- notes the percentage of inputs that are both correctly clas- sified and robust. For comparison, we also compute the upper bound on verified accuracy using projected gradient descent (PGD) attacks (Madry et al., 2018).
Finally, LP-All is not scalable to large models and is also noticeably weaker than us on certified accuracy.
6.2. Tightness of lower bounds and verified accuracy
Table I shows the verified accuracy and the average compu- tation time for SDP-CROWN, CCO-N, BICCOS, B- CROWN, a- a-CROWN, LipNaive, LipSDP, LP-All and BM- Full. While BM-Full achieves the best verified accuracy in the first case, it unfortunately becomes computationally prohibitive in all remaining cases its complexity scales cubically with respect to the number of preactivations. In all the remaining cases, SDP-CROWN achieves verified accuracy close to the PGD upper bound while the bound propagation method a-CROWN exhibits limited certifica- tion performance. Other bound propagation methods B- CROWN, GCP-CROWN and BICCOS can greatly improve over a-CROWN, but the gap is still large compared to SDP. CROWN, LipNaive and LipSDP.
As the neural network verification problem (2) is NP-hard, all methods based on finding a lower bound on (2) via any sort of convex relaxations must become loose for suffi- ciently large la perturbations. However, robustness veri- fication is only necessary in the interval where the upper bound of (2) is positive, which can be efficiently estimated via PGD. Therefore, it is crucial for the lower bound to be tight within this region.
In this experiment, we examine the gap between the lower bound computed from SDP-CROWN and the upper bound computed from PGD across a wide range of &g pertur- bations. To ensure an accurate evaluation, we compute the average lower bounds over 90 instances of (2), which are generated via 9 incorrect classes for the first 10 cor- rectly classified test images. We compare our average lower bound to a a-CROWN, LipNaive and LP-AIl, which
Notably, SDP-CROWN is consistently tighter than Lip- Naive and LipSDP, suggesting that verifying robustness solely through the Lipschitz constant can be overly conser-
8

---

SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
Specifically, the average offset of SDP-CROWN is taken h(0) (g(a())), ((h) in (14) for k ,...., N, as in over
Offsets h(g(a), A) from EDP-CROWN
Offsets lt(a) from cRCRN
N E h ()) )()), and the average offset of a- CROWN is taken over h (a)(1) in (12)for k: = 1,..., NN, N E (a))). To ensure an accurate evalu-
as in 1 ation, we compute the average offsets over 90 instances of (2), which are generated via 9 incorrect classes for the first 10 correctly classified test images. Figure 4 re- ports the average offsets with respect to three models of different scales: a small-scale model MLP (MNIST); a medium-scab model ConySmall (0),A--1); and large- scale model ConvLarge (CIFAR-10).
Model
MLP (MNIST)
CouvSmall (CIFAR-10)
ConyLarge (CIFAR-10) 10)
0.1
0.15
0.2
Eg-norm perturbation
Figure 4: Linear relaxation offsets under 22-morm per- turbations. We compare the offset h(a) from a-CROWN to the offset h(g(a), A) from SDP-CROWN. The offsets are averages over 90 instances of (2). (Red line.) Small- scale model MIP (MNIST). (Green line.) Medium-scale model ConvSmall (CIFAR-10). (Blue line.) Large-scale model ConvLarge (CIFAR-10).
As shown in Figure 4, SDP-CROWN consistently yields a tighter offset compared to a-CROWN under general set- tings, which demonstrates its effectiveness in tightening bound propagation and improves certification quality. No- tably, a-CROWN exhibits significant drop in h(a) for larger networks such as ConvLarge (CIFAR-10) and Con- vSmall (CIFAR- 10) as the l perturbation increases. In contrast, SDP-CROWN does not experience rapid reduc- tion in (((a), A), maintaining significantly larger offsets across all models and perturbation sizes.
are verifiers also based on solving convex relaxations of (2). Figure 3 reports the average lower bounds and the average PGD upper bound with respect to three models of different scales: a small-scale model MLP (MNIST); a medium-scale model ConvSmall (CIFAR-10); and a large- scale model ConvLarge (CIFAR-10).
7. Conclusion
In this work, we present SDP-CROWN, novel frame- work that significantly tightens bound propagation for neu- ral network verification under en-norm perturbations. SDP- CROWN leverages semidefinite programming relaxations to improve the tightness of bound propagation while re- taining the efficiency of bound propagation methods. The- oretically, we prove that SDP-CROWN can be up /n tighter than bound propagation for nee-neuron network under zero-centered fg-norm perturbations. Practically, our extensive experiments demonstrate that SDP-CROWN consistently outperforms state-of-the-art verifiers across a range of models under f2-norm perturbations. including models with over million parameters and 65,000 neurons, where traditional LP and SDP methods are computation- ally infeasible, and bound propagation methods yield no- tably loose relaxations. Our results establish SDP-CROWN as both theoretical and practical advancement in scalable neural network verification under f--nrrm perturbations.
As shown in Figure 3, our proposed SDP-CROWN con- sistently outperforms a-CROWN, LipNaive and LP-AIl, and significantly narrows the gap between the PGD upper bound. Notice that a-CROWN produces extremely loose lower bounds in almost all cases, especially for large net- works such as LonyLarge (CIFAR-10), where its lower bound drops rapidly. LP-All marginally improves over a-CROWN. We note that LP-AIl is excluded in ConyS- mall (CIFAR-10) and ConvLarge (CIFAR-10) due to its high computational cost. LipNaive provides tighter lower bounds than a- a-CROWN and LP-All as all three models are trained to have small global Lipschitz upper bounds, but is consistently looser than SDP-CROWN.
6.3. Tightening bound propagation
In Section 5, we prove that when f(x) = RcLU(x) and the center of the l2 norm perturbation zero, the off- set set h(g(a), X) computed from SDP-CROWN is guaranteed to be least factor of /n tighter than the offset h(a) from bound propagation methods. However, the amount of improvement cannot be analyzed analytically under general settings. To empirically demonstrate how much improvement SDP-CROWN can achieve, in this experi- ment, we compute the average offset h(g(a), X) from SDP- CROWN, and the average offset h(a) from a-CROWN.
Acknowledgments
Financial support for this work was provided by NSF CAREER Award ECCS-2047462, IIS-2331967, and ONR Award N00014-24-1-2671. Huan Zhang is supported in part by the A12050 program at Schmidt Sciences (A12050 Early Career Fellowship).

---

SDP-CROWN:
Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
Impact Statement
De Palma, A., Behl, H. S., Bunel, R., Torr, P., and Kumar, M. P. Scaling the convex barrier with active In Pro- ceedings of the ICLR 2021 Conference. Open Review, 2021.
The work presented in this paper aims to advance neural network verification in machine learning. There are many potential societal consequences of our work, none of which feel must be specifically highlighted here.
Dvijotham, K., Stanforth, R., Gowal, S., Mann, T. A., and Kohli, P. A dual approach to scalable verification of deep networks. In UAI, volume 1, pp. 2, 2018.
References
Anderson, B. G., Ma, Z., Li, J., and Sojoudi, S. Partition- based convex relaxations for certifying the robustness of relu neural networks. arXiv preprint arXiv:2101.09306, 2021.
Fazlyab, M., Robey, A., Hassani, H., Morari, M., and Pap- pas, G. Efficient and accurate estimation of lipschitz constants for deep neural networks. Advances in neural information processing systems, 32, 2019.
Fazlyab, M., Morari, M., and Pappas, G. J. Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming. IEEE Transactions on Automatic Control, 67(1):1-15, 2020.
Araujo, A., Havens, A. J., Delattre, B., Allauzen, A., and Hu, B. A unified algebraic perspective on lipschitz neu- ral networks. In ICLR, 2023.
Barrett, B., Camuto, A., Willetts, M., and Rainforth, T. Certifiably robust variational autoencoders. In Interna- tional Conference on Artificial Intelligence and Statis- tics, pp. 3663-3683. PMLR, 2022.
Ferrari, C.,, Mueller, M. N., Jovanović, N., and Vechev, M. Complete verification via multi-neuron relaxation guided branch-and-boune In International Conference on Leurning Representations, 2022.
Batten, B., Kouvaros, P., Lomuscio, A., and Zheng, Y. Efficient neural network verification via layer-based semidefinite relaxations and linear cuts. In IJCAI, pp. 2184-2190, 2021.
Gouk, H., Frank, E., Pfahringer, B., and Cree, M. J. Regu- larisation of neural networks by enforcing lipschitz con- tinuity. Machine Learning, 110:393 416, 2021.
Brix. C., Müller, M. N., Bak, S., Johnson, T. T., and Liu, C. First three years of the international verification of neural networks competition (vnn-comp). International Journal on Software Tools for Technology Transfer, 25 (3):329-339, 2023.
Gowal, S., Dvijotham, K. D., Stanforth, R., Bunel, R., Qin, C., Uesato, J., Arandjelovic, R., Mann, T., and Kohli, P. Scalable verified training for provably robust image classification. In Proceedings of the IEEE/CVF Interna- tional Conference on Computer Vision, pp. 4842-488 4851, 2019.
Brix, C., Bak, S., Johnson, T. T., and Wu, H. The fifth international verification of neural networks competition (vnn-comp 2024): Summary and results. arXiv preprint arXiv:2412. 19985, 2024.
Hashemi, V. Kouvaros, P., and Lomuseio, A. Osip: Tightened bound propagation for the verification of relu neural networks. In International Conference Soft- ware Engineering and Formal Methods, pp. 463-480. Springer, 2021.
Brown, R. A., Schmerling, E., Azizan, N., and Pavone, M. A unified view of sasebased neural network verification through completely positive programming. In Interna- tional conference on artificial intelligence and statistics, pp. 3334-9355 PMLR, 2022.
Hu, K. Zou, A., Wang, Z., Leino, K., and Fredrikson, M. Unlocking deterministic robustness certification on ima- genet. Advances in Neural Information Processing Sys- tems, 36:42993 430013--3-11..11 2023.
Chiu, H.-M. and Zhang, R. Y. Tight certification of adver- sarially trained neural networks via nonconvex low-rank semidefinite relaxations. In International Conference Machine Learning, pp. 5631-5660. PMLR, 2023.
Huang. Y., Zhang, H., Shi, Y., Kolter, Z., and Anandku- mar, A. Training certifiably robust neural networks with efficient local lipschitz bounds. Advances in Neural In- formation Processing Systems, 34:22745-2223 2021.
Dathathri, S., Dvijotham, K., Kurakin, A., Raghunathan, A., Uesato, J., Bunel, R., Shankar, S., Steinhardt, J., Goodfellow, I., Liang, P., et al. Enabling certification of verification-agnostii networks via memory- semidefinite programming. In Advances in Neural In- formation Processing Systems, 2020.
Leino, K., Wang, Z., and Fredrikson, M. Globally-robust neural networks. In International Conference on Ma- chine Learning (ICML), 2021.
Li, Q. Haque, S., Anil, C., Lucas, J., Grosse, R. B., and Ja- cobsen, J.-H. Preventing gradient attenuation in lipschitz
10

---

SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
constrained convolutional networks. Advances in neural information processing systems, 32, 2019.
Vandenberghe, L. and Andersen, M. S. Chordal graphs and semidefinite optimization. Foundations and Trends in Optimization, 1(4):241-433, 2015.
Ma, Z. and Sojoudi, S. Strengthened sdp verification of neural network robustness via non-convex cuts. arXiv preprint ar arXiv:2010.08603; pp. 715-727,
Wang, S., Pei, K. Whitehouse, J., Yang. J., and Jana, S. Efficient formal safety analysis of neural networks. Advances in neural information processing systems, 31, 2018.
Madry, A., Makelov, A., Schmidt, L., Tsipras, D., and Vladu, A. Towards deep learning models resistant to ad- versarial attacks. In International Conference on Learn- ing Representations, 2018.
Wang. S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, C.-J., and Kolter, J. Z. Beta-crown: Efficient bound propaga- tion with per-neuron split constraints for neural network robustness verification. Advances in Neural Information Processing Systems, (-29999-2992)) 2021.
Meunier, L.., Delattre, B. J., Araujo, A., and Allauzen, A. A dynamical system perspective for lipschitz neural net- works. In International Conference on Machine Learn- ing, pp. 1 15484-15500. PMLR, 2022.
Wong. E. and Kolter, Z. Learning perturbation sets for robust machine learning. In International Conference on Learning Representations, 2021.
Newton, M. and Papachristodoulluu A. Exploiting sparsity for neural network verification. In Learning for dynam- ics and control, pp. 715-727. PMLR, 2021.
Wong, E. and Kolter, Z. Provable defenses against adver- sarial examples via the convex outer adversarial poly- tope. In International Conference on Machine Learning, 2018.
Raghunathan, A., Steinhardt, J., and Liang, P. S. Semidef- inite relaxations for certifying robustness to adversarial examples. Advances in Neural Information Processing Systems, 31, 2018.
pp.
Xu, K., Shi, Z., Zhang, H.,, Wang. Y., Chang, K.-W., Huang, M.. Kailkhura, B., Lin, X., and Hsieh, C.-J. Au- tomatic perturbation analysis for scalable certified ro- bustness and beyond. Advances in Neural Information Processing Systems, 13:1129-1144 2020.
Salman, H., Yang, G., Zhang, H., Hsieh, C.-J, and Zhang, P. convex relaxation barrier to tight robustness verifi- cation of neural networks. Advances in Neural Informa- tion Processing Systems, 32, 2019.
Xu, K., Zhang, H., Wang. S., Wang, Y., Jana, S., Lin, X., and Hsich, C.-J. Fast and complete: Enabling complete neural network verification with rapid and massively par- allel incomplete verifiers. In International Conference on Learning Representation (ICLR), 2021.
Shi, Z., Jin, Q., Kolter, Z., Jana, S., Hsich, C.-J., and Zhang, H. Neural network verification with branch- aarhch--n--eee and-bound for general nonlinearities. In International Conference on Tools and Algorithms for the Construction and Anal- ysis of Systems, 2025.
Singh, G. Gehr, T., Mirman, M., Püschel, M., and Vechev, M. Fast and effective robustness certification. In Ad- vances in Neural Information Processing Systems, pp. 10802-10813. 2018
Xu, X., Li, L., and Li, B. Lot: Layer-wise orthogonal training improving 12 certified robustness. Advances in Neural Information Processing Systems, 35:18904- 18915, 2022.
Singh, G., Gehr, T., Püschel. M., and Vechev, M. An ab- stract domain for certifying neural networks. Proceed- ings of the ACM on Programming Languages, 3(POPL): 2019.
Zhang, H., Weng. T.-W., Chen, P.-.,, Hsich, C.-J,, and Daniel, L. Efficient neural network robustness certifi- cation with general activation functions. Advances in neural information processing systems, 31, 2018.
Singla, S. and Feizi, S. Improved deterministic 12 robust- ness on 10 and c00. In International Confer- ence on Learning Representations (ICLR), 2022.
Zhang, H., Wang. S., Xu, K., Li. L., Li, B., Jana, S., Hsieh, C.J., and Kolter, J. Z. General cutting planes for bound-proe pronadd-oppgttion-bbeee tion. Advances in Neural Information Processing Sys- tems, 2022.
neural network verifica-
Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., and Fergus, R. Intriguing proper- ties of neural networks. In International Conference on Learning Representations, 2014.
Zhou, D.,. Brix, C., Hanasusanto, G. A., and Zhang, H. Scalable neural network verification with branch-and- bound inferred cutting planes. In The Tiihth An- nual Conference on Neural Information Processing Sys- tems, 2024.
Trockman, A. and Kolter, J. Z. Orthogonalizing convolu- tional layers with the cayley transform. In International Conference on Learning Representations, 2021.

---

SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
A. Experimental Setup
Hlperparameter settings. In our method SDP-CROWN, the variables a and À are solved by the Adam optimizer with 300 iterations. The learning rate 0.5 and 0.05 for and X, respectively, and is decayed with a factor of 0.98 per iteration. For a-CROWN, the variable is solved by the Adam optimizer for 300 iterations, with the learning rate 0.5 and the decay factor 0.98. For 3-CROWN, GCP-CROWN, and BICCOS, the timeout threshold for branch and bound is set to 300 seconds.
Model architecture.
All the model architectures are taken from Wang al. (2021) and Leino et al. (2021).
Table 2: Model architectures used in experiments.
Model name
Model structure
Parameters
Neurons
Accuracy
MLP (MNIST)
Linear(784, 100) Linear(100, 100) Linear(100, 10)
89,610
994
79%
ConvSmall (MNIST)
Conv(1, 16, 4, 2, 1) ConCooC,,.. 32, 4, 2, 1) Lin- ear(1568, 100) Linear(100, 10)
166406
5598
87.5%
ConvLarge (MNIST)
Conv(1, 32, 3, 1, 1) Conv(32, 32, 4, 2, 1)
1976162
48858
89.5%
Conv(32, 64, 3, 1, 1) Conv(64, 64, 4, 2, 1) Linear(3136, 512) Linear(512, 512) L5near(512, 10)
CNN-A (CIFAR-10)
Conv(3, 16, 4, 2, 1) Conv(11, 32, 4, 2, 1) Lin- car(2048, 100) Linear(100, 10)
214918
9326
62%
CNN-B (CIFAR-10)
Conv(3, 32, 5, 2, 0) Conv(32, 128, 2, 1) Lin- car(8192, 250) Linear(250, 10)
21 1118856
15876
66%
CNN-C (CIFAR-10)
Conv(3, 8, 4, 0) Conv(8, 16, 4, 2, Lin- ear(576, 128) Linear(128,, 64) Linear(64, 10)
85218
5650
51%
ConvSmall (CIFAR-10)
Conv(3, 16, 4, 2, 0) Conv(16, 32, 4, 2, 0) Lin- ear(1 152, 100) Linear( 10)
125318
7934
60.5%
ConvDeep (CIFAR-10)
C3nv(3, 8, 4. 2, !) Conv(8, 8, 3, 1, I) Conv(8, 8, 3, 1, 1) Conv(8, 8, 4, 2, 1) Li1ear(512,, 100)
54902
9838
53%
Linear(100 10)
ConvLarge (CIFAR-10)
Conv(3, 32, 3, 1, 1) Conv(32, 32, 4, 2, 1) C3nv(32, 64, 3, 1, 1) Conv(64, 64, 4, 2, 1)
2466858
65546
74%
Linear(4096, 512) Linear(512, 512) Linear(512.
10)
Note: Conv(3, 16, 4, 2, 0) stands for convolutional layer with 3 input channels, 16 output channels, a x 4 kernel, stride 2 and padding O. Linear(1568, 100) represents fully connected layer with 1568 input features and 100 output features. There are no max pooling average pooling used in these models and ReLU activations are applied between consecutive layers.
Training procedure. We retrained all the models used in experiment make them 1-lipschitz. The training strategy involves two phases: First, we train the model using the standard cross-entropy (CE) loss. Then, we retrain the model from scratch using a combination of KL-divergence and the spectral norm of the new model as the loss. During this phase, the outputs of the initially trained model are used as labels.
12

---

SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
B. Details on integrating our method into bound propagation
Bound propagation is an efficient framework for finding valid linear lower bounds for of f²)( within some input set E X. In this section, we first give a brief overview of performing bound propagation using the elementwise bound on preactivations. We then demonstrate how our results can be integrated into this framework yield SDP-CROWN, an extension capable of performing bound propagation using the form constraint on the preactivations.
We include concrete example in Section B.3 to illustrate the details of both bound propagation and SDP-CROWN.
B.1. LiRPA: bound propagation using the elementwise bound on preactivations
To better concept of bound propagation, express each 2(h) as function of the input and redefine the neural network ((x in (1) as
f(x) = (x), (x) ((++1) (eLU()(((t)) (x) = w for k = 1. 1 N 1.
The bound propagation we describe in this section the backward mode of Linear Relaxation based Perturbation Analysis (LiRPA) in (Xu et al., 2020) that efficiently constructs linear lower bounds for c" f(x) within an elementwise bound relaxation of the imput set X':
g(a)" h((a) S c (x) for all B (5, X
where ë, ò E IR are the radius and center of the elementwise bound.
LiRPA computes (9) by backward constructing linear lower bounds with respect to each preactivation 2 (x))
(a (x) + A (1*)) (a) S c" f(x) for all a E (T,
(10)
ie., starting from k: N all the way down to k = 1. Here, < (k) s 1 are variables of the same length as 2 (x)).
which are defined in (11).
For k N. The linear lower bound with respect to =(k) is simply
Jf (1)))) S cf f(x),
and therefore, (*)) (a)())) and h (a) =0 O.
For k = N - L,..., 1. LiRPA takes linear lower bounds with respect to (x)+1)(z)) ((10) at ++ 1) to construct linear bounds with respect to (x) ((10) at k). The first step is to substitute (()+)((x=) = ((++1) (cl.((())))))))))()))))))))))))) to yield
( ReLU(2 (*)
(*) (x)) + (h) s sc_ f(x)
where (k)) [W(+ g( (k+1) (a and (*)) (h(+ (k++t)) Since (cLU(2 (x)) nonlinear, LiRPA performs
linear relaxation on each ReLU(2; (x)) to propagate linear bounds from ReLU(=(() (x:) to 2 ((x) In particular, LiRPA
constructs linear bounds a; (x) S ReL.U(> (x)) s ((() 2i
(x)
(x) + vi within 2 (x) =((²1 S P3
(b)
(k) where
(k)
3. 1.
(k) =0
if 2
(k) (k)
- 2 0
= 0. (kk) = 0.
if (b) + P; 0 0
7 =0
(11)
a a p
(k) (M)
f tp!
20
7
(R) (2 +p (E
2p
otherwise,
and S (k)
< is a free variable that can be optimized (see Figure 5 for illustration). Here, the elementwise bound on
each preactivation
|2 (k)
(x)
2 < /! can be computed by treating 2 (k) (x) as the output of LiRPA, i.e., and
[(x) = (x))
Using (11), the linear lower bounds with respect to (kk are given by
(h) + +
(k) @ ((k))T2(0 (x) + 1 (+) + d(k) s (6 ReLUU)((())) + (()) <F
(12)
(a(t))
(a((a()))
(k) where c
max(c(()) 0} and ( (t), 03.
Finally, setting g(a)= = [ (a and M(a)= 1 (a())) yields the desired linear lower bound (9).
13

---

SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
(=)) 1- (x)
(eLU() (x))
ReLUie (F)) (( A (x)
0-aj (x)
0
0
200
P
84 +
(x)) simply upper and lower bounded by 2, (z). (Middle.) 2/ + Pi O. In this case, ReLU(z, (z)) (x) is simply upper and lower
Figure 5: Illustration of the linear relaxation (11). (Left..) 2/! - p(x)) 2 0. In this case, ReIUU2
(8)
(k)
bounded by 0. (Right.) 5/( p S 5 S 2 + + this case, ReLU(z,)) (x)) (x)
is lower bounded by a; 25
(8) (x) for
(k) and upper bounded by linear function intersects (z/ pj 0) and (z(*) + ((k) =(k)
(k)
+ P )
any a;
B.2. SDP-CROWN: bound propagation using the fo-morm constraint on preactivations
SDP-CROWN efficiently constructs linear lower bounds for e² [xx within an 4--nomm ball relaxation of the input set Xt:
g(a)²xx x + h(((a), A) S of ((x) for all x E (2 p) 2 X,
(13)
where i E I2 and IR are the center and radius of the f2-norm ball. To extend LiRPA to compute (13), we simply set i = â. p = p1 in (9) and follow the same process of LiRPA, except with the offsets h (a()) in (12) replaced by
( (a (K) (()) - - (x' (co -1= + X(R (0)*)) (g (M) (a (2) (( (((
where (a) 2 is a free variable that can be optimized and
( (g (b) (k)) xk) = minfc g (a) (a(*)) (4) p(0),
2())))) 0} for all
Here g(k) and (*) are the center and radius of the Eg norm ball for (x), i.e. || (x) - 2 S p(A), The E nomm W and
ball for ((x (ar) can be computed via the spectral norm of the weight matrices, as 5(k) w(k
p(k) = ||
||W(()) llp,, or by more sophisticated methods such as (Fazlyab al., 2019). Here, we use [|W(0))|2 2| denote the spectral fg-norm of the matrix (((), We note that by Theorem 4.1, we always have
lg (1)) (8) (x) + (8) (g 18) (a (k) (,()))) S c² f(x) for all æ E B2(d,
(14)
for all k= N, N,...,1.
Finally, setting g(a)= = [Wa)T ( (a and h(g(a), = h (a)) (() yields the desired linear lower bounds in (13).
B.3. A small example LiRPA and SDP-CROWN
We give a step-by-step illustration of how to find a linear lower bound on cf f(x) within ||x - a112 S p. Here, we consider a 3-layer neural network (z) with
-1 1]
T 1
c= 1, 33 = 111 -1], w = i -1
w(
= p -=1. 1.
1
0
LiRPA. For simplicity, we compute each intermediate bound (x)) - 2 <
( via interval bound propagation
(Gowal et al., 2019), and always pick (A)) = 0 in (11) for A 1, 2. In this particular example, the choice of ā @(*) does not affect the final result. The intermediate bounds are given by
1
0
2 2
g() =
(())
2(2)
0
14

---

SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
Starting at & 3, we simply have
g ) 1, (a = 0.
At k = 2, substituting (x) W ReLU(=(((x)) and constructing af of I ReLU(zz((()) 1
8/²0 2/ ( (x) + + (2) via (x) - 1 f 2 gives
e g -1
[-] d (a(3) 0, a -0=-00
0
(
0.5
7(2)
1
1
0
0.5
Therefore, we have
-0.5
(a!2)) = c/ 3 (2) + (2)
о 0,3(20
(a
(0 + d -2
-0.5
At h 1, substituting (x) 2 ReI.U(=((x)) and constructing
2 (x) S ReI(Uzz( s
8 2j [0(()) (x) + Ys (1) via (x) - | - ~()) gives
e = (a 0
(a dاه) 1 (a = 22, a
g H
7:0 =
0 0
00
1
Therefore, we have
00
(a())) = o 2 + +000 (2) o 0.000
0
(c (000)dd) +d = --2.
As result, from LiRPA, conclude
-2 = 0
i 1.
+ -2
S 2.1.111111 f(x) for all
For simplicity, we compute each intermediate bound (z) 201)12 (()) for k =1,2 via the Lipschitz constant of W(k), which is given by
SDP-CROWN.
=(I) (()) p0)==111 =1, 5(2) =0)= = 0
((2) = 2.
Starting at k 33, 3, we simply have
(3) (a 1, (2 = 0.
k 2, taking , (a from LiRPA, setting d(2) h (3) (g (3) (3)) ). ((3)) 0. and substituting them into
(9 (2)), 1(2) =
1
(1)) (10121)-111(()) -1 + 22)
( (211), x1111133 + d(2)
1
2
4x)(2 + 122 0.5
2
Notice that 2 (22) (2) (2),, 122) is maximized at ( V 1/8, and hence we have
-0.5
g (a
(2) =
(a ((2))= -2, x V1/8.
0.5
15

---

SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
At k 1, taking c0 (a)(( from LiRPA, setting d(1) (1 -v2,, and substituting them into
(a
1
1(1)
(
1 A(1)
| (g (a) ),(0))13 + d(
2
1
-1(0) 1 \(1)
|| - (1) (1)) 03 v2
2
(-x") + +1(0, |min| f 201) 20) 20, ,0113) v2
2
2 (a") - -22.
Obviously, max h()) (g (a ) is maximized at A()) 0, and hence
0 (a'))((())) v2,
( (1)
1 0.
As result, from our method, we conclude
T x - 11- for all x |
1
In this particular example, our method tightens bound propagation by exactly factor of V2.
C. Some extensions of SDP-CROWN
In this section, we describe several extensions that can further tighten SDP-CROWN.
C.1. Ellipsoid constraints
The tightness of SDP-CROWN hinges crucially on the quality of the & f--norm ball relaxation (2(2(M) ((0) 2 (z(1) x E
(2 p)} for the input set each (k) during the computation of linear lower bounds (14). However, in general settings, fo-norm balls might not be the best choice to relax the input set at 2()) For illustration, consider simple one-layer example with
(1)) =
0.5
0.5
5
0
==1. 1.
1.5
0.5
0
As illustrated in Figure 6, the input set at 2(1), (2(1) relaxing this input set by naively propagating no-m ball from x to (1) can result in extremely loose relaxation. To address this issue, we generalize SDP-CROWN to handle ellipsoids of the following form
I
E B2( is rotated and elongated ellipsoid; therefore,
Ez P) = {- diag( - #) 11}
where é, ò E IR" are the center and axes of the ellipsoid.
We note that the ellipsoid can also be efficiently propagated via the Lipschitz constant of (R)., Given E2(2(k), p(()), one simple heuristic is to select the center and axis for (2((++1), (((( as
=(k+1)= ((++))
((*+1)= = y - diag()(*) ||2 with y [[((++)) ((ag
where || I|,2 = / (W & W denotes the rowwise & norm of a matrix W.
C.2. Intersection between ellipsoid and elementwise constraints
at (R) into account when com- puting the relaxation of (7). In particular, SDP-CROWN can be further tightened by considering the intersection between the ellipsoid (2k((,), ,(()) and the elementwise bound B (2 (k(k), (rak) at 2(k) For illustration, in Figure 7, we plot the
Another extension of SDP-CROWN is to also take the elementwise bound B
16

---

SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
[ l Bll
By ((
By
0
-1
-1
Figure 6: Constructing the 62-norm ball and the ellipsoid relaxation at =(4) for one layer neural network with W(2)
[0.5, 0.5; 1.5, -0.5]. & = [0; 0] and 1. (Left.)) The input set at 21) with respect to the f--norm ball input set (2 (ē, p)
at x. The input set at =²(2) is a rotated and elongated ellipsoid. (Middle.) The 62-norm ball relaxation B2(2(), p()) at
2()), where g(1) = [0; 0j and p())
| = 1.5302. fn-norm ball does not have enough degree of freedom to
capture the shape of the input set at 211), (Right.) The ellipsoid relaxation & ())) at e(1), where $(1) [0: 0] and p(1) [0.5464; 1.9360]. The ellipsoid can better capture the shape the input (2)).
Le |a Baik.o))
[ B( Bu (ro)
Bith Eatall (PM) Buttt (P
Figure 7: Constructing the intersection between ellipsoid and elementwise bound as a relaxation at 2 for one layer neural network with ((1) = [0.5, 0.5; 1.5, -0.5). & = [0; 0] and = = (Left..) The input set at 20)) with respect to the f2-norm ball input set B2 p) at x. The input set at (1) a rotated and elongated ellipsoid. (Middle.) The elementwise bound relaxation ax (2 (()) at 20), where (()) 00: and p()) || 11. [0.7071; 1.5811]. (Right.) The intersection between ellipsoid E2 (()) and elementwise bound (5(1), p()) (1), where g(L) [0;0]
and p()) [0.5464; 1.9360] The intersection removes the corners of B (2(1), ((1))
intersection between the elementwise bound (2(k), p(k) and the ellipsoid & (2(k) a(k) using the same one-layer ex- ample in Figure 6. In this case, the intersection removes four corners of B (g(k), p(k)). We note that as the dimension increases, the number of corners removed grows exponentially.
We can simply accommodate (z p(k)) by adding the following inequality constraint into (7)
RcLU(x;; (((h) (k)
where ( and 7, are defined in (11). We summarized the extension of SDP-CROWN for handling the intersection between the elementwise bound B. (2(8), (()) and the ellipsoid F,(2()),p()) in the following Theorem. Theorem C.1. Given e, ft, p, R" where P. 0. The following holds
C ReLUU()) TT hg. X, for all B
(o,
for any X, 0 and g I² where
Mgg (g = X(1 [ + ( 200)
> 16 X, x,,,
1
and
(c(g, X, = m.-minn - 9: + T(6i Tz)) Ao 2., 9i 7 + 3.) + 23.
17

---

SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
C.3. Proof of Theorem C.1
Given a linear relaxation c² (R)UU() 2 g"x h that holds within x E E2 p) B (5, tightest possible h within () n B (2: p) admits the following generic problem
(ā, p), the process of finding the
A: + 8;
p - x2
min e ReLLU(2) - g= s.t. diag(() - 'xx 2)1l2 S 1, *ER"
ReLU(a;)
x
+
for i = 1,...,
2p:
2p:
Without loss of generality, we assume a; - A 5 S क. + P. for all i. Applying the positive/negative splitting x = u where u, v 2 0 and u 3 v 0 yields the following
min u
ch g²(uu 2)
Σ (p_ uu)² - -2p," (w: - v,),, + 10,'0,)) < 1- -
s.t.
(15)
1=1
(i: Tz) u; + (e: + tz)0 S - - for i = ,,...,7, "
u u 0, v 20 v 0.
The SDP relaxation of (15) reads:
min U.U.U.UUVVEE
Tu- - 5 g0(u==
(u- v)
n
Σ " 2p, (u, - 0;)a; + -V S || diag (p) 1a1/2
s.t.
(p: ;))u; + (p: + =;);; $ p - a for = 1,...,n. n
u 120 0, 0 v20, 20,
ü+ 1=
ü; u1
0 0 V
0,
0
for i = I,...,n.
n.
02
Let E denote the dual variable of the first inequality constraints, т; E denote the dual variable of each (ø. k.)us; + (ø: + +z)a S गे 2ł. and 8, 8,4,, Rn denote the dual variable for u 0, 2 0 and respectively. The Lagrangian dual is given by
(A(1 ||diag()) 1 (2)
27 2-
ppop- 1)
max A,t,8,t.je
s.t.
C1 - 9: + Te(pi Σj) Ap; 2 8t
Hi
- 91 + (p: 2,))
>pp 20. st
- 0 for 1,..., ny
gi + (p
+ a.) + Ap, 2; - tt
0 for i I,...,
91 + (Ø: + x.) + Xp;
- 2z. - 4
p X
A 0, T20 0, 8 z 0, 12 0,
n 2 O.
For a 2 x 2 matrix, note that X - 0 holds if and only if det(() 2 and diag(X) 2 0. Applying this insight yields a second-order cone programming (SOCP) problem
1
2 - 1 80 +00)) 11 s.t. , 2 (c - 9i + (; - 5;) - 2
max A,
$;)², -
(16)
nx > 0z + T( + -z) 20 - 11)²
A 2 0 7 720 0, s20, 120 0, 2 0.
We are now ready to prove Theorem C.I.
18

---

SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
Proof. Given any gg IR. Let Ar - 91 + + -.)) >Ø; 2 and b, -u( Te + T.,) ^0r 2.y)) Fixing
any X, r 2 0 and optimizing js in (16) yields
1
max { - [0)=-s))2a0 (b; - tz)
A(1
A,8,220
A
1
min {a,, h4 0]
max X20
2
A
max T, X20
where the first equality follows from ming,20(4, sz)² min man 0}2 and min,, (b; - 1,,2 = min and max m 0}2; min(b;, bi, 0}2] minfa;, bū, 032 for any a, E R. Since h(g, 7) is a lower bound on (15) for any x, 2 0, we have c² ReLU(x) 2 g"v h(g. for all () B (., for any g E R, 0.
D. Derivation of the dual problem (8)
Recall that we have the primal problem
min U.
cuu u g² (u v)
(U + +V - -(( - -) S sp 2- 1
s.t.
u 2 0, V 2 0,
û+ =1
ü; 4:
0
U
0,
2 0 for = I.....n.
U.
1/
Let A 2 0 denote the dual variables of the first inequality constraints. 8, t 2 0, E R" denote the dual variable for u 2 0,
v 2 0 and ū + i = 1, respectively.
y:
y/
0,
2
z denote the dual variables of the last two PSD constraints
y/ Y;
21
Ze
for I....n. n. The Lagrangian is given by
C(ū,0, u, U,
V, 8, (,
Σ 1=1
Cuu
g: v.)
AUU, + V2) 220,(u- - -ma)
-2(0² - -1
(8:44 + (2;)) + Σ uilū; + 0; 1)
Vi
yi
W4
Σ
2i
Y/
Yi
24
2g
V/
Rearranging the terms, have
V. - 1| - Σ k4
1m 1
4 11
1(q - 9i - 2X4; 86)
1/4
U4 U4
(17)
(G 9: - - 31) -
A- Y,
U
14-
[c 2X4; (4) zi
T Vi
(18)
(c 2X'; 14) zi
X Z
V.
19

---

SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
Minimizing the Lagrangian the primal variables yields
min U.S.u.u.U.VE..
L(ū, 0, u, U, X, s, 2.
A(p² (
E 1==1 Mi
if (17) = 0 and (18) = 0 for all U, R
8
otherwise
where
(17) 0
Vi
Vi
14
[G 9i
2xă; ss)
for all é E (I.....m.)
M/
Y1
[/ 9:
2 8,)
A
(18)
E 24
14
2 (
+
2xσ; 4i)
for all E (I....,n..
Ai
Z
[/ + 2AĀ; ti)
A
Hence, the Lagrangian dual is given by
1(p² - 1|0112) 1=1
A,8,f,
2(1 9i - 2λu;; -8i]
s.t.
[ - 9: 2\d; - s;)
X
0 for i = 1,...,
[ + 2\σ; - 44)
14
= 0
for i = 1, -.....
(c + 2\0; - 4))
X
X2 0, 8 2 0, t 0,
1 120 0.
Rescaling \ = 1 and μ = j to yield
1
M(p² 11x1
2 1
max A.
2
14
C 91
20 for i 1,...,,. n
C₁ 91 Xā;-
8,
X
Mi
9i
X6; 4 X
2 0
for i 1, 1,...,n,
9 + Xā;
X 2 0, 2 0, 12 0,
J 0.
For x matrix, note that X 2 0 holds if and only if det and diag(X) 2 0. Finally, applying this insight yields the desired dual problem:
- xx ( 1
max X.
s.t.
dp4 2 (a - 9: 5; X²,) for i 1, n. Ap4 2 (-g +4 - A2,) for i I,...,
z 0, 8 820 0, 2 0, p 2 0.
20


Reviews:
[{"review_id": "potjEQ2usK", "reviewer": "Reviewer_4cg2", "summary": "The authors propose a new method they call SDP-CROWN. They use the framework of semidefinite programming to derive linear bounds on the networks behaviour however based not on an $L_\\infty$ norm but based on $L_2$ norm bound perturbations. This linear bound can then be used for any linear bound propagation method to obtain a certificate. Specifically, what they do is to use a standard bound propagation method, but the constant offset of that bound is then adjusted (from an $L_\\infty$ bound to and $L_2$ bound offset) but still sound.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We want to thank reviewer 4cg2 for valuable comments and for recognizing the key contributions of our paper. We hope our response would adequately address your questions and concerns.\n\n **\"They claim that their bounds can be up to $\\sqrt{n}$ better compared to standard single-neuron bounds. While this is clear for the input - for the output this can be larger or smaller i would assume. (imprecisions can accumulate) \"**\n\nThe input bound improvement by a factor of $\\sqrt{n}$ follows directly from the fact that the volume of an $\\ell_2$ ball is smaller than that of an $\\ell_\\infty$ box by this factor.\n \nRegarding the output bound, we prove that our method can achieve up to a $\\sqrt{n}$ improvement vs traditional bound propagation (Theorem 5.2). However, this proof applies specifically to as simple network $\\mathrm{ReLU(x)}$ under $\\ell_2$ perturbations of the form $\\Vert x\\Vert_2\\leq\\rho$. \n\nFor general multi-layer neural networks, the extent of improvement is hard to quantify theoretically. To address this, we provide empirical results demonstrating that our method consistently outperforms bound propagation methods, especially on large neworks.\n\n**\"The experimental design is standard. That said, I would be curious how far one could push the method.\n\"**\n\nThank you for your insightful comment. In this paper, we utilize SDP to tighten the offset of the linear bounds in bound propagation. Our method has been integrated into $\\alpha$-CROWN with minimal overhead, as it only introduces one additional variable $\\lambda$ per postactivation neuron. \n\nOur next step is to integrate our method into the $\\alpha,\\beta$-CROWN codebase, hence allowing our method to work with powerful branch-and-bound based methods and a wide range of neural network architecture. Our current algorithm already outperformed the existing branch-and-bound based approaches (including GCP-CROWN, BICCOS and beta-CROWN, as presented in the **[new table](https://imgur.com/a/QITgjmq)** we added during rebuttal), and additional improvements can be further demonstrated once we finish this integration. Additionally, we aim to extend our approach to jointly optimize both the slope and offset terms, with the goal of developing optimal linear relaxations for $\\ell_2$ perturbations.  We expect these two future directions to yield tighter results on an even larger scale than considered in the present paper.\n\n**\"Most related work I know of is adequately discussed. What I find curious about the work here is that the offset adjustment here is exactly the opposite of what is done in [A] and [B], where unsound bounds are adjusted to be sound. Here, sound bounds are adjusted to be more tight but still sound.\"**\n\nWe appreciate the reviewer for bringing these references to our attention. We will include a discussion of these works in the final version of our paper.\n\n[A] presents a method for certifying robustness against geometric transformations. This approach begins with potentially unsound bounds and subsequently adjusts them to be sound through a combination of sampling and optimization techniques. In contrast, our method operates in the opposite manner; we start with sound bounds and refine them to be tighter while ensuring they remain valid.\nRegarding [B], we believe this reference may have been included by mistake, as it presents a framework for robotic tissue manipulation using deep learning for feature extraction, which does not appear relevant to the context of our work. We will be happy to discuss any additional works you suggest.\n\n**\"I have the feeling that the limits regarding the most optimal linear bounds (Salman et al 2019) regarding the expressivity also apply here. Specifically, just restricting $\\ell_2$ to $\\ell_\\infty$ and adjustment of the offset do not address fundamental expressivity shortcomings.\"**\n\nOur critical contribution is to introduce multi-neuron SDP relaxations into bound propagation. This allowed us to overcome the “convex relaxation barrier” faced by traditional single-neuron LP relaxations underlying the vast majority of prior work. It also improved upon prior work on multi-neuron relaxations, which were either too loose (i.e. LP-based) or limited to tiny models (i.e. SDP-based). Addressing $\\ell_2$-norm constraints is a crucial first step, but we anticipate further work to greatly expand the applicability of models and new threat models (beyond $\\ell_p$ norm) using our key idea of combining SDP with bound propagation. We will also cite the paper on the Expressivity of ReLU networks in our final version.", "claims_and_evidence": "- They claim that their bounds can be up to $\\sqrt(n)$ better compared to standard single-neuron bounds. While this is clear for the input - for the output this can be larger or smaller i would assume. (imprecisions can accumulate) \n- The authors claim also soundness which is supproted by a proof (4.1).", "methods_and_evaluation_criteria": "The method is evaluated against several competitors that are tailored for $L_\\infty$. Evaluation takes place on MNIST and CIFAR-10 which is standard. The creteria are certified accuracy and time.", "theoretical_claims": "See above.", "experimental_designs_or_analyses": "The experimental design is standard. That said, i would be curious how far one could push the method.", "relation_to_broader_scientific_literature": "Most related work i know of is adequadely discussed. What i find curious about the work here is that the offset adjustmeht here is the opposite of what is done in [A], where unsound bounds are adjusted to be sound. Here, sound bounds are adjusted to be more tight but still sound. \n\n- [A] https://proceedings.neurips.cc/paper_files/paper/2019/file/f7fa6aca028e7ff4ef62d75ed025fe76-Paper.pdf", "essential_references_not_discussed": "- https://openreview.net/pdf?id=awHTL3Hpto I have the feeling that the limits regarding the most optimal linear bounds (Salman et al 2019) regarding the expressivity also apply here. Specifically, just restricting $\\ell_\\infty$ to $\\ell_2$ and adjustment of the offset do not address fundamental expressivity shortcomings.", "other_strengths_and_weaknesses": "I like the combination of SDP and linear bound propagation. This is a neat idea - though it is not quite clear to me how far one could push this idea.", "other_comments_or_suggestions": "No further suggestions.", "questions_for_authors": "The question are above.", "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": "CAQsiY7689", "reviewer": "Reviewer_4uhX", "summary": "The work proposes SDP-CROWN, a modified bound propagation framework based on CROWN for verifying the robustness of neural networks to $\\ell_2$ norm perturbations. SDP-CROWN introduces an additional parameter into the bound propagation framework which is used for tightening the bias term in the linear relaxations propagated through the network. The formulation for the bias term is derived from the tighter Semidefinite Programming relaxation and enables a more accurate representation of the $\\ell_2$-norm interdependencies between neurons. When compared to a number of competing approaches, the authors show experimentally that their method results in tighter bounds while preserving scalability.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank you for the detailed review. We added **additional experiments on GCP-CROWN and BICCOS, as well as LipSDP [5] (another SDP method) for all models** as requested. We hope you can reevaluate our paper based on our response.\n\n**Clarifying Figure 1**\n\nWe apologize for the confusion and will correct Figure 1. The model name should be ConvLarge, not ConvBig. ConvLarge is trained on CIFAR-10 and has 4 convolutional and 3 linear layers, totaling 24.6M parameters. The whiskers in Figure 1 illustrate the uncertainty gap where the true certified accuracy lies; blue numbers represent lower bounds on certified accuracy from different methods, and red numbers represent the PGD upper bound. A smaller gap indicates stronger verification.\n\n**Comparison to GCP-CROWN and BICCOS**\n\nDuring the rebuttal period, we implement $\\ell_2$ norm support into GCP-CROWN and BICCOS. Particularly, the cutting planes found were using precise $\\ell_2$ norm constraints rather than directly constructing an enclosing $\\ell_\\infty$ ball. This shows the best GCP-CROWN and BICCOS can do. We included comparisons to GCP-CROWN and BICCOS on **all benchmarks** in Table A below.\n\n[Table A: Comparisons to new baselines](https://imgur.com/a/QITgjmq)\n\nSince GCP-CROWN and BICCOS are all part of the $\\alpha,\\beta$-CROWN verifier, to avoid confusion, we renamed the original $\\alpha,\\beta$-CROWN baseline to $\\beta$-CROWN (Wang et al., 2021). GCP-CROWN and BICCOS marginally improve over $\\beta$-CROWN, although the gap to our method is still large especially on bigger models.\n\n**Explain BM method**\n\nBM is an SDP-based method [6]. It exactly solves the SDP relaxation of the verification problem using specialized low-rank solvers. BM is one of the tightest SDP-based verifiers (as demonstrated in their paper) but is not scalable to CIFAR-10 models. We choose BM because it is a recently published SDP-based method with strong results.\nBM is tighter than our method because our approach remains LP-based as the SDP relaxation is only used to refine the offset of linear bounds. However, our method is orders of magnitude more scalable; our ConvLarge is a factor of 100x larger than the models considered in BM. Our comparisons with BM demonstrate that the substantial improvement in scalability achieved by our method comes with only a mild loss of tightness.\n\n**Comparison to SDP-based methods**\n\nBesides the BM SDP-based method already reported in our paper, we conduct additional experiments on LipSDP [5] in Table A. \n\n[Table A: Comparisons to new baselines](https://imgur.com/a/QITgjmq)\n\nFor a fair comparison, we run LipSDP with multiple configurations by splitting original networks into subnetworks. We show the results in Table A. The verified accuracy by LipSDP is significantly lower than ours, even in the tightest (slowest) setting with no split.\n\nWe also considered additional SDP baselines that can scale to the networks we evaluated, such as SDP-FO (Dathathri et al., 2020). However, we found that their algorithm and implementation support $\\ell_\\infty$ norm only, and it is not straightforward to adapt their implementation to our setting.\n\n**Add new references**\n\nThank you for bringing these references to our attention. We will incorporate these works into the final version to provide a more comprehensive discussion of related research. We’ve added an experimental comparison to GCP-CROWN [1], BICCOS [2], Lip-SDP [5] above, and [6] is the BM in our paper. We will cite and discuss [3] (a survey paper) and [4] (focusing on training certifiable networks with special architectures).\n\n\n**Response to Questions For Authors:**\n\n1.  Given $c^T\\textrm{ReLU}(x)\\geq g^Tx+h$ that holds within $\\Vert x-\\hat x\\Vert_\\infty \\leq \\rho$. Observe that from bound propagation $g_i=c_i$ if $\\hat x_i>\\rho$, and $g_i=0$ if $\\hat x_i<\\rho$. Hence, $c_i\\textrm{ReLU}(x_i)-g_ix_i=0$ if $|\\hat x_i|>\\rho$. Therefore $x_i^\\star=\\hat x_i$ is a minimizer of $\\min_x c^T\\textrm{ReLU}(x)-g^Tx\\text{ s.t. } \\Vert x-\\hat x\\Vert_2 \\leq \\rho$ if $|\\hat x_i|>\\rho$, and $x_i$ can be removed by substituting $x_i=\\hat x_i$. It follows from positive/negative splitting $x_i^\\star=u_i^\\star - v_i^\\star$ that $u_i^\\star=\\max\\lbrace\\hat x_i,0\\rbrace$ and $v_i^\\star=\\min\\lbrace\\hat x_i,0\\rbrace $.\n \n2 & 3. See our comparison to GCP-CROWN, BICCOS, LipSDP and BM above.\n\n4. Our method is a hybrid framework that tightens bound propagation using SDP relaxations specifically for ReLU activations. Our approach is complementary to existing work on leveraging specialized architectures, offering an alternative route to achieve certified robustness. We will add a paragraph to discuss methods that leverage specialized architectures, such as [4], Cayley layers, AOL, SLL, etc. While a direct comparison is not feasible due to the different aims of these approaches, we will explore the design of verification-friendly architectures that can utilize the strengths of both bound propagation and specialized architectures in future work.", "claims_and_evidence": "- The general claims are mostly supported by sufficient evidence. SDP-CROWN clearly outperforms the baselines which are considered by the authors. However, as mentioned in the methods section, some comparisons with other methods are missing which makes it more difficult to assess the contributions of this work. Besides this, a clarification of what the \"BM\" method is (which outperforms SDP-CROWN) would be helpful.\n- Figure 1: This figure is supposed to show the advantages of SDP-CROWN, but I find it confusing for a number of reasons. Firstly, it is unclear which dataset the ConvBig network used for creating this figure is actually trained on. Secondly, the caption refers to Section 6.1 for details but 6.1 does not contain any results on ConvBig. Thirdly, the axes in the figure are not labeled, it is unclear what the whiskers represent (confidence intervals? Or is the upper number the PGD upper bound of robustness?). Lastly, the numbers mentioned in the caption are different from the ones shown in the figure. Overall, this figure probably needs to be revised and currently doesn't help understand the method.", "methods_and_evaluation_criteria": "- I wondered why the method is only integrated into the $\\alpha$-CROWN verifier and not into $\\alpha, \\beta$-CROWN or even GCP-CROWN [1], possibly with the BICCOS cuts [2]. If this is difficult to do, at least a comparison with these should be possible. Since the authors describe at the beginning that this is not extremely difficult to do (just construct an $\\ell_\\infty$ box containing the $\\ell_2$ box as a naive baseline), there seem to be little reason not to provide those results on the state-of-the-art verifiers (unless I'm missing something here).\n- The fact that no benchmarking against SDP solvers is done despite the fact that the authors repeatedly mention that they are the most suitable method for solving $\\ell_2$ robustness verification problems is a major weakness of the work. In Section 6, they state that \"We ignore the comparison with SDP-based verifiers as we only use SDP relaxation for facilitating linear bound propagation over a $\\ell_2$-norm ball region.\". I don't understand this argument, to me the fact that SDP is only used in a certain way in the proposed approach doesn't mean that the proposed approach shouldn't be benchmarked against what the authors themselves identify as the (presently) most suitable way to solve the verification problem.\n\n[1] Zhang, H., Wang, S., Xu, K., Li, L., Li, B., Jana, S., ... & Kolter, J. Z. (2022). General cutting planes for bound-propagation-based neural network verification. Advances in neural information processing systems, 35, 1656-1670.\n\n[2] Zhou, D., Brix, C., Hanasusanto, G. A., & Zhang, H. (2024). Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes. arXiv preprint arXiv:2501.00200.", "theoretical_claims": "I checked all the proofs in the main part of the paper. Some of them are a bit difficult to follow since a number of reformulation/rewriting steps are done implicitly, but overall the proofs seem correct to me.", "experimental_designs_or_analyses": "In Table 1 there is a method termed \"BM\" for the MNIST-MLP which appears to outperform SDP-CROWN by a significant margin (although the runtime is much longer). Could the authors clarify what this method is and why it is not explained in the paper? I was surprised to see a method here which outperforms the proposed method but is not described in the work.", "relation_to_broader_scientific_literature": "$\\ell_2$ robustness is not considered in most of the verification literature or only considered in a somewhat naive way (except for the global robustness literature and the works on constructing networks with small Lipschitz constants), so this work tackles a problem that seems relevant. I find the lack of of contextualisation and comparison with these methods problematic.", "essential_references_not_discussed": "There seem to be a number of references on verification of neural networks to $\\ell_2$ norm robustness missing in the related work section. The section only mentions SDPs and standard bound propagation. However, there are a number of other works on such perturbations, see e.g. Table 1 in [3] for a number of other papers that support $\\ell_2$ perturbations. There are also works such as [4] which construct networks more amenable to robustness verification and which usually focus on $\\ell_2$ robustness as well. However, neither of these feature in the related work section. Approaches such as [5] which compute the Lipschitz constant of a network using SDPs might also be relevant. A comparison with the method proposed by [6] which also supports $\\ell_2$ perturbation would be extremely important since that method seems to perform comparably well when compared to bound propagation methods.\n\n[3] Meng, M. H., Bai, G., Teo, S. G., Hou, Z., Xiao, Y., Lin, Y., & Dong, J. S. (2022). Adversarial robustness of deep neural networks: A survey from a formal verification perspective. IEEE Transactions on Dependable and Secure Computing.\n\n[4] Hu, K., Zou, A., Wang, Z., Leino, K., & Fredrikson, M. (2023). Unlocking deterministic robustness certification on imagenet. Advances in Neural Information Processing Systems, 36, 42993-43011.\n\n[5] Fazlyab, M., Robey, A., Hassani, H., Morari, M., & Pappas, G. (2019). Efficient and accurate estimation of lipschitz constants for deep neural networks. Advances in neural information processing systems, 32.\n\n[6] Chiu, H. M., & Zhang, R. Y. (2023, July). Tight certification of adversarially trained neural networks via nonconvex low-rank semidefinite relaxations. In International Conference on Machine Learning (pp. 5631-5660). PMLR.", "other_strengths_and_weaknesses": "The strengths and weaknesses are mentioned above.", "other_comments_or_suggestions": "#### Typos\n- Line 113: tightened by optimizing over the linear relaxation themselves --> tightened by optimizing over the linear relaxation**s** themselves \n- Line 160: defining a set of linear relaxation --> defining a set of linear relaxation**s**\n- Line 170: why bound propagation tends to be lose --> why bound propagation tends to be lo**o**se\n- Line 177: \"with radii $\\|x - \\hat{x}\\|$\" - what norm is this? I assume $\\ell_2$?\n- Line 177: are a factor of $\\sqrt{n}$ than the radius --> are a factor of $\\sqrt{n}$ **larger** than the radius\n- Line 244: the bound [...] satisfy --> the bound [...] satisf**ies**\n- Line 253: We are now ready to proof --> We are now ready to pro**ve**\n- Line 255: Fix any [...] and optimized each [...] yields --> Fix**ing** any [...] and optimiz**ing** each [...] yields\n- Line 257: We show**s** that --> We show that\n- Line 260: As shown in Lemma 5.1, linear lower bound [...] yields --> As shown in Lemma 5.1, **the** linear lower bound [...] yields\n- Line 266: The desire result follows --> The desire**d** result follows\n- Line 271: our method is guarantee to --> our method is guarantee**d** to\n- Line 321: and $h(\\alpha)$ form $\\alpha$-CROWN --> and $h(\\alpha)$ f**ro**m $\\alpha$-CROWN\n- Line 410: As neural network verification is **an** NP-hard, all methods --> As neural network verification is NP-hard, all methods\n- Line 429: significantly narrowing the gap the PGD upper bound --> significantly narrowing the gap **with respect to** the PGD upper\nbound\n\n#### Other\n- Can Figure 4 be moved to the main paper? It seems like there would be enough space for it and it would make it easier to check the figure while reading Section 6.3.", "questions_for_authors": "- Could the authors explain their reasoning in line 205ff a bit more? They assume that $\\| \\hat{x} \\|_\\infty \\leq \\rho$ holds and if it doesn't, they substitute something with $u_i^*, v_i^*$. Could they explain where exactly this $u_i^*, v_i^*$ are substituted and how that leads to their assumption being correct?\n- Could the authors comment on GCP-CROWN/BICCOS and why they weren't considered in this work? Are any results on these verifiers available?\n- Is there a reason why SDP-based verifiers are not evaluated?\n- Are the authors aware of the substantial body of literature on $\\ell_2$ robustness verification using special architectures such as [4] above? Could the compare their work/contextualise it relative to those works?", "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": "nsD5bILN4x", "reviewer": "Reviewer_zfFU", "summary": "The paper introduces SDP-CROWN, a hybrid framework combining semidefinite programming (SDP) relaxations with bound propagation for neural network verification under L2-norm perturbations. The core contribution is a novel linear bound derived from SDP principles that includes a new bias term h, which provides theoretical guarantees for L2-norm balls. Theoretical analysis shows the proposed bound can be tighter than bounds computed for the L-infinity norm. Experimental results demonstrate that SDP-CROWN outperforms state-of-the-art verifiers like α-CROWN and α,β-CROWN while maintaining moderate runtime.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We want to thank reviewer zfFU for for your positive feedback and valuable comments. As suggested, we’ve added new experiments on GCP-CROWN [2] and BICCOS [3] (a follow-up work of GCP-CROWN), as well as a more sophisticated Lipschitz constant method (LipSDP [1]). \n\n**New experimental results**\n\nWe provide additional comparisons with LipSDP [1], GCP-CROWN [2], and BICCOS [3] in the table below, using the same settings as Table 1 in our paper. We report the verified accuracy (%) and average per-sample verification time (in seconds), except for LipSDP, where we report the total time required to compute the Lipschitz constant.\n\n[Table A: Comparisons to new baselines](https://imgur.com/a/QITgjmq)\n\nSince GCP-CROWN and BICCOS are all part of the $\\alpha,\\beta$-CROWN verifier, to avoid confusion, we renamed the original $\\alpha,\\beta$-CROWN baseline to $\\beta$-CROWN (Wang et al., 2021). GCP-CROWN and BICCOS marginally improve over $\\beta$-CROWN, although the gap to our method is still significant, especially on large models. LipSDP can outperform native Lipschitz but is still not competitive compared to our method, and computing the Lipschitz constant using SDP is also quite slow and not scalable.\n\n[1] Fazlyab et al. \"Efficient and accurate estimation of lipschitz constants for deep neural networks.\" NeurIPS 2019\n\n[2] Zhang et al. \"General cutting planes for bound-propagation-based neural network verification.\" NeurIPS 2020\n\n[3] Zhou et al. \"Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes.\" NeurIPS 2024\n\n**\"Whether the chosen radius for L2-norm perturbation is reasonable\"**\n\nWhile Table 1 only presents results for a single $\\ell_2$ perturbation radius, we would like to highlight Figure 4 (c) (d) in Appendix (also [linked here](https://imgur.com/a/MFUS3RX)), which presents the certified lower bounds computed from different methods over **a wide range of $\\ell_2$ perturbation radii**. As shown in Figure 4, our lower is consistently tighter than $\\alpha$-CROWN and the naive Lipschitz approach across different perturbation radii, which demonstrates the effectiveness of our approach.\n\n**\"More advanced methods beyond naive Lipschitz\"**\n\nWe agree that more advanced methods based on Lipschitz constant estimation can yield significantly tighter robustness bounds. To address this, we have added a comparison with LipSDP [1] in the [Table A](https://imgur.com/a/QITgjmq) above, which employs SDP relaxation to estimate the network’s Lipschitz constant. This provides a stronger baseline for Lipschitz-based verification methods. Our method still significantly outperforms this baseline in all scenarios.\n\n**Response to Questions For Authors:**\n1.  While our current work focuses on refining the bias term $h$, it is certainly possible to refine both the slope term $g$ and bias term $h$ simultaneously for tighter bounds. A key direction for future work is developing an efficient parameterization of $g$ that can be seamlessly integrated into existing bound propagation frameworks.\n2. BM is an SDP-based method [4]. It exactly solves the SDP relaxation of the verification problem using specialized low-rank solvers. BM is one of the tightest SDP-based verifiers (as demonstrated in their paper) but is not scalable to CIFAR-10 models. We choose BM because it is a recently published SDP-based method with strong results.\n\n3. We have added a comparison with GCP-CROWN [2] and BICCOS [3] above. The original GCP-CROWN implementation considers $\\ell_\\infty$ norm only, but we’ve able to extend the implementation to $\\ell_2$ norm by finding cutting planes specifically for $\\ell_2$ norm input constraints. It marginally improves performance and the gap between GCP-CROWN and our method is still large esepcially on bigger models.\n4. We note that without $\\mathrm{rank}(X_i)=1$, $X_i\\succeq 0$ alone does not imply $u_iv_i = 0$, and the relaxation stems from dropping the constraint $\\mathrm{rank}(X_i)=1$. Specifically, to derive SDP relaxation of ReLU activation: $x_i=u_i$, $u_iv_i=0$, $u_i\\geq 0$, $v_i\\geq 0$. We first add a redundant constraint $X_i=[1\\ u_i\\ v_i][1\\ u_i\\ v_i]^T\\succeq 0$ and then set $U_i=u_i^2$, $V_i=v_i^2$, and $u_iv_i=0$ in $X_i$. It is clear that $X_i\\succeq 0$ and $\\mathrm{rank}(X_i)=1$ if and only if $u_iv_i=0$. Since $\\mathrm{rank}(X_i)=1$ is nonconvex, we drop the rank-1 constraint to obtain the SDP relaxation: $x_i=u_i$, $u_i\\geq 0$, $v_i\\geq 0$, $X_i\\succeq 0$.\n\n[4] Chiu et al. \"Tight certification of adversarially trained neural networks via nonconvex low-rank semidefinite relaxations.\" ICML 2023.", "claims_and_evidence": "Overall, the claims are supported by clear experimental results and theorem:\nTighter bounds under L2 perturbations: Empirical results (Table 1, Figure 3 and 4) show SDP-CROWN achieves significant verified accuracy improvement, outperforming baselines. \nScalability: Experiments on models with 65k neurons validate scalability.\nTheoretical tightness: Theorem 5.2 proves that in a special yet crucial case, the proposed bound can achieve an improvement by a factor of the square root of n.", "methods_and_evaluation_criteria": "The method is well-motivated for L2 robustness verification. Evaluation uses standard MNIST/CIFAR-10 benchmarks and models that are widely recognized in this field. It compares against relevant baselines (alpha-CROWN, alpha-beta-CROWN, LP-Full). The only aspect that may need further clarification is the baseline Naive_Lipschitz, which could benefit from a more detailed explanation.", "theoretical_claims": "I have reviewed the theorems in the main text and did not find any major issues.", "experimental_designs_or_analyses": "I have reviewed the experimental setup, and overall, it is valid. The only concern is that I am unsure whether the chosen radius for L2-norm perturbation robustness evaluation is reasonable.", "relation_to_broader_scientific_literature": "The work effectively bridges bound propagation-based verification and SDP technique. It aims to verify model robustness under L2-norm perturbation and thus related to neural network security.", "essential_references_not_discussed": "While I keep up with the literature on neural network verification, particularly the CROWN series, my understanding of SDP-based and Lipschitz-based verification is rather limited. Therefore, my main concern is whether more advanced methods exist, as the evaluation only considers a “naive” Lipschitz approach.", "other_strengths_and_weaknesses": "1. I appreciate Section 3 which clearly explains why and how the existing SOTA methods produce loose bounds under L2-norm perturbation.\n2. Both the theoretical analysis and empirical results demonstrate that the proposed method represents a valuable step forward in addressing this problem.", "other_comments_or_suggestions": "Typo: line 171 “lose” -> “loose”.", "questions_for_authors": "1. As I understand it, the core idea of this paper is that an L2-norm ball with the same radius is a subset of an L-infinity norm box, which allows existing bound propagation-based verification methods to be further tightened by focusing on L2-norm balls. The key improvement in this work lies in obtaining a tighter linear bias term h. My question is whether this idea is limited to refining the bias term h, or if it can also be extended to improve the slope term g for even tighter bounds.\n2. In the evaluation on MLP models and the MNIST dataset, the baseline BM exhibits superior performance (even approaching the upper bound given by PGD). However, I could not find an introduction to BM—did I overlook something?\n3. The selected baselines include alpha-CROWN and alpha-beta-CROWN. As I understand it, these existing CROWN-based tools directly verify L-infinity norm boxes rather than L2-norm balls under the current experimental setup. Would GCP-CROWN be inapplicable to this experiment? To my knowledge, GCP-CROWN has demonstrated stronger verification capabilities. Additionally, the Lipschitz-based baseline appears to exhibit a relatively favorable overhead. Are there more advanced methods in this category? A more detailed introduction to this baseline may also be necessary.\n4. Again, I am not very familiar with SDP-based verification techniques, so I had some confusion while reading Lines 120–135. According to the authors, U_i = u_i^2 and V_i = v_i^2, and the constructed matrix X_i being positive semidefinite seems to directly imply u_i v_i = 0. This appears to be an exact equivalence to ReLU activation—where is the relaxation incorporated in this formulation? Based on my understanding, the conditions U_i \\geq u_i and V_i \\geq v_i seem to make more sense.", "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:

Meta-review: This paper combines the two techniques: CROWN (linear bound propagation) and semi-definite programming based bound propagation. The claims are well supported both empirically and theoretically. The reviewers have provided details feedback on how to improve the related work section, which authors should take into account while preparing the final version.
Decision: Accept (spotlight poster)