Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization
Authors: Jianting Yang
Srecko Durasinovic
Jean B. Lasserre
Victor Magron
Jun Zhao
Venue: ICLR 2025 Poster (2025)
Keywords: Binary Neural Networks
Sparse Polynomial Optimization
Semidefinite Programming
Robustness Verification
Primary area: optimization

Abstract: This paper explores methods for verifying the properties of Binary Neural Networks (BNNs), focusing on robustness against adversarial attacks. Despite their lower computational and memory needs, BNNs, like their full-precision counterparts, are also sensitive to input perturbations. Established methods for solving this problem are predominantly based on Satisfiability Modulo Theories and Mixed-Integer Linear Programming techniques, which are characterized by NP complexity and often face scalability issues.
We introduce an alternative approach using Semidefinite Programming relaxations derived from sparse Polynomial Optimization. Our approach, compatible with continuous input space, not only mitigates numerical issues associated with floating-point calculations but also enhances verification scalability through the strategic use of tighter first-order semidefinite relaxations. We demonstrate the effectiveness of our method in verifying robustness against both $\||.|\|_\infty$ and $\||.|\|_2$-based adversarial attacks.

Published as a conference paper at ICLR 2025
VERIFYING PROPERTIES OF BINARY NEURAL NET- WORKS USING SPARSE POLYNOMIAL OPTIMIZATION
Jianting Yang
Srećko Durašinovic
Academy of Mathematics and Systems Science Chinese Academy of Sciences yangj i ant i n amss ac.
CNRS@ CURS@CREATE Singapore
CCDS, NTU Singapore
8 srecko001e @ee nt.. edu .g
Jean-Bernane Lasserre LAAS-CNK Toulouse School of Economics la lasserreel aas.
Victor Magron LAAS-CNRS
Jun Zhao
CCDS, NTU Singapore junzhao@ntu u. edu.
Université de Toulouse
vmagron& laas.
ABSTRACT
This paper explores methods for verifying the properties of Binary Neural Net- works (BNNs), focusing on robustness against adversarial attacks. Despite their lower computational and memory needs, BNNs, like their full-precision coun- terparts, are also sensitive to input perturbations. Established methods for solv- ing this problem predominantly based on Satisfiability Modulo Theories and Mixed-Integer Linear Programming techniques, which often face scalability is- We introduce alternative approach using Semidefinite Programming re- laxations derived from sparse Polynomial Optimization. Our approach, compat- ible with continuous input space, not only mitigates numerical issues associated with floating hoating-point calculations but also enhances verification scalability through the strategic use of tighter first-order semidefinite relaxations. We demonstrate the effectiveness of our method in verifying robustness against both |l and blased adversarial attacks.
INTRODUCTION
In the evolving landscape of machine learning, Binary Neural Networks (BNNs) have emerged as an intriguing class of neural networks since their introduction 2015 (Courbariaux et al.] 2015 Hubara et al.) 2016). The architectural simplicity and inherent advantages BNNs, such as reduced memory requirements and lower computational time, have garnered significant attention. As these networks have matured. they have been integrated into a wide range of machine learning applications (Rastegari et al. 2016;; Sun et al.) 2018 Xiang et al. 2017 Voraabi et al. [024]). For instance, BNNs are widely used in edge devices for tasks such as object detection, image recognition, and decision- making in resource-constrained environments, like autonomous delivery drones.
Despite their great approximation capacities, general deep neural networks are sensitive to input perturbations (Szegedy et al.] 2014 Antun et al.) (021). BNNs are not any different in this re- gard. Indeed, quantized or binarized networks do not necessarily preserve the properties satisfied by their real-precision counterparts (Galloway et al., 2018 Giacobbe et al. 2020). BNN-controlled autonomous delivery drones, for example, might encounter adversarial environmental conditions, such lighting variations, weather disturbances. Failing robustly classify objects under these altered environmental conditions could lead to a collision, endangering people or property. That is why verifying their robustness is of the crucial aspects of their design and deployment. A classi- fying network is said to be robust to adversarial attacks if small input perturbations do not cause any misclassifications. Formally speaking, the network verification consists of finding a point æ satisfy- ing P(æ) A Q(BNN(a)), where P is a pre-condition on Ø, e.g., stating a valid input perturbation, and Q post-condition on y BNN (z), e.g., stating an (undesirable) alteration of the highest output score. If both properties hold for some x. the network is not robust.
"Jinnting Yang was mainly affiliated with CNRS CREATE Singapore during the completion of this paper.

---

Published as a conference paper at ICLR 2025
Compared to much research on the robustness verification of full-precision networks, verification of BNNs is a question yet to be addressed with more attention. Moreover, many formal verifica- tion frameworks do not exploit the bit-precise semantics of BNNs (Giacobbe et al. (020), and in parallel, those BNN-specific approaches for robustness verification often suffer from limited scala- bility (Lazarus & Kochenderter [022] Narodytska al., 2020). Two related methodological axes can be identified. Firstly, methods based on Satisfiability Modulo Theories (SAT/SMT), as in Amir al. (202T); Jia Rinard (2020a); Narodytska al. (2018) 2020), encode the BNN verification problem into Boolean formula satisfiability, and leverage modern off-the- solvers to prove ro- bustness or find counterexamples. Secondly, Khalil et al. (2019); Lazarus & Kochenderfer (2022) cast robustness verification
Mixed Integer Linear Programming (MILP) optimization problem. Both approaches belong to the group of exact verification methods, i.e., they are sound and com- plete. In this paper, instead of solving the BNN verification problem exactly, we rather examine it through the lens (Sparse) Polynomial Optimization Problems (POP) (Lasserre, 2015 Magron & Wang 2023), that can be approximated with hierarchies of relaxations based Semidefinite Programming (SDP). Recent frameworks (Chen et al.] 20200] 2021 Latorre et al., 2020) Newton & P'apachristodoulou 2023) have demonstrated that sparse variants of SDP hierarchies could certify the robustness of full-precision ReLU neural networks, by efficiently providing accurate bounds for the associated optimization problems.
1.1 CONTRIBUTION
We exploit the semi-algehraic nature of the sign activation function to encode the BNN verifi- cation problem as a POP. We then solve the resulting first-order SDP relaxation of this POP to obtain lower bounds that can certify robustness. In addition, our method overcomes floating- point-related numerical issues that typically compromise the branch and bound process of MILP solvers. To the best of our knowledge, this is the first 3DPeb method for BNN verification.
From the theoretical point of view, we prove that adding tautologies (redundant constraints) to the initial POP encoding leads to first-order SDP relaxations with highly improved accuracy. Know- ing that higher-order SDP relaxations quickly become intractable for high-dimensional problems, designing tighter first-order SDP relaxations that exploit the structure of the network is crucial for enhancing the scalability of the method. We show that our bounds can be up to 55% more accurate than those derived from the linear relaxations typically used in traditional MILP algorithms.
We demonstrate the effectiveness of our method, compatible with continuous input space, in verifying robustness against both ll and ll-ll--based adversarial attacks, the latter being much less studied in the BNN verification literature. Our experimental results indicate that, for || and I|-112 robustness verification problems, our algorithm provide an average speedup of 4.5 and 11.4 times, respectively. For some severe attacks, the speedup exceeds a factor of 50.
1.2 RELATED WORKS
General verification methods: Neural network verification has been extensively studied in recent years. Optimization solvers based on works of Xu et al. (202I): Wang et al. (2021b) integrate bound propagation with efficient gradient computations, achieving state-of-the-art performance verification using abstract domain representations has been explored in Lopez al. (2023). while enhanced abstract interpretation approach has been recently implemented in PYRAT (Lemesle et al. 2024). Verification via MILP formulations has been investigated in Katz al. (201)). Sampling- based approach has been introduced in Li et al.
multiple benchmarks. Reachability-
2022). An overview of established verification techniques is available in Liu et al. (20TT).
SDP-based verification methods: Certifying adversarial robustness using SDP relaxations has been first proposed in |Raghunathan al.] (20T8). Tightening of the SDP bounds via linear reformulations and quadratic constraints has been proposed in |Fazlyab et al. (2020); |Batten et al.) (202]); Lan et al. (2022). Verification can also be tackled by computing upper bounds of Lipschitz constants (Fazlyab et al.) 2019 Latorre et al. 2020; Chen et al., 2020). Chordal and correlative
sparsity can be exploited (Anton et al. 20224) Newton & Papachristodoulou 2023; Chen et al,, 2021] to design more efficient SDP relaxations. The first-order dual SDP approach developed in
Dathathri et al. (200)) enables efficient verification of high-din digh-dimensional models. Note that these approaches have been mainly designed verify standard full-precision ReL.U networks.
2

---

Published as a conference paper at ICLR 2025
BNN verification: Binarized weights and activation functions allow for the BNN verifica- tion problem to be exactly encoded into Boolean expression. However, solving the resulting encoding via SAT solvers is usually quite computationally expensive as the number of involved variables grows very fast with the network size (Narodytska et al. 2018] Narodytska 2018)_ Consequently, only small and medium-sized networks can be handled within this framework. In order improve the scalability, different architectural and training choices have been proposed: inducing sparse weight matrices, achieving neuron stabilization via input bound propagation, direct search instead of unguided jumps for clause-conflict resolution (Narodytska et al. (020), enforcing sparse patterns to increase the number of shared computations, neuron-factoring (Narodytska et al. 2020 Cheng et al. 2018). The SAT solver proposed in Jia & Rinard (2020a (b) is tailored for BNN verification. By efficienlly handling reified cardinality constraints and exploiting balanced weight sparsification, this solver could achieve significantly faster verification on large networks. The SMT-based framework from et al. (202T) extends the well-known Reluplex (Katz et al. 2017) framework to support binary activation functions. Notice that these works are either incompatible with continuous input data are restricted to I1- perturbations. In contrast, our approach does not require an extra input quantization step and is compatible with more general perturbation
regions, including the one defined by the ||-1/2 norm.
The sole nature of BNNs makes them convenient for being directly represented via linear inequal- ities and binary variables, enabling the verification problem to be cast as MILP. These properties are exploited in Khalil et al. (2019), where big-M constraints model the neuron activations, and a heuristic named rorop decomposes the original problem into smaller MILP problems. However, the Mig-M approach is also well-known to be sensitive to the M parameter (Gurobi Optimization, LLC). Improved bounds for each neuron have been proposed by |Han & Goméz (2021) that lead to tighter relaxations, but only on medium-sized networks. This suggests that BNNs might also suffer from convex relaxation barrier for tight verification (Salman et al,) 2019). Another MILP-based approach has been discussed in Lazarus & Kochenderfer (2022); Lazarus al. (May, 2022), where both in- put and output domain of a property to be verified are restricted to polytopes. The set-reachability method from Ivashchenko et al. (2023) extends the star set and Image star approaches from Bak & Duggirala ( Tran et al. (2019) 2020). Unlike most other methods, it allows the input space to be continuous. However, our experiments highlight the intrinsic weaknesses of LP relaxations for BNN verification, negatively influencing the bounding step of MILP solving. We argue that SDP bounds would be able to provide significant speedups these exact solvers, especially for larger networks and more severe attacks. Somewhat related works concern quantitative BNN verification, where one tries to estimate how often a given network satisfies or violates some property. In [Baluta et al. (2019): Narodytska et al. (2019), quantitative robustness verification is reduced into model counting problem over a Conjunctive Normal Form (CNF) expression. SAT-based approaches are derived from either (Ordered) Binary or Sentential Decision Diagrams in Shi et al. (2020); Shih et al. (2019) Zhang et al. (2021).
(
1.3 NOTATIONS AND PRELIMINARIES
We use Roman letters to denote scalars, and boldfaced letters to represent vectors and matrices. If A is a matrix, then A (A..) denotes its k-th row vector, and || denotes its Frobenius norm. The entry j of a vector x (or x.) is denoted by æ, (or 2.,)). The Hadamard product is denoted by O, i... (A @ B))))) = A(.)) (a.)). For any p q matrix A, (v)A) is p-dimensional column vector whose k-th coordinate is given by [|A(k.:)]i.
The ring of n-variate real polynomials (resp. of most degree d) is denoted by R [[x] (resp. RR [x))). Let [[x] be the cone of multivariate Sum Of Squares (SOS) polynomials and E[x]a == Σ |z) n R[xx2a- By (ar, y) Σ JaAh we denote the standard inner product of vectors æ, y E R². If
ki, k2 E N with k < k2, then [k], ka] := (KI...., f2). Let [1].1( be the ||.l|-ball of radius centered &. We denote by ST. the set of symmetric positive semidefinite matrices of size n. We G where Da := (1, (1,01...... ......... .....,, Fn. ..., an) is the vector of monomials of degree at most d with size s(d) = (n+d).
recall that f E R[x]22 za is SOS if and only if positive semidefinite matrix G satisfies
Definition 1.1. Let ge == (g))jen. ml and h = (ha)kefL,q denote familless of polynomial functions. functioon
For [1, m.. k [1, 1], define dz == [deg(g;) (o/) and de deg(ha). Then, the d- d-truncated
3

---

Published as a conference paper at ICLR 2025
quadratic module Qa(g) generated by g, and the d-truncated ideal Ia(h) generated by h are
Qa(g)=
999 oo Elæla, E E[z)a-d,, E [1, [1,m] ml J:
(I)
Ia(h)= thela the [R(arlaadd k [1,
2 MAIN INGREDIENTS
2.1 BINARY NEURAL NETWORKS
Let L 2 be the number of hidden layers of classifying BNN, with layer widths being given by (No, "I....,, A1,,,,, (I++1) E N where no and n1.+1 are input and output dimensions. feed-forward BNN a mapping from the input region Rig C Ro to the output set [1, ( i] realized via successive compositions of several internal blocks (B) L)....... and an output block Bg:
BNN Reo 11,
2o BNN( == argmax (Bo (B) (xo)))))
For any i [[,, L], the internal block B, implements successively three different operations: affine transformation, batch normalization and point-wise binarization, that its output vector, denoted by 2,, belongs to { {-1,1)"* These operations are described by set of trainable parameters:
( wy1411, bli+1)
11-,,,, x R"
(4)
(710) ,ig1 1al
2.14)
E (R"1)*
(5)
ie[1.A]
Consequently, the output of a neuron
E
[1, nill from the hidden layer [[1 L] is given by
Zi = sign (wlil
Gra me +)+ 19)
3 with small enough & > 0. The output block B,
Vaz /13.144
applies a softmax transformation to the affinely-transfommed outputs of the last hidden layer, i.e., for each j E [1, ml+lI IL+1J
exp(z,)
where 2j = 1/.-1] x æ1
[!++1]
L exp(=))
(3)
In BNNs, replacing vector-matrix multiplications with simpler 1-bit XNOR-count operations comes cost: the sign function prevents effective (adversarial) training due the lack of proper gradi- ent information. However, promising framework for training BNNs via automatic differentiation was recently introduced in Assman et al. (A2024). For comprehensive analysis and the latest advancements in training (robust) BNNs, see Qin et al. (2020); Yuan & Agaian (202T).
2.2 PROBLEM FORMULATION
Casting BNN verification as an optimization problem requires using an appropriate representation of the non-linear sign(-) activation function. For any b) RR?, we have:
sign(b) a² 0, and ab 0.
(6)
This motivates the introduction of sequence of vector-valued functions (h,, 9:) such that
h,(x;) 2; 2; 1=0. x;-1) (1,, x; (W w._1 ( + bb.)) 2 0, (7b)
(7a)
x: : sign xr + Bla)
(
[b]]] nv (Wll), for each k [1, nu:]. This assumption eliminates the case in which some neurons are either always or never activated, since such neurons have no impact
where 1
R satisfies
Since hatch normalization can he understood as another affine transformation, it can be omitted throughout the technical modeling part, without loss of generality.
4

---

Published as a conference paper at ICLR 2025
on the verification process. Furthermore, suppose that the input perturbation region B C R Ro
can be encoded via positivity conditions on (at most quadratic) polynomials 2g + 9 (T)). For
example, In (2o) (e Σ- œo) @ (E + æo) corrssonnds to B Bi1-11 (z, a E Rng. Finally, the standard form BNN verification problems studied here are:
(E,E), E), where
min f(zo: 21...., .L..
(8a)
s.t. h((m;) = 0, i [1, L]. (0 2 0, i [1, gB( 2 0,
(8b)
T
(8c)
(8d)
where f is either a linear or quadratic function.
Remark 2.1 (Adversarial attacks). Given some point 5 E Rno whose true label is ij E [1, R1+1].
we define k-targeted attack be any allowed perturbation Dg satisfying (8b) &d for which the oulput of the network is le + V. If the network is robust, then
(8b)-188
gadv (Z., (2.,, , ..,...,,LL)- FL)
(w/l (5.)
wil+!]] (k..) LL + b [1++1]
by [[+1]]
always positive. Notice that f is an affine mapping of the neurons from the last hidden layer. Our framework is suitable for verifying properties of BNNS other than adversarial robustness (e.g. certain properties describing the ACAS-Xt controller from et (2017, or energy conservation in dynamical systems (Qin et al. (2019).. Verification against non-targeted attacks could be achieved via a simple objective function modification.
2.3 SPARSE POLYNOMIAL OPTIMIZATION
Notice that (8) is an instance of Quadratically Constrained Quadratic Programming (QCQP), in- volving : Ei=n ni decision variables and m := 2' n, + nB constraints, where n is the number of polynomials (at most quadratic) needed to represent the input region B. As such, problem (8) is a special case of Polynomial Optimization since one minimizes polyno- mial if over feasible set S defined with finitely many polynomial (in)equality constraints. Here fa= (x) 2 0, h;(x)) = 0, Vi E [1, LI, ( 2 0). Note that an equivalent characteriza- tion of the global infimum of f on S is r = mnnn[((r) x E S) max E IR f- 2 0 on S). This requires one to efficiently handle the set of polynomials that are nonnegative on S, which is known to be intractable. However, in practice, we rely on its tractable inner approximations based on weighted combinations of elements in == (gg))ee 9B), the weights being SOS polynomials.
By (Lasserre 2001 Theorem 4.2), ," = supfA E E -- a E Qa(g)) defines a hierarchy of dense SDP relaxations whose size increases with the relaxation order d, and such that 7d 1 as d + +oo. Moreover, the convergence towards T is generically finite, which means that d T for some d N Nie 2014 Theorem 1.1).
Example 2.1. Consider a BNN with L = 2, (no, n1, 72, na) = (3, 2, with trainable param-
eters given by (Will, W 3 =
(
-1 1
() (= - )) (= 1 )) and
-1 1
-1
(6 UPI [3)
1.5
1
: ) Suppose gn (an) = 0.22 (xo (80-->)
x)) T
2
-0.5
2). with æ (0, 0.5, O)T. The network assigns the label ū since 23,2 > 03,1 -2, By
Remark 2.1 the affine objective function to minimize becomes + peal (x: (11322 2222 +
22. D2.2 1+2) 2x 1. The corresponding dense SDP relaxation of order d 2 becomes
sup
A
G.G. Go.GE padv
s.t.
- -0
(10a)
7d
2
G.va + o = o=
Σ Giy + + Gnuannu
(10b)
111=1
GB, E (s((d-1)
..j E [1, 21, Go E st(()
(10c)
5

---

Published as a conference paper at ICLR 2025
checking for membership in Ia([h1, h22) ) in the line (0aa) boils down to imposing linear conditions on the coefficients of the involved polynomials. Those can be obtained after applying the substitution rules (z; =
In addition SDP conditions from (10c).
x for E [[]
For fixed relaxation order d, dense SDP relaxations involve ((n22) equality constraints, which prevents them from being applied to large-scale problems, However, many POP problems, including BNN robustness verification, exhibit important structural sparsity properties, which enables one to build significantly more computationally efficient SDP relaxations (Waki et al. 2006] [Wang et al.) 2021ap. For instance, let us suppose that [1, r =: To = - 1s with Ia not necessarily disjoint. To every subset 4 we can associate a subset of decision variables æT, == (ar, E [x). An instance of the BNN robustness verification problem of the form (8) exhibits correlative sparsity since
There exist (ff)Re().n . such that f = Ei fu. with fo E R[
The polynomials g can be split into disjoints sets JR, such that gi(:); E Ju if and only if g.(:), 1. Moreover, In E Ja for & E [1, pl. Since h.(-), only depends æi.j. the overall sparsity structure is induced by inequality constraints that mimic the cascading BNN structure.
As in the dense case, a hierarchy of correlatively sparse SDP relaxations given by Tes == sup(A E > Oh Ia(h), 0% (-((g:()) E Ja))}. Under additional ball constraints Magron & Wang 2023 Assumption 3.1), one still has 7 f - +oo. If = max [x), then these sparse relaxations involve (ppp2d) equality constraints, yielding a significant improvement when o < n. Apart from this computational gain, we will benefit from the fact that the first- order sparse relaxation is not conservative with respect to the dense one, meaning that T 7 Vandenberghe et al. 2015 Theorem 9.2).
R
COMPARISON OF LINEAR PROGRAMMING (LP) AND SDP BOUNDS
Here, we assume that f is linear, e.g., the function fadd defined in The goal of this section to compare LP and SDP relaxations of the QCQP encoding (8). when the perturbation region is
S S + Ø Let 2 2, w E 111,,1), and b E IR satisfying [b] < n. As pointed out by Amir et al. (2021) an equivalent linear approximation
described by B = |1-1 (Ø, =) for 2
of the {(x 3) [- 1]"h x {-1, 13, y sign (w, a 6)} given by
2 (x. w) + b) n +
1, y S ((x, w) + +6) b
(2, E 1- 1 x xf {-1, Hence, for each layer E [[1, L].
(11)
replace the quadratic function gi by two linear functions
( (m;;, 11-1) = (nv(W b(0) @ (æ: + 1) [ - + bb
(12a)
G.Ln (x,, x1-1) (nv(w/)) (0) o (1 xx) + W 2 + b14]
(12b)
Thus, by encoding the sign(.) function described in (2ab 12b the standard BNN verification
problem can be equivalently formulated as an instance MILP.
min f(Z0: ,1,...,,11) z.
20 #o..F......
s.t.
( (t,,
(w,,
0, E [1, L],
(13a)
MIILP
G.LIN (Ii, xb-1)
0, E L],
(13b)
gB ( 2 0,
(13c)
a; E (11,1)]m i [1, T.].
(13d)
By further relaxing the binary constraints in 13db via o G = corresponding L.P relaxation of the MILP problem in 13
-x Dy + 1), we can derive the
min
[ x 01,...... 231.)
....
TLP ==
s.t.
P.LIN (x.) 2 0,1 E [1, LJ.
(14a)
13a
13c
(14b)
'Replacing the initial sign constraint by gi,L and of provides valid encoding only if 20 [-1, However, it always possible to transform the input perturbation region that corresponds to Bij-ii 1).

---

Published as a conference paper at ICLR 2025
Notice that always have TLP I TMILP
Remark 3.1 (Encoding of sign(-)). In Lazarus Kochenderfer (2022; Khalil et al. (2019). the authors have also considered MILP encoding of the BNN verification problem, based I, E IR such that v (x, w) + b S u and
4 ((x, w) +b 3 y and y 2 -
4 (1,,,,, ((r,,)) b) +1.
y sar w)
(15)
u
For w
1 and n +n b, we conclude that 11 provides a tighter bound than 75) because
4 n ((x, w) b) - 3) = - (n 1 ((x, w) +b 1 +
2
wRta)
(16)
+
Theorem 3.1. For an arbitrary BNN with depth L 2 2, there always exists an affine function f: IR [ro .1..... F. R such that TLP > Tes-
Sketch of proof. Consider fZo. 21,..., σL) 9 LIN (ZL, Fz-1)y for some E [1. nz]. Then
Appendix A. explicitly constructs a feasible solution to the dual of the sparse first-order SDP re-
laxation of (8 yielding the value of the objective function equal 11, implying Td. 7 < -1.
Since l( (oo 21 .1.... Ct.) 2 O is one of the constraints in 14), we deduce that T.P 2 0.
Theorem 3.1 states that the lower bound 71 generally not competitive.
other hand, the inequality 2 TTPP is derived in Appendix A.2 but the second-order SDP relaxation remains computationally inefficient for high-dimensional problems.
4 TIGHTENING OF THE FIRST-ORDER SDP RELAXATION
The goal of this section to propose a more accurate first-order SDP relaxation. We still assume that B B111-I1-. (z) Firstly, notice that the semi-algebraic representation of the subgradient of the ReLU function derived in (Chen et al., 2020, Section 1.3) provides an additional way of exactly encoding the sign(-) function using quadratic polynomials. Consequently, for each i E [1, LJ, let us replace the constraint defined in (7b) by the following two constraints:
gl (z, v = (a: 1) C [ -1 + b(t)
2 0,
(17a)
of (.,, (- (a: 1) Ø [ -; + b(0) 2 0.
(17b)
Furthermore, we include the following redundant quadratic constraints (tautologies):
g (x 11-) = (z; + 1) nv (wlt) W x 2
(18a)
jf (r, 0i = (1 (1=x;) o (uv (wlk) + Wib 2 0,
(18b)
which hold true for æ:-1 1-1,1 and W S nv (Wil), where understood component-wise
should be
Hence, we get an alternative POP encoding of the BNN verification problem:
min f(Fo, F1,..., .I) 2o.21....223
s.t. (x,))) = [1, LJ.
(19a)
Ttighter
g (Ii, .1 1) 2 0, :. (æi, z; 0, i [1, L],
(19b)
d (mi 11 2 gf (æ,, 0;-1) 0, i [],
(19c)
nn (xn) 2 0,
(19d)
and corresponding dense and sparse hierarchies of SDP relaxations, i.e., (Teighter )a and (nd Lighter,ca
Theorem 4.1. For any BNN verification problem, Tighter,cs = Tighter 2 T!. If L 2 2, there exists an affine such that the inequality is strict. We also have T_ tighterr,s 2 TLP for any affine.
7

---

Published as a conference paper at ICLR 2025
Theorem 4.1 asserts that adding tautologies (18a) and (8b) is crucial, they allow to generate
a larger first-order quadratic module and consequently enable more accurate SOS decompositions. See Appendix A.3 for the proof and experimental illustration.
Illustration for the case L = (refer to Appendix A.4 for the general case): Generally, the BNN structure allows of size R2 + 1. Those subsets are given by I {01,1,.... 2i,n Fo,k) for E [o] and
decompose the problem by considering no + n2 subsets of variables, each
Inoth = f.1,1...... 21,M 22 for l E [[1 nel.
20,1
1.1
22
33,1
20,
1.2
2,
33
20.3
Figure 1: A toy BNN with L and (no: n1, 122, 12,, 2,,
The subsets of interacting
variables 11 -1,,, F1,,1211 red polygons) and (12, 22,1 1. (12,1, 222) (represented by blue polygons) used to compute "iighter,es"
(1.2) 13 = (20.3, 21 æ1,2) (represented by
For the BNN from Example 2.1 depicted Figure most SOS multipliers are non-negative reals when d = 1. With g: ( g g. 9.th the tighter first-order sparse SDP relaxation writes:
sup
A
s.t. fidv x - o E (h),
(20a)
2
5 (o 2 Og(a,, +
tiighter.cs
o(x) = Σ Σ
Σ 00, (B) (20b)
1=1 gEa:
k=
0o, (x1,) di (z G G2 E s 11lt1
& [1,
(20c)
og 0. g E [1, 2].
σB 2 0.
(20d)
NUMERICAL EXPERIMENTS
In this section, we provide numerical results for BNN robustness verification problems with respect different perturbations. All experiments are run on a desktop with a 12-core i7-12700 2.10 GHz CPU and 32GB of RAM. The tightened first-order sparse SDP relaxation is modeled with TSSOS (Magron& Wang 202T) and solved with Mosek (Andersen & Andersen, 2000). Gurobi (Gurobi Op- timization, LLC. 2023) is used to solve MILP. BNNs were trained on standard benchmark datasets,
using Larq Geiger & Team (2020). The full experimental setup detailed in Appendix B
5.1 ROBUSTNESS AGAINST ||-1 ATTACKS
MNIST dataset used to train two sparse networks BNN, and BNN2, where sparsity refers to
weights sparsity defined by W, 1-Σ [ We assess the performance of method
Ee R,0;11 (number of solved cases (cert.) and verification time t (s)) in verifying robustness of the first 100 images from the test set. Obtained results, see Table are compared with both LP (14) and MILP
13 methods, where the latter was converted into an easier, attack feasibility problem by adding T0 < 0 to the constraint set.
Notice that, unlike in Newton & Papachristodoulouu 2023)). the presented structure of decision variables subsets dependent the input size no. which enhances its computational efficiency.
8

---

Published as a conference paper at ICLR 2025
Our method is average 15.75% (for BNN1) and 25.67% (for BNN₂) less conservative than the LP-based method. Moreover, larger input regions do not significanlly affect performance, com- pared to MILP, where the impact running time is much more severe. This is partially due to the coarseness of I.P bounds, see Figure 2 and is even more prominent for densely connected networks.
Table I: Performance comparison for different models and input regions, given by d||l1 127.25 .5c (data were scaled to [-1, 1]74), We use to separate the number of robust and robust instances, within a time limitation of 600 s. The runtime parentheses refers to the average runtime over the instances that method verified successfully.
non-
Model
611 lo
tighter,es & (()
TSoft-MILP
cert.
t (s)
cert.
cert.
{s)
BNN1: [784, 500, 500, 10]
0.25
83
0.01
91
3.62 (3.58)
3 3195
0.04 (0,04)
0.50
0.02
60
6.69 (6.50)
4194
1.21 (0.06)
1.00
1
0.03
21
10.76 (8.22)
15 500
251.90 (1.37)
W² 34.34%
1.50
0.06
6
38.32 (26.99)
20 12
428.24 (191.95)
BNN2:
0.25
14
0.03
59
11.97 (10.64)
3195
2.23 (0.69)
774,, 500, 500, 10]
0.50
0
0.05
23
42.37 (24.21)
9
220.53 (13.24)
W. 19.07%
0.75
0
0.08
9
139.18 (52.01)
10 19
455.61 (186.54)
Figure 2: Comparing TLP and nighter,,s bounds for BNN, and different 6 1o0 Each subplot x- axis represents indices of test set images sorted in the descending order of Tighter,es values. The upper bound ub is obtained by random sampling. The relative improvement over LP is estimated through ub
On average, Fighhter,ss bounds are 21, 33, 46 and 53 percent more accurate,
respectively.
100
Computed bound
0
-100
-200
-300
Tagasar
11.11000
0.6
100
Computed bound
Min M
-100
-200
ub
-300
611:110
1.0
51111
1.5
Additional experimental results on ||oo robustness verification on CIFAR-10 data set are presented
Appendix Table g
The discontinuity of the sign(-) activation function can exacerbate floating-poin errors, leading to significant numerical inaccuracies in the MILP solving process. For instance, if node's value after linear transforattinns is -1.9 10 assigning the value -1 to this node unreliable, as floating-por poiing errors could easily flip the sign. Such incorrect sign values critically affect the feasibility of the solution and the overall bound. To
SDP methods provide trusted bounds:

---

Published as a conference paper at ICLR 2025
address this, introduce margin of 10-7 for sign determination, which call Soft-MILP. In contrast, for the SDP-based method, we can easily enclose the errors with interval arithmetic as in (Magron et al. 2013] Section 2.2), to obtain rigorously valid lower bound.
5.2 ROBUSTNESS AGAINST |1-1/2 ATTACKS
We replace the constraint 13c with 9B such that B = B11-112 (ã.E) n |-1, The resulting Mixed Integer Non-Linear Programming (MINP) problem, also solved using Gurobi, and its optimal value are referred to TSoft MINP-
Table 2: Performance comparison for ||..||2verifiaationn where ò11.11a 255c.
||-1|a
tighter.os t {s)
TSoft-MINP
cert.
cert.
(s)
BNN
[784, 500, 500,
10). w,
34.34%
10
70
5.23 (5.02)
3 93
33.35 (5.75)
20
36
19.54 (15.20)
4 30
447.11 (278.38)
30
13
34.24 (18.08)
4 6
556.07 (467.16)
BNN₂
[784, 500, 500, 10] w,
19.07%
5
81
8.57 (8.50)
2 96
3.31 (1.18)
10
46
19.00 (15,44)
3 58
272.92 (106.25)
15
27
63.21 (36.73)
4 23
475.78 (293.96)
As displayed in Table 2 when the perturbation region is small, the exact MINP method can verify more instances. However, for more severe attacks, method certifies robustness for almost the same number of instances, but 11.4 times faster on average (for more details, refer to Appendix B).
CONCLUSION AND FUTURE WORKS
In this work, we studied SDP relaxations associated with polynomial optimization problems to verify the properties of BNNs with continuous input space. We demonstrated the ability of method to verify robustness against both I|-I|s and ||-l|2 attacks. The proposed method efficiently exploits the inherent sparse structure of given BNN and generally provides much less conservative bounds than the LP-based method. Moreover, its running time does not scale exponentially with either the size of the network or the perturbation region.
Our method relies on the interior interior-point point SDP solvers, and thus inherits their limitations. One direction for future improvements could be based on the embedding of automatic differentiation either improve existing interior-point SDP solvers create new ones, like in Dathathri et al. (2020).
Moreover, our experimental results suggest that one could replace LP relaxations with SDP relax- ations in branch-and-boumnn
algorithms, such as the ones implemented in Gurobi. Based on our experiments, an alternative SDP-based relaxation embedded within general-purpor MILP/MINP solvers would significantly accelerate the exact verification process, especially for larger input perturbation regions.
Better bounding at comparable time cost could significantly improve the overall performance of such solvers, which another exciting topic of future research.
10

---

Published as a conference paper at ICLR 2025
ACKNOWLEDGMENTS
This work benefited from the HORRZON-MSCAA-023-D- der the Grant Agreement No 101 120296 (TENORS), the ANITI AI Cluster program under the Grant agreement n" ANR-23-IACL-0002 the Basic Science Center Program (No: 12288201) of the National Natural Science Foundation of China, the National Key R&D Program of China (2023YFA 1009401,, as well as the National Research Foundation, Prime Minister's Office, Sin- gapore under its Campus for Research Excellence and Technological Enterprise (CREATE) pro- gramme.
of the European Commission un-
REFERENCES
Guy Amir, Haoze Wu, Clark Barrett, and Guy Katz. An SMT-based approach for verifying binarized neural networks. In Tools and Algorithms for the Construction and Analysis of Systems, pp. 203- 222. Springer International Publishing, 2021. ISBN 978-3-030-72013-1
Erling D Andersen and Knud D Andersen. The MOSEK interior point optimizer for linear program- ming: implementation the homogeneous algorithm. In High performance optimization, pp. 197-232. Springer, 2000.
Xue Anton, Lars Lindemann, and Rajeev Alur. Chordal sparsity for SDP-based neural net- work verification. Automatica, 161:111487, 2024. ISSN 0005-1098 doi: https://doi.or//00
1016j.automatic.22233111113 URL https: //ww://ww.//////////////////tt sci encedi com sc ence/
arriclle//11/500011999005555
V. Antun, N.M. Gottschling, A.C Hansen, and B. Adcok. Deep learning in scientific computing: Understanding the instability mystery. SIAM News, 54(2), 2021. March 01.
Johannes Aspman, Georgios Korpas, and Jakub Marecek. Taming binarized neural networks and mixed-integer programs. Proceedings of the AAAI Conference on Artificial Intelligence, 38(10); 10935-10943, Mar. A2024. doi: 10.160 00268........ URL Ittpp::/ /ttps:://oos..aas
AAAI http://eeeee.pp/aaaaaaaaaaa/cc//
Stanley Bak and Parasara Sridhar Duggirala. Simulation-cquivalles reachability of large linear sys- tems with inputs. In Computer Aided Verification, pp. 401-420, Cham, 2017. Springer Interna- tional Publishing. ISBN 978-3-319-63387-2
Teodora Baluta, Shiqi Shen, Shweta Shinde, Kuldeep S. Meel, and Prateek Saxena. Quantitative verification of neural networks and its security applications. CCS '19, pp. 1249-1264, New York, NY, USA, 2019. Association for Computing Machinery. ISBN 9781 4503674797 doi: 10.
114573319535.3354245. URL http::://....org//// wtt.:///.....1111111111111 3319933..335222665 3354245
Ben Batten, Panagiotis Kouvaros, Alessio Lomuscio, and Yang Zheng. Efficient neural network ver- ification via layer-based semidefinite relaxations and linear cuts. In Proceedings of the Thirtieth International Joins Conference on Artificial Intelligence, IJCAI-21, pp. 2184 2190. International Joint Conferences on Artificial Intelligence Organization, 2021. doi: 10.24963/rjcai.2222/3330 202/ai..222/311111
URL http::://ool.org/11...2
Tong Chen, J.-B Lasserre, Victor Magron, and Edouard Pauwels. Semialgebraic Optimization for Bounding Lipsehitz Constants of ReLU Networks. Proceeding of Advances Neural Information Processing Systems 33 (NeurIPS), 2020.
Tong Chen, J.-B Lasserre, Victor Magron, and Edouard Pauwels. Semialgebraic Representation of Monotone Deep Equilibrium Models and Applications to Certification. Proceeding of Advances in Neural Information Processing Systems 34 (NeurIPS), 2021.
Chih-Hong Cheng. Georg Nührenberg, Stung-Hao Huang, and Harald Ruess. Verification of bi- narized neural networks via inter-neuron factoring. In Verified Software. Theories, Tools, and Experiments, pp. 279-290. Springer International Publishing, 2018. ISBN 978-3-030-03592-11

---

Published as a conference paper at ICLR 2025
Matthieu Courbariaux, Yoshua Bengio, and Jean-Pierre David. BinaryConnect: Training deep neural networks with binary weights during propagations. In Advances in Neu-
ral Information Processing Systems, volume 28. Curran Associates, Inc., 2015. URL
neur haap://s.a..nnipssppppappperrrrr http://pprrrrrleeepeeeeeeeee http://ppppppppppppeeaee/e///a/a
3e [ac.
pdf
Sumanth Dathathri, Krishnamurthy Dvijotham, Alexey Kurakin, Aditi Raghunathan, Jonathan Uesato, Rudy R Bunel, Shreya Shankar. Jacob Steinhardt, Ian Goodfellow, Percy Liang, and Pushmeet Kohli. Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming. In Advances in Neural Information Processing Systems, volume 33, pp. 5318-5331. Curran Associates, Inc., 2020. URL https::/prroceednnss neur httpp/ppee..leeepppppeeeeeeeeeee B3/ocb/cc8c1102111e2222222222220
Paper. Paper.pdirrr..
Mahyar Fazlyab, Alexander Robey, Hamed Hassani, Manfred Morari, and George J. Pappas. Ef- ficient and accurate estimation of lipschitz constants for deep neural networks. In Proceedings of the 33rd International Conference Neural Information Processing Systems, Red Hook, NY, USA, 2019, Curran Associates Inc.
Mahyar Fazlyab, Manfred Morari, and George Pappas. Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming. IEEE Transactions on Automatic Control, PP:1-1, 12 2020. doi: 10.10997AAC2200.3444191..
Angus Galloway, Graham W. Taylor, and Medhat Moussa. Attacking binarized neural networks. In International Conference Learning Representations, 2018. URLLhttps:/// httlhttttp:/oppeeeeieee
met/forou ddt.mnid--HHKP22-2
Lukas Geiger and Plumerai Team. Larq: An open-source library for training binarized neural net-
works. Journal of Open Source Software, 5(45):1746, 2020. doi: 10.21105/joss.11456 011444 URL
https://doo /ttp:://doi.or//// www.ooo............ooooooo..o... 111....111//osss.. 01..01110 61746
Mirco Giacobbe, Thomas A. Henzinger, and Mathias Lechner. How many bits does it take to quantize your neural network? In Tools and Algorithms for the Construction and Analysis of Systems, pp. 79-97, Cham, 2020. Springer International Publishing. ISBN 978-3-030-45237777
Gurobi Optimization, LLC. Dealing with big-M constraints, ddocmentation httpr//oooeouueeeeeeeeeeee/eeale cessed: 17 May 2024.
com/
Ac-
Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual, 2023. URL https://wwk. gurobi. com
Shaoning Han and Andrés Goméz. Single-neuron convexification for binarized neural networks. Optimization Online, 2021. URL httts:://ptimizzatte
84197
Itay Hubara, Matthieu Courbariaux, Daniel Soudry, Ran El- Yaniv, and Yoshua Bengio. Binarized neural networks. In Advances in Neural Information Processing Systems, volume 29, Curran Associates, Inc., 2016. URL
hew.reeiiinnnnnnne..s......... nwwrips. wtw..nsssssss.cccpp.pp.... fttp:/papppffeesssseppppp
Mykhailo Ivashchenko, Sung Woo Choi, Luan Viet Nguyen, and Hoang-Dung Tran. Verifying binary neural networks on continuous input space using star reachability. In 2023 IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE), pp. 7- 17, 2023. doi: 10. 1090/ 2003.0009..
Kai Jia and Martin Rinard. Efficient exact verification of binarized neural networks. In Proceedings of the 34th International Conference on Neural Information Processing Systems, NIPS'20, Red Hook, NY, USA, 2020a. Curran Associates Inc. ISBN 9781713829546.
Kai Jia and Martin C. Rinard. Exploiting verified neural networks via floating point numerical error. 2020b. Ut/.itttsss./aaxx..ooo//aaabbbbp 03021
CoRR,
12

---

Published as a conference paper at ICLR 2025
Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In Computer Aided Verification, pp- 97-117, Cham, 2017. Springer International Publishing. ISBN 978-3-319-63387-9,
Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Alcksandar Zeljić, David L. Dill, Mykel J. Kochenderfer, and Clark Barrett. The marabou framework for verification and analysis of deep neural networks. In Isil Dillig and Serdar Tasiran (eds.). Computer Aided Verification, pp. 443 452, Cham, 2019.
Springer International Publishing. ISBN 978-3-030-22540-44
Elias B. Khalil, Amrita Gupta, and Bistra Dilkina. Combinatorial attacks on binarized neu- ral networks. In International Conference Learning Representations (ICLR), 2019. URL
https: /wwpvv/rxvvvv//. www.i.org//aa.......... 3ttg/abb//B11..3355
Diederik P. Kingma and Jimmy Ba. Adam:
method for stochastic optimization. CoRR, abs/1412.6980, 2014. URL https://app semanticscholar. wtt.::ooo......ooooooouo...uu. 6628106
Jianglin Lan, Yang Zheng, and Alessio Lomuscio. Tight neural network verification via semidefi- nite relaxations and linear reformulations. Proceedings of the AAAI Conference on Artificial Intelligence, volume 36, pp. 7272-7280, 2022.
Lasserre. Global Optimization with Polynomials and the Problem of Moments. SIAM Journal Optimizationn, 11(3):79-8817, 2001. doi: 10. 10.1137751055222403666699 URI. 1tt.:...11111011
ht https: /tt.:/...........1..030033333330
Bean-Bernard Lasserre. Convergent SDP-Relaxations Polynomial Optimization with Sparsity.
Siam Journal on Optimization, 17:263-277 01 2006. doi: 10. (0.1137/050645444.
Bean-Bernard Lasserre. An Introduction to Polynomial and Semi-Algebraic Optimization. Cambridge Texts in Applied Mathematics. Cambridge University Press, 2015. ISBN 9781316240397. URL
https://booke: gooq 1e. com htt..///ooooos..dpd.sa......
Fabian Latorre, Paul Rolland, and Volkan Cevher. Lipschitz constant estimation Neural Networks via sparse polynomial optimization. In International Conference on Learning Representations, 2020.
net./e/wweeeeeeeeeeeeeeeeeeeeeee httt:/fformmmdddrerere XSFDB
Christopher Lazarus and Mykel J. Kochenderfer. A mixed integer programming approach for verifying properties binarized neural networks. International Joint Conference on Artifi- cial Intelligence (IJCAI), AI Safery Workshop. 2022. doi: 1048550VaxXi22223.7777. URL
https: http:::///ooooggg////
1/550/arXiii www.ii.................. 07078
Christopher Lazarus, Mykel J. Kochenderfer, Stephen Boyd, and Mert Pilanci. Trustworthy machine learning by efficiently verifying compressed models. https://pnrLtaffoootllet///////9 May, 2022.
Augustin Lemesle, Julien Lehmann, and Tristan Le Gall. Neural network verification with PYRAT. arXiv, 2024. URL
23903
Renjue Li, Pengfei Yang, Cheng-Chao Huang. Youcheng Sun, Bai Xue, and Lijun Zhang. To- wards practical robustness analysis for dnns based on pac-model learning. In Proceedings of the 44th International Conference on Software Engineering, ICSE '22, pp. 2189-2201, New York, NY, USA, 2022. Association for Computing Machinery. ISBN 9781450392211. doi: http://1111115511111111 3510143
10.1145/35100033351000
Changliu Liu, Tomer Amon, Christopher Lazarus, Christopher Strong, Clark Barrett, and Mykel J. Kochenderfer. Algorithms for verifying deep neural networks. Now Fondations and Trends, 2021.
Diego Manzanas Lopez, Sung Woo Choi, Hoang- Dung Tran, and Taylor T. Johnson. Nnv 2.0: The neural network verification tool. In Constantin Enea and Akash Lal (eds.), Computer Aided Verification, pp. 397-412, Cham, 2023. Springer Nature Switzerland. ISBN 978-3-031-37703-7.
13

---

Published as a conference paper at ICLR 2025
Victor Magron and Jie Wang. TSSOS: Julia library to exploit sparsity for large-scale polyno-
mial optimization. ArXiv, abs/2103.00915, 2021.
org/CorpusIDI ID: 2:2==pu6S 230076082
Victor Magron and Jie Wang. Sparse Polynomial Optimization: Theory and Practice. Series on
Optimization and Its Applications. World Scientific (Europe), 2023, doi: 10.1142/00382. URL
https: /twp://wwwww.. wor wwt.:wowwddssenii..... com/ www.o///w/ab////ooooooocoooaaala 1112///002122222222
Victor Magron, Xavier Allamigeon, Stéphane Gaubert, and Benjamin Werner. Formal proofs for Nonlinear Optimization. Journal of Formalized Reasoning, 8(1):1-24, 2015.
Nina Narodytska. Formal analysis of deep binarized neural networks. In IJCAL, pp. 5692-5696, 2018.
Nina Narodytska, Shiva Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, and Toby Walsh. Verifying properties of binarized deep neural networks. Proceedings of the AAAI Conference on Artificial Intelligence, volume 32, 2018.
Nina Narodytska, Aditya Shrotri, Kuldeep S. Meel, Alexey Ignatiev, and Joao Marques-Sile SSllaa. As- sessing heuristic machine learning explanations with model counting. In Theory and Applications of Satisfiability Testing- SAT 2019, pp. 267-278, Cham, 2019. Springer International Publishing. ISBN 778-3-033--2225-9
Nina Narodytska, Hongce Zhang, Aarti Gupta, and Toby Walsh. In search for SAT-friendly bi- narized neural network architecture. In International Conference on Learming Representations, 2020. URL
net www.:nneee/oommmddd/eemm SJx 4F
Matthew Newton and Antonis Papachristodoullu. Sparse polynomial optimisation for neural net- work verification. Automatica, 11231,, 2023. ISSN 0005- 1098. doi: https:/doi.org//10
0016:aaattomaaica2223111133 URL http:///wwwwssceeeeeeeeee...... wtwp://wwwwneeeeteeoeeeeeeeeeeee articleep11/50001092233333
Jiawang Nie. Optimality conditions and finite convergence of Lasserre's hierarchy. Mathematical
programming, 146:97-121, 2014.
Chongli Qin, Krishnamurthy (Dj) Dvijotham, Brendan O' O'Donoghue, Rudy Bunel, Robert Stanforth, Sven Gowal, Jonathan Uesato, Grzegorz Swirszez, and Pushmeet Kohli. Verification of non-linear specifications for neural networks. In International Conference Learning Representations, 2019. URL
Haotong Qin, Ruihao Gong, Xianglong Liu, Xiao Bai, Jingkuan Song, and Nicu Sebe. Binary neural networks: A survey. Pattern Recognition, 105:107281 2020.
Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. Semidefinite relaxations for certifying robustness to adversarial examples. In Advances in Neural Information Processing Systems 31: Annual Conference tems 2018, NeurlPS 2018, December 3-8, 2018, Montréal, Canada, pp. 10900- 10910, 2018. URL https: http:::::///poreeedeggo nwwriie..ipp..... wwwpccppppp..eeecce 20aper/20110 8/hash/
Neural Information Processing Sys-
Abst htt.::/csssssa...sattttt..... html
Mohammad Rastegari. Vicente Ordonez, Joseph Redmon, and Ali Farhadi. XNOR-Net: ImageNet classification using binary convolutional neural networks. In Computer Vision - ECCV 2016, pp. 525-542, Cham, 2016. Springer International Publishing. ISBN 978-3-319-44493-00
Hadi Salman, Greg Yang. Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. con- vex relaxation barrier to tight robustness verification of neural networks. In Ad- vances in Neural Information Processing Systems, volume 32. Curran Associates, Inc.,
2019. URL. https:: wtw.::eeeennnn..e..e..eee...ee.. www.:eewwrireeeeeeeeeee ccppppr.rrcppppp..pppppppp httpl/ppprrfffepppppppeee files/paper/201111 Flee:66ac5544eeffFaaaaaaaaaaaaaa
Weijia Shi, Andy Shih, Adnan Darwiche, and Arthur Choi. On tractable representations of bi- nary neural networks. In International Conference Principles of Knowledge Representa- tion and Reasoning, 2020. URL https: app. www.nticscholeeeeee..... http:////.aaeemamnncsssoooo.rro htt.s//chh...aaaooooooooooooaoaa
21 214802814
14

---

Published as a conference paper at ICLR 2025
Andy Shih, Adnan Darwiche, and Arthur Choi. Verifying binarized neural networks by angluin-style learning. In Theory and Applications of Satisfiabilitty Testing- SAT 2019, pp. 354-370, Cham, 2019. Springer International Publishing. ISBN 978-3-030--2255-99
Siyang Sun, Yingjie Yin, Xingang Wang, De Xu, Wenqi Wu, and Qingyi Gu. Fast ob- ject detection based on binary deep convolution neural networks. CAAI Transactions Intelligence Technology, 3(4):191-177, 2018. doi: https///bblorr//001004/tttttt..t
1026. URL htttts::/iettreseerrreee on ineeeseaarc..ommmeeieieeeeee hiw.eiibrrry..lllee.co////aee wwl.ey..comddd//bb///1 049/trit.2013 1026.
Christian Szegedy, Wojeiech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian J. Goodfel- low, and Rob Fergus. Intriguing properties of neural networks. In 2nd International Conference on Learning Representations, ICLR 2014, Banff, AB, Canada, April 14-16, 2014, Conference Track Proceedings, 2014. URL /ttt::://aaaiii org/ abs/ 1////311.11 6199
Dung Tran, Diego Manzanas Lopez, Patrick Musau, Xiaodong Yang, Viet Luan, Luan Nguyen, Weiming Xiang, and Taylor Johnson. Star-based reachability analysis of deep neural networks. In 23rd International Symposium on Formal Methods, pp. 670-686, 2019.
Hoang-Dure Danng Tran, Stanley Bak, Weiming Xiang, and Taylor T. Johnson. Verification of Deep Convolutional Neural Networks Using ImageStars. In Computer Aided Verification, pp. 18-42, Cham, 2020. Springer International Publishing. ISBN
Lieven Vandenberghe, Martin S Andersen, et al. Chordal graphs and semidefinite optimization. Foundations and Trends@ in Optimization, 1(4):241-433, 2015.
Lorenzo Vorabbi, Davide Maltoni, and Stefano Santi. On-device learning with binary neural net- works. In Image Analysis and Processing ICIAP 2023 Workshops, pp. 39-50, Cham, 2024. Springer Nature Switzerland. ISBN 978-3-031-51102336
Hayato Waki, Sunyoung Kim, Masakazu Kojima, and Masakazu Muramatsu. Sums of Squares and Semidefinite Program Relaxations for Polynomial Optimization Problems with Structured Sparsity. SIAM Journal on Optimization, 17(1):218 242, 2006. doi: 10.1137/050623802 URL
https://doo .org////g....................... 10. www.1117000000
Jie Wang, Victor Magron, and Bernrd Lasserre. TSSOS: A Moment-SOS Hierarchy That Exploits Term Sparsity. SIAM Journal on Optimization, 31(1):30-55 58, 2021a. doi: 10.1137/ 19M1307871. URL htttp::///doto ooriiiorg//1... 100g///0.100 1137/1 9M1307871
Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and Zico Kolter. Beta- crown: efficient bound propagation with per-neuron split constraints for neural network robust- ness verification. In Proceedings of the 35th International Conference on Neural Information Processing Systems, NIPS '21, Red Hook, NY, USA, 2021b. Curran Associates Inc. ISBN 9781713845393.
Xu Xiang. Yanmin Qian, and Kai Yu. Binary deep neural networks for speech recog- nition. Interspeech 2017, 18th Annual Conference of the International Speech Com- munication Association, Stockholm, Sweden, August 20-24, 2017, pp. 533-537. ISCA, URL /ttp:::://o...og/1...2..22
2017. doi: 0.22437/INTERSPPECH227777
Interspeech. 2aneecchh.0171113
Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. International Conference Learning Represantations, 2021. doi: 10.
48550/arXiv..011..337
Chunyu Yuan and Sos S. Agaian. A comprehensive review of binary neural network. Artifi cial Intelligence Review, pp. 1-65, 2021. URL httph:ttt///t..t http::////.pi..smmatttscccccciee
CorpusID:23874430
Yedi Zhang, Zhe Zhao, Guangke Chen, Fu Song, and Taolue Chen. BDD4BNN: A BDD-based quantitative analysis framework for binarized neural networks. In Computer Aided Verification, pp. 175-200, Cham, 2021. Springer International Publishing. ISBN 978-3-030-81685--
15

---

Published as a conference paper at ICLR 2025
A THEORETICAL DISCUSSION
A. DUAL SIDE OF POLYNOMIAL OPTIMIZATION RELAXATIONS MOMENT HIERARCHIES
We have discussed computing a global minimum of multivariate polynomial using SDP relaxations obtained by interpreting the requirement for polynomials to be positive on sets defined with finitely many (in)equalities.
It is also possible to derive the corresponding dual relaxations. Notice that polynomial f in the variable x (#1:-. Fnd can also be written as f -n with A No and fa E I, where x 21 2n Then the moment hierarchy (Lasserre) 2001) for the POP introduced in
Section 2.3 corresponds to:
inf (f(
V/
s.t.
Ma(y) 2 0,
(21a)
Ma-1(9:(-jj9) 0, E [1. 4]. [1, ml]
(21b)
mom =
M M = = [1, L1.j e [1, n:],
(21c)
M. Ma-1(gB()44)) 0, [1. 1,
(21d)
(21e)
where y (aa)a is sequence indexed by a E N and Ly the linear functional defined by
f 1+400) := E
(22)
For N, Ma(y) denotes the moment matrix of order d associated with y and defined as follows
(a(y)( == L,, L,,(xx²)) = U34rs vB,7 E No.
(23)
Similarly, for = En x E [[xx], Ma(gy) denotes the localizing matrix of order associated with g and y. detined as follows
(3(gy)(,,1) 7) = Ly Luggxx' Dayattt4r v3, E N
(24)
When the correlative sparsity is present, analogous hierarchies sparse moment relaxations can be derived well (Lasserre 2006 Magron & Wang 2023). Such reasoning was adopted in the
following proof of Theorem 3.1
Proof of Theorem
3.7 Let j
[1, nr. and of nv(W(4)); + 6/² and define (
f 3 $1...., 01) = L..j - 2
((w
x LL-1
+ bb/ll) 1). Then,
(1:)*
w L
1
0
(1.)
M
L W
Will LL G.)
L4
(25)
m1-1
(3
(3:)
0
1
represents a feasible moment matrix for the sparse first-order moment relaxation of (8) yielding [4]
the value of the objective function equal to -1 (because || ll nv(w(4)),) implying that
< -1. However, since f Li...., xL) > 0 is one the constraints in 14). we deduce that TL 0.
As direct consequence of Theorem we have the following corollary:
Corollary A.1.1. Consider an arbitrary BNN with depth L 2 2, and let j [1, nz]. Then,
Og & (1(Hgu()))),
(26)
thus the set ( Ll g P.L.N i [1, m.} is not included in Q ((g),,... 99,99))
16

---

Published as a conference paper at ICLR 2025
A.2 BOUNDS FROM THE RECOND-ORDER RELAXATION
Theorem A.2.1. If (æn, 2i,..., x.. + [L ,I...., (.) Consequently, any dual-feasible solution of (14) yields valid SOS decomposition for the second- order SDP relaxation of (8).
is affine, we have T 2 72 2 T.P.
Proof of Theorem A.2./ We proceed by analyzing the feasible sets of each problem. Firstly, both problems share the same input perturbation region given by (13c). For the remaining constraints, let us consider three different cases:
(i) Single node bounds: Let i E [1. L] and E n.]. Then, the following equations on R[x:]] hold true:
( - 5/1 - (1.)) 1
2 (( and g. = (al + 1)² + _ he hz:))))) (27)
Thus {gL.LI, i E [1, L c Q2(1gr..... .L....)....g)....
(ii) Interaction between two adjacent hidden layers: Fix i E [2, L] and j E [I, n.]. Let us define
d1,- nv((ll)) // > 0. If we apply the substitution rules x;-1 x1-1 1 and 2ī, 1, then the following equations always hold true on ::
L.LLN (2;, (2t, Zi-1s-- (1 (1-zi.j) xi,))
gi gx
+ (1+ (1+221))
Dú.) )²
1 w bi]
(1,0) (i (28)
2
2
4c45
k=1
LinN(T, Fi-1s (1 )i.1)
g. gi x + (1 Fi.j (1-xij)
R4-1
1 w
(,)) ) (29)
2c-
Ac-jj
(1b)
k=1
Equations 28 and (9) certify that II RIINS i E [11 LD} C Oz(1gn.... gL. gL.9Bl).
(ii) Interaction between the inpul layer and the first hidden layer: For any j E [1, nı]. let us define ch. == uv uv(WWll), + =b41 0. It follows that
(i,,IN((1,,00), (1 )2
91 (300, æ1); + (1 + 21.5)
no (will)) (G.R)
w (.A))oo.)) (30)
20h
_c4-
1m
(1 + 111)2
91 (av, 2nly + (1 x )1,))
no
(willh) Gis)
+ W
(.)) -u.k) (31)
2c__
2c11
provide the Q2 (fgi(-);)) (0))))))-ae based representations for (), and L., valid after substituting æं,- 1.
Example A.2.1 (Illustration of Theorem A.2.1]. This theorem indicates that any dual-feasible solu- tion of (74 provides feasible solution for the second-order SOS relaxation (TO) of QCQP (8) For instance, let us consider the toy BNN from Example (2.1). Recall that we aim to minimize the linear function fadv (x)
2x2,2 1. Since the LP relaxation problem has following constraints:
1
4 o
+ 22
2
-x1,1 2 -1, 21,2 2 -1,
22, 2 -1,
(32)
3
3
3'
the expression
3
4x1,2
401,1
5
2
(2x2,2 1) 44
32.2
+
(- 11)
10
3
3
3
(33)
2
17
+ 5
(-21,2 + 1) +
(x2.2
+
1) 20
10
gives one feasible dual solution of the LP relaxation problem. From this dual solution, we can
recover the following SOS decomposition, certifying that fādv > 3:
(20:2.2 1)+ +)++. 4=
3
2
22222 1)
11,2 F1,
2
(1
+ 22 11. + m1.1)
10
3
2
1
2
17
1
+
(1 21.1)
+
(1 + x2
(1 + #,,2)
5 2
2
10
2
(34)
17

---

Published as a conference paper at ICLR 2025
A.3 IMPORTANCE OF TAUTOLOGIES
Proof of Theorem
4.1 Since all the variables are bounded, we have T tighter,cs = tighter Moreover,
the inequality tighter,ss 2 r! is consequence of the identity
1
9i g F.-1) 9 (1.: xt-1) 700 (2t, xi-1), E [2, LJ..
(35)
In order to prove that T
righter.es 2 TLP holds, we show that all linear functions g. P.INN e [1. T.J. involved in the constraints 13a and (13b) belong to ( ... .. J.. E [1, LJ)). We consider two different scenarios:
(i) Let i E [2, LI, j E [1, nzl and c == nv(W))) + b > 0. When we apply the
substitution rules 0; @ 04-1 and #i = 1, then the following equations always hold true on 1(2;:11
PLLNN (z,, 1111 = of (z 1)-s
gf (a;, 11-1)
(36)
Cts
ctd
1
D (ais 8i- ))j +
Di (mis Fb. 11;-1)j-
(37)
c-
(ii) Secondly, for any j E [1, m1], and c1. = nv (Wi(l + b1u
> 0. substituting o9, = yields
the following equalities on R[x0, æ1,5]: (IN =
1
1
Do)s g2(21, ool; + ( xo0j;
(38)
c.j
ctj
L.. vo); = gı (x), mo); + gi' (I1, zo)j
(39)
c
c+j
certifying that (2) mo), and ( belong (ig o g.1 0.. [1, LI}).
Finally, Theorem 3.1 implies that there exists an affine f such that T tighter.cs 2 TLP > 7!.
Remark A.3.1. We insist that tautologies (8a) and 188 are both important and necessary. If we consider the optimization problem without tautologies, where only ([7a) and (77b) are used to replace (b)). then we have the following strict containment relationship:
Q (g gh g.. E [1, L.)) & (igB Di."". of [1, Indeed, following the same reasoning as the proof of Theorem 3.1
(40)
we obtain that
#L-1
L.
will
Gi
M 1
aw!
l
w
tW (9:
(41)
(1))
(3:)
mi,
0
W
(3.))
[r.]
(bf1)) 2
with a = $/22 (nv(W14))))
2 Zav(Weel and v1 a² is a feasible moment matrix for
(6
(WI)))) which the value of the objective function is (W
1 (nv(Will),)
< 0. To
prove that M positive semidefiitt, we observe that M has a nn--1- ni-r--dimessoonl null space cor- responding to the direct sum of the sets A and B, where
A O)) E 1R
(W]4]] [L]
(G.)) 0) =].
(42)
B {a (-any(Wlo)), w
[ 6.9 -w | |aER]
18

---

Published as a conference paper at ICLR 2025
Thus, M has RL-1 eigenvalues equal to zero, and eigenvalue equal 1 corresponding to the eigenvector (-1, 0, a) Since the trace of M is nv nv(Wll)), + 2, we know that the maximal eigenvalue of M is nv(Wl())) +1
Details from the previous discussion can be summarized in the following corollary:
Corollary A.3.1. Let E [2, L] and j [1, ns]. If the substitution rule 2,. is applied on the space R. [x4 Fi.bb
gl.LN())s Q1
P (o.u())))))))))) (n,+i)).
(43)
Moreover, at least one of the polynomials defining the constraints from 17a--188 18b is not in (i(1) (.m))))))))))))))))))))))))))))) D.....n and consequently
(1((gr(),, (la
1.((). -. p. i [1. LJ).
(44)
Numerical experiments, simultaneously illustrating both scalability and bound superiority of "sghter,cs" are reported Table
Table 3: Behaviour of bounds from the first-order sparse relaxations on randomly generated ao- verification instances. Parameter represents row sparsity, i.e., the number of non-zero elements in each of the weight matrices rows, while "dense" indicates fully populated weight matrices. The relative TLP running time being significantly smaller, we omit it from the table.
Network size and sparsity
bound
(s)
tighter,cs
TOCQP
TLP
Fighhter.cs
TOCOP
[300, 100, 100], dense
-24.71
-78.64
-78,83
413.51
427.28
500, 100, 100], dense
-27.17
-78.58
-77.89
795.41
721.81
3300, 100, 100, 100), dense
-19.49
-77.06
-76.81
739.21
992.66
[500, 100, 100, 100). dense
-32.35
-82.35
-81.94
928.16
964.56
[1000, 100, 100, 100], dense
-26.19
-81.70
-81.32
1764.67
1659.13
300, 100, 100, 100, 100), dense
-30.58
-80.59
-80.42
966.76
1523.92
5500, 100, 100, 100, 100], dense
-16.19
-77.61
-77.25
1341.33
1498.51
10000, 100, 100, 100], dense
-1.31
-76.32
-75.89
1959.30
2237.44
300, 100, 100, 100, 100, 100), dense
-28.62
-80.95
-80.99
1012.18
1803.31
500, 100, 100,
100, 100 dense
-16.04
-78.10
-78.12
1255.16
1641.50
100, 100, 500, 100, 100],
100, 100), dense
-3.554
-83.93
-82.84
2225.89
2866.54
s 10
-80.84
-94.59
-98.16
12.53
14.90
800, 200].
10
181.52
194.96
198.97
218.72
186.77
1000, 100, 100],
s 10
-81.13
-94.72
.8.188
13.44
12.55
1000, 200, 200].
$
-174.13
192.79
198.61
243.87
191.24
1000, 300,300,,
10
-242.60
283.95
297.999
1203.41
1093.90
1000, 100, 100, 100), 8 10
-72.79
-92.88
99.788
69.70
77.63
1000, 100, 100, 100, 100), = 10
-8181
-9.300
98.30
327.83
319.04
1000, 500, 500], 5
476.01
-495.79
-499.78
520.61
502.97
20000, 500,
5 3
466.91
-492.66
-499.69
238.35
225,89
22000, 300, 300), $ s= 3
283.58
296.90
-99.775
469.02
309.20
22000, 1000),
2
944.68
.999777
.99.833
207.37
245.58
(3000, 1000, 1000
8 2
994.68
-989.65
-999.83
81.96
84.25
3000, 2000, 1000),
2
.92.09
-996.68
-999.97
662.55
648,97
2000, 500, 500, 500],
s 2
-48.19
-497.30
-499.90
144.28
146.75
3000, 500, 500, 500],
5 2
-480.42
-496.66
-499.88
137.56
159.70
As it can be observed in Table the bound T Lighter.cs consistently better, across all instances. Moreover, the running time of Tighterrcs is relatively stable, even for networks with large number of neurons, akin maal-to-mediim-siize convolutional networks.
19

---

Published as a conference paper at ICLR 2025
A.4 ON DETERMINING THE SUBSETS OF DECISION VARIABLES
Let us describe in details how decision variables are structured within the first-order sparse SDP relaxation of the problem (19). We emphasize that this structure is valid only for the first-order sparse SDP relaxations, and regardless of the norm describing the input perturbation region.
We recall that subsets ([*)<e[1.p] are said to satisfy the RIP property
(Ix+1 n ())*)()) C 1,, for some S k.
(45)
The RIP property 445) is one of the essential requirements for the convergence of the sparse SOS- based hierarchy of SDP relaxations (Magron & Wang 2023 Assumption 3.1).
Theorem A.4.1. The structure of decision variables of the standard BNN robustness verification problem is such that:
If L 1, there no subsets size nı 1, given by Is 121,1,...... 21,m Do.k 1 l [1,no]]
If I= = 2, there are no + subsets of size 1,, given by I = { 1m Fo,k) for E [11, (01,no) nol and Ih +k f01,1...... ;1,1...,,,,,,, 22 ) for le E [1, n2].
If L 2 3. there are - 2 + no + nL subsets in total, and their maximum n(jt1).. The subsets
size is given by max(n1 1, n1 1, maxxjgL-2 are given by I = 1: TR.u Ik+1,1.---- 3R+1, for to E [1, 21. 11-248 (#1.-I.b.... It-l. LL for [L, nt..
VI, Di.ny } for k [L, no]] and 11-2400th
In any of the three cases, the defined subsets satisfy the RIP property.
Proof of Theorem A.4.1 We consider different cases, depending on the depth of the BNN:
L
All the nodes from the hidden layer form a separate subset with each individual input node, result- ing in vi subsets of size 1. Thus, we can set T = (æ11,1.... LI,,, Zo. J. for & E [1, no]. The RIP property clearly satisfied, as the nodes from the hidden layer appear in each subset.
= 2:
All the nodes from the first hidden layer form separate subset with each individual input node, resulting in no subsets of size n4 + 1. Thus, we can set 1 [.1,1--... Fi Lo for k [[L no]]- Moreover, they also form separate subset with each individual node from the second hidden layer, resulting in no subsets of size + 1. Thus, we can set 4no+k = (.1,1...., Fi,n #2,x), J. for & [1, nz]. The RIP property is satisfied as the first hidden layer nodes appear in each subset.
L L23 3:
For every & E [1,L - 21. a pair (k, k + 1) of adjacent hidden layers forms a subset I {Ik,1...... Ik,n, 1..+1.1.... ................................ Ik+1,me+1 } of size ny 74+11 Furthermore, all the nodes from the first hidden layer form a separate subset with each individual input node, resulting in nn subsets of size m + 1. Thus, Finally, all the nodes from the penultimate hidden layer form a separate subset with each individual node from the last hidden layer, resulting in nz subsets of size n + Thus, we
set Tr.2+* [21.1,..., Fi.....,,i,,, Fi,ny ko for k E [1, no]-
can set + = -- -L-1.n--1 LL for k E [1, mz].
Therefore, there are L 2 + no + subsets in total, and the maximum subset size is given by max(ni + 1, n + 1, m..xxss--2(1, + nj+1)). Moreover, given this particular ordering (enumeration) of subsets, the RIP property is satisfied. Indeed,
If [22 L 2]. then
Ig (Ujgk-119) (01-1111.... Fk 1,m C T
(46)
20

---

Published as a conference paper at ICLR 2025
lfk [L -
nol. then
4. n (Ujsk-11)) { ,..., 3imma 41.
(47)
If E [L 2 no + +, 2 m21ltten
n (U)gA-11z) ( (#L-111.... D.1--1,....,LLLI....... LL-LM. C IL-
(48)
Thus, the RIP property holds in all three cases, which concludes the proof.
An alternative structure of node subsets, independent of the depth of the BNN, is to consider 1SSS
( Li Jigjsn 1.1Skkn This choice results in Σ 74-1 n, subsets of size two, since every node coupled with all the other nodes form adjacent layers. The RIP property always holds in this case if subsets are enumerated in an order that mirrors the feed-forward structure of the BNN. Computations are generally faster for this structure of subsets, but the obtained bounds are much coarser.
B EXPERIMENTAL SETUP
Training details: All neural networks have been trained on MNIST dataset (data were scaled to belong to [-1, 1)784) using Larq (Geiger & Team, 2020), open-source Python library for training neural networks with quantized (binarized) weights and activation functions.
The training process, lasting 300 epochs, has consisted of minimizing the sparse categorical cross-entropy, using the Adam optimizer (Kingma Bal 2014). The learning rate has been handled by the exponential decay learning scheduler, whose initial value has been set to be 0.001. SteTern quantizer with different threshold values has been used induce different sparsities of the weights matrices. Network parameters have been initialized from uniform distribution. Batch normalization layers have been added to all but the output layer. All networks have achieved over 95% accuracy the test set.
Optimization details: Semidefinite Programming (SDP) problems have heen assembled using TSSOS (Wang et al.] [2021a). specialized Julia library for polynomial optimization. Correlative sparsity has been exploited by using the CS="MF" option, which generates an approximately smallest chordal extension of the identified subsets structure. The SDP values have been computed via the interior-point solver Mosek (Andersen & Andersen 2000), and the SDP solving time was recorded.
Since computing the exact value of the objective function for MILP and MINP problems is highly computationally demanding, we transform those problems into satisfiability problems by setting the objective function to be a constant function equal zero, and adding f()) < 0 to the set of constraints. Infeasibility the resulting problem provides a certificate of robustness. These problems have then been solved using Gurobi, where the time limit was set 600 seconds. The upper bound presented in Figure 2 has been determined by randomly sampling 10, 000 points from the uniform distribution over the perturbation region and documenting the lowest objective function value observed at those points.
Our code is available via the following following link: POP4BNN GitHub Repository
More detailed experimental results: We provide detailed verification results against ||-Iloo (see Table and Table 5) and ||-1|2 (see Table and Table 7 attacks. Those results illustrate that the solving time general branch and bound algorithms could be significantly improved the LP bounds would be replaced by tighter SDP bounds, such Trihhter.ss The improvement would be noticeable for ||-I|2 verification.
Finally, due to their increased computational complexity, the experiments from Table were run on server with 26-core Intel(R) Xeon(R) Gold 6348 CPU @ 2.60GHz and RAM of 756GB.
21

---

Published as a conference paper at ICLR 2025
Table 4: Verification against -atacck:: detailed numerical results for BNN1 (784, 500, 500, 10], w² 34.34%. For example, image 72 illustrates that MILP methods can not handle severe attacks. Likewise, image 28 confirms the potential benefits accommodating T Trighter.cs within the branch and bound algorithms. Note that MILP implementation only solves the attack feasibility problem, since computing exact bounds would result in much more timeouts.
Image Index
tighter,cs bound (s)
MSPf-MMIPP
bound
(s)
11.11x
1.25
14
1.08
1 11.53
infeasible
552.99
24
5.82
15.43
timeout
> 660
26
0.31
7.18
infeasible
4.07
28
29.86
14.90
infeasible
29.08
31
7.54
10.08
infeasible
11.67
52
12.17
7.53
infeasible
0.49
55
11.05
6.99
infeasible
3.33
57
3.23
8.69
infeasible
6.41
72
29.43
9.75
infeasible
1.36
83
17.29
14.07
infeasible
44.62
100
19.99
6.64
infeasible
0.30
611111
1.50
28
11.18
70.62
timeout > 600
52
0.48
18.35
infeasible
7.18
55
2.25
16.33
infeasible
7.42
72
20.65
28.52
infeasible
15.68
83
8.37
17.68
infeasible
519.23
100
8.32
10.39
infeasible 2.21
61111
1.75
28
0.20
42.46
timeout 600
72
13.50
37.79
timeout -600
Table 5:
Verification against attacks: detailed numerical results for BNNg [784, 500, 500, 10), n, 19.07%. Remarkable improvements can be observed for images 20, 28, 29 and 33.
Image Index
Fighter.ce bound (8)
TSoRt-MILP
bound l (s)
$1111 0.75
19.54
42.31
infeasible
13.39
20
8.72
107.36
timeout
> 600
26
14.90
37.25
infeasible
10.61
28
14.26
75.15
infeasible
227.07
29
7.48
47.33
infeasible
200.02
7.31
49.35
timeout
> 600
55
25.14
28.96
infeasible
4.67
35.33
35.80
infeasible
6.85
83
22.14
44.61
infcasible
16.26
22

---

Published as a conference paper at ICLR 2025
Table
Verification against |ltll=-attacks:
detailed numerical results for BNN1
[784, 500, 500, 10), wi 34.34%. Notice that the number of timeouts is significant. On the other hand, the verification time associated to tighter.cs remains relatively stable.
Image Index
tighter. bound (s)
TSoft-MINP
bound t (s)
11-111
20
4.20
12.79
timeout
600
10
0.71
16.41
infeasible
564.03
11
6.05
13.91
infeasible
376.86
12
14.34
8.00
infeasible
181.41
13
5.03
21.96
timeout
> 600
14
34.12
15.05
infeasible
47.93
15
4.35
18.58
timeout
> 600
23
9.91
9.13
infeasible
0.40
24
37.52
12.37
infeasible
354.42
26
32.32
11.12
infeasible
0.71
28
58.43
22.14
infeasible
203.53
31
27.73
8.31
infeasible
1.05
48
12.48
16.48
timeout
600
49
14.85
15.72
timeout
600
52
34.45
10.35
infeasible
0.07
55
42.34
5.32
infeasible
0.08
56
15.68
11.15
timeout
600
57
30.32
6.16
infeasible
0.48
59
17.66
27.45
timeout 600
61
8.08
15.45
infeasible
102.50
65
5.20
8.99
timeout
600
69
12.73
19.38
infeasible
272.38
70
6.37
15.82
infeasible
292.86
72
46.78
15.88
infeasible
0.15
73
18.78
11.73
infeasible
14.15
77
22.70
30.85
infeasible
480.90
80
11.89
12.12
infeasible
72.41
83
43.12
20.10
infeasible
60.96
86
9.89
14.54
infeasible
531.24
89
18.74
17.25
infeasible
229.98
91
11.59
18.89
infeasible
505.02
92
13.55
34.95
timeout 62.56
600
94
7.13
14.75
infeasible
98
2.64
13.02
infeasible
165.10
99
13.27
12.16
infeasible
100.43
100
42.32
8.95
infeasible 0.09
61.11a
30
14
11.81
17.54
timeout 600
24
15.04
28.94
timeout
600
26
15.48
7.28
infeasible
108.11
28
35.08
40.25
timeout
> 600
31
6.89
16.39
timeout
600
52
16.78
10.86
infeasible
191.03
55
21.80
10.49
infeasible
555.08
57
12.04
10.93
timeout
> 600
72
35.81
12.45
infeasible
353.96
73
3.59
10.44
timeout
> 600
77
3.45
37.65
timeout 600
83
26.76
22.78
timeout
600
100
25.51
9.14
infeasible
64.95
23

---

Published as a conference paper at ICLR 2025
Table Verification against [784, 500, 500, 10], w, 19.07%. Images 57 and 89 demonstrate that T tighter.ss typically cer- tify robustness more than times faster.
||.ll-attacks:
detailed numerical results for BNN2
Image Index
tighter,cs bound
TSoftMMIN
(s)
bound
(s)
0111112 15
2
2.74
31.34
infeasible
279.66
0.14
47.94
timeout
> 600
11
50.95
17.32
infeasible
12.99
19.98
39.04
timeout
> 600
20
33.38
88.27
timeout
> 600
23
13.43
19.91
infeasible
253.64
26
40.90
16.40
infeasible
12.57
28
40.87
45.39
infeasible
73.84
29
39.00
23.42
infeasible
9.52
31
15,00
15.89
infeasible
59.66
33
30.05
51.76
infeasible
134.40
48
16.31
47.78
timeout
> 600
55
53.65
12.11
infeasible
0.25
57
6.16
25.38
timeout
> 600
61
2.29
19.44
infeasible
253.44
69
20.93
67.48
timeout
600
71
18.96
17.43
infeasible
88.33
72
61.78
14.47
infeasible
1.40
73
25.72
14.60
infeasible
62.32
77
2.48
37.19
infeasible
510.44
83
47.72
23.62
infeasible
81.36
86
6.54
115.93
timeout
>> 600
87
22.33
69.43
infeasible
344.06
88
15.48
23.39
infeasible
250.97
89
27.29
29.73
timeout 600
92
23.51
57.17
timeout 600
100
15.40
20.03
infeasible 108.08
Experimental results for more complex data sets and larger networks: To further demonstrate the versatility of our method, provide additional illustrative experiments for BNN; [3072, 5000, 800, 10], w, = 55.97%, achieving the test accuracy of 47.66% on CIFAR-10 data set.
As illustrated in Table 8 our approach demonstrates comparable performance even on larger datasets, such as CIFAR- IO, and for larger networks involving nearly 9000 neurons.
Specifically, tighterr,s proves the robustness of images 1, 2 and 35 at least 3x, 6x, and 5.5x faster than MSLP-MILP, respectively. contrast, the low quality of LP bounds prevents MILP from provid- ing an answer within the imposed one-hour time limit. These additional experimental results further validate that our method consistently provides high-quality lower bounds, even for large-scale prob- lems, which is concordant with the results for BNN, and BNN2-
However, for images indexed by and 10, for example, our method unable to provide an answer, while MILP efficiently certify their non-robustness. This difference arises due to the fact that MILP based methods do not aim to solve the optimization problems to global optimality but instead focus determining the feasibility of an adversarial attack, which is inherently less computationally demanding.
We believe that incorporating tighter SDP bounds within the MILP framework could enhance the ability of MILP methods to certify robustness in more complex cases. This represents a promising direction for future research.
24

---

Published as a conference paper at ICLR 2025
Table 8: Verifying robustness of 3NN; on CIFAR-10, for an input region determined by 611-11> 0.2/255. Data were scaled to [-1, 3072 and a time limitation of 3600 s was imposed. We present the results of the robustness verification queries on the first 40 images from the test data set, among which 22 were correctly classified.
Image Index
"ighterr.ss
TSon-MILP
bound
t (s)
bound timeout
(s)
1
20,46 (robust)
1179.55
3600
2
7.83 (robust)
571.08
timeout
3600
7
-30.28 (unknown)
380.10
timeout
3600
8
-68.50 (unknown)
1721.79
feasible (not robust)
1.71
10
-62.31 (unknown)
1330.03
feasible (not robust)
87.46
11
142.50 (unknown)
650.79
feasible (not robust)
0.11
12
-94.22 (unknown)
1115.18
feasible (not robust)
0.071
14
103.36 (unknown)
493.80
feasible (not robust)
0.067
15
-71.09 (unknown)
2090.44
feasible (not robust)
57.09
18
-97.96 (unknown)
1469.67
feasible (not robust)
0.08
19
31.06 (robust)
344.70
infeasible (robust)
9.02
20
-25.66 (unknown)
823.54
timeout
3600
21
-90.54 (unknown)
670.94
feasible (not robust)
0.59
24
29.08 (unknown)
629.50
timeout
3600
27
-83.76 (unknown)
766.95
feasible (not robust)
0.54
29
110.26 (unknown)
873.51
feasible (not robust)
0.07
30
-60.63 (unknown)
1407.68
feasible (not robust)
1.39
31
-29.51 (unknown)
1190.56
timeout
3600
33
timeout
3600
timeout
3600
34
-73.15 (unknown)
569.46
feasible (not robust)
0.51
35
36.62
(robust)
657.73
timeout
3600
40
-5.82
(unknown)
650.79
timeout
> 3600
25


Reviews:
[{"review_id": "SEy5cRVHey", "reviewer": "Reviewer_TkGW", "summary": "The paper presents a novel approach for verifying properties of Binary Neural Networks (BNNs), particularly in the context of robustness against adversarial attacks. Traditional verification methods for BNNs, such as Satisfiability Modulo Theories (SMT) and Mixed-Integer Linear Programming (MILP), face scalability issues when applied to larger networks. To address these challenges, the authors propose using Semidefinite Programming (SDP) relaxations derived from sparse polynomial optimization. This approach is designed to verify BNN robustness efficiently and accurately, overcoming numerical challenges inherent in MILP solvers. Experimental results indicate that the SDP-based method provides significant improvements in both robustness verification against adversarial attacks and computational efficiency, with an average speedup of 4.5 to 11.4 times compared to conventional methods.", "questions": "Could the authors provide additional experimental results on a wider variety of models? Including more model architectures would enhance the robustness of the conclusions and provide a stronger case for the method’s effectiveness across different settings.", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "-  Introduces a new SDP-based approach that enhances the scalability and precsion of BNN verification.\n - Efficiently handles continuous input spaces without requiring input quantization.\n -  Theoretical contributions, including tighter SDP relaxations, improve the accuracy of robustness bounds.\n  - Experimental validation across benchmarks highlights the method’s advantages in speed and robustness certification.", "weaknesses": "The paper presents an interesting approach; however, it lacks sufficient model variety in its experiments. Only two models were used to demonstrate the proposed method, which limits the generalizability and persuasiveness of the results. For a more robust evaluation, it would be beneficial to include additional models, particularly from diverse architectures, to strengthen the findings and validate the method across a broader range of scenarios.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "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": "ENw9rnVvSb", "reviewer": "Reviewer_Rj7X", "summary": "The paper introduces a novel method for verifying the robustness of Binary Neural Networks (BNNs) against adversarial attacks using Semidefinite Programming (SDP) relaxations derived from Sparse Polynomial Optimization. This approach outperforms existing LP relaxation used in MILP-based verification methods without introducing much computation overhead. Specifically, the authors suggest that the SDP-based relaxations could be embedded within branch-and-bound algorithms in MILP solvers to improve bound estimation, accelerating the verification process without altering the core MILP framework. Their method achieves bounds that are up to 55% tighter than those obtained with traditional linear relaxations and demonstrates significant computational efficiency, especially under large input perturbations.", "questions": "1. Have you tested this method on more complex datasets or architectures beyond MNIST? If so, what were the results, and if not, do you anticipate any challenges?", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. **Novel Use of SDP for BNN Verification**: Employing sparse Polynomial Optimization and SDP relaxations for BNN verification represents an innovative approach, potentially enhancing scalability and precision over existing MILP-based methods.\n\n2. **Significantly Improved Bounds**: By using SDP relaxations, the authors achieve up to 55% tighter bounds compared to traditional linear relaxations in MILP, a notable improvement in robustness certification accuracy.\n\n3. **Efficient Computation**: Experimental results demonstrate considerable speedups (up to 50x in severe attack scenarios), showing that the method is computationally efficient and less conservative in bounding compared to LP-based techniques, especially in high-dimensional BNNs.\n\n4. **Broad Norm Compatibility**: The method accommodates both ∥.∥∞ and ∥.∥2 norms for adversarial attacks, expanding its applicability across different attack types, which is less common in the BNN verification field.", "weaknesses": "1. **Limited Dataset and Network Complexity**: The experiments are primarily on MNIST-based networks, which may not fully demonstrate the method’s performance on more complex datasets or larger architectures. Expanding the experimental validation could strengthen the generalizability of the approach.\n\n4. **Comparative Analysis with State-of-the-Art**: While comparisons with LP and MILP are made, a broader comparison with recent state-of-the-art BNN verification techniques could further validate the advantages and potential limitations of the SDP-based approach.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "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": "fGYdbCg7ne", "reviewer": "Reviewer_7uz5", "summary": "This paper introduces a novel approach to verify the robustness of BNN based on sparse polynomial optimization, specifically through Semidefinite programming relaxation. The authors first encode the original verification problem as a polynomial optimization problem (POP) and then apply SDP relaxation on it to obtain lower bounds for certifying the robustness. While the verification method is sound and incomplete, experimental results show that it provides a more precise bound than LP-based methods.", "questions": "See the weakness raised in **Weaknesses**.\n\nOther minor comments:\n\n- I failed to find the explanation for what the data in parentheses in Column $\\tau_{tighter,cs}^1$ represent in Tables 1 and 2.\n- MILP methods aim to verify whether a property holds or fails, offering a definitive answer rather than estimating bounds to certify robustness. Therefore, comparing the two approaches (SDP-based vs. MILP-based) should ideally focus on metrics related to verification success rates, computational efficiency, or scalability across various network sizes, rather than on bound tightness.", "limitations": "", "rating": 5, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "- The problem (verification of Transformers) is important.\n- A novel method based on SDP to verify the robustness of BNN.\n- Compared to LP-based methods, a more precise lower bound is obtained.", "weaknesses": "- The motivation for this approach is not intuitive. The authors claim that existing methods are either incompatible with continuous input data or are limited to $L_\\infty$ input perturbations. However, expanding support to other types of input regions may not constitute a compelling contribution: i) $L_\\infty$ perturbations are the primary standard in the field, and ii) most BNN verifiers support continuous input spaces. Furthermore, for methods $M$ specifically designed for discrete input region (i.e., input $x\\in$ {-1,1}$^{n_0}$), one can also treat the second layer (assuming the original input region is continuous, as the setting in this work) as the new input layer and then apply these methods $M$ to verify the robustness.\n- The experimental results are not convincing. The MILP-based method, which is sound and complete, solves significantly more verification tasks than the proposed SDP-based approach. While the authors introduce a \"soft\" encoding to avoid numerical errors, it is relatively straightforward similar to methods in previous work.\n- For $L_\\infty$ experiments, it would be beneficial to include comparisons with other SOTA methods, such as the SMT-based approach (Amir et al.). \n- As Gurobi supports multi-threaded solving, presenting experimental results on multiple threads would also strengthen the evaluation.\n- Table 3 gives more results on bound computation, however, it is not clear if these bounds lead to verified results (i.e., proving the robustness).", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "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": "aWpiZ1mTjS", "reviewer": "Reviewer_o79c", "summary": "The paper considers the formal verification of binary neural networks in the classification setting.\nFormal verification is necessary as (any) neural network is inherently prone to adversarial attacks.\nIn the paper, the robustness of binary neural networks is verified using semidefinite programming derived from polynomial optimizations.\nIn particular, polynomials up to order 2 are used as constraints and existing solvers (Mosek, Gurobi) are used to prove the robustness property by providing a lower bound.\nThe experients considers l_2 and l_inf robustness properties and shows that while achieving better bounds than simple linear programming, it also has a reduced verification time than related methods based on MILP/MINP.", "questions": "- Can you provide the missing details about the evaluation I mentioned above?\n- You mentioned in Sec. 2.3 that you use the (tractable) inner approximations of the set of polynomials that are nonnegative on S. Why is it enough to only consider that subset?\n- Why can the weights take values {-1,0,1} but the bias any value in |R?\n- Why does you appraoch not suffer from floating-point inaccuracies?", "limitations": "", "rating": 6, "confidence": 3, "soundness": 2, "presentation": 2, "contribution": 3, "strengths": "- the considered problem is highly relevant\n- deep theoretical analysis that goes beyond simple linear relaxations and rather design the verification algorithm to exploit certain properties of the considered network architecture\n- The theoretical results show strictly better bounds (Thm. 3.1 & 4.1), which proves the point of using the more complex verification algorithm.\n- the approach allows to verify more general input perturbations. In particular, l_2, which was not considered before in binary neural network verification although it has been considered in standard neural networks.", "weaknesses": "Main points:\nIt is hard to follow the theoretical analysis in the paper. I tried to identify some of the key issues and give examples for each case:\n- Crucial results from references are used without re-stating them or at least providing the exact equation number in the reference paper:  E.g., Sec. 4: \"Firstly, notice that the semi-algebraic representation of the subgradient of the ReLU function derived in Chen et al. (2020) provides an alternative encoding of the sign(·) function.\" This sentence in then used without further explanation to transform (7) into (17). \n- Formal inconsistencies: E.g., it is unclear what the output of sign(0) is; (4) says that W can be in {-1,0,1} but later in Sec. 3 says it is in {-1,1}, which might influence how certain normalizations have to be considered, e.g., the bounds in (11).\n- try to introduce all concepts before they are used. E.g., the term \"cliques\" is not properly introduced. It appears to be sets of neurons but I am unable to assess how they are determined. Also, the variable \"d\" is used throughout Sec. 2.3 but is only later introduced as \"relaxation order\". Similarly, the operation \"nv(A)\" is introduced after its first usage in (12), making (12) unable to be understood by the reader up to this point. It is explained in the paragraph after, but I think moving such things to the notation section would be more beneficial as they are used throughout the paper and a reader can then go back to the notation section to (re-)refer to those details. \n- Steps to derive the constraints are rather quick and more explanations could help to follow along\n\nAdditionally, the experiments show only single-dimensional results without saying over how many instances the results are averaged and do not provide a standard deviation where applicable. Also, it is unclear if the compared approaches are taken from the literature or arbitrarily constructed. If the latter is true, it misses a comparison to related work altogether.\n\nMinor points:\n- It is unclear why the approach does not suffer from floating point inaccuracies. In fact, the term \"floating-point\" only appears twice in the paper (only in the abstract and the contribution section (Sec. 1.1)).\n- the paper claims that the approach does not suffers from an exponential running time (Sec. 6) but it misses a thorough analysis of its runtime. The average speed up of 4.5 / 11.4 stated in the contribution section (Sec. 1.1) does also not support this claim.\n- Make the example in Fig. 1 a running example by moving it further up in the paper and continuously refer to it when explaining all terms.\n- Similarily, give an intuitive explanation why adding those tautologies are necessary\n- Only the classification setting is considered. This could be stated more clearly.\n- the related works section could also include more research on the verification of standard neural networks (e.g., VNN-COMP) to better place this line of research in the broader context.\n- Fig 2: misses a label and ticks of the x axis.\n- no repeatability package is provided\n\nFurther points that could help improve the paper but did not directly influence the score:\n- give a real-life example where binary neural networks are used and verifying the robustness is necessary\n- Avoid the usage of abbreviations. These usually do not save a lot of space but makes reading more difficult as one is challenged to memorize all abbreviations in addition to the complexity of the paper.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "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:

Decision: Accept (Poster)