Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization

## Abstract

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
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} ∥ . ∥ start_POSTSUBSCRIPT ∞ end_POSTSUBSCRIPT and ∥ . ∥ 2 \|.\|_{2} ∥ . ∥ start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT -based adversarial attacks.

## 1 Introduction

In the evolving landscape of machine learning, Binary Neural Networks (BNNs) have emerged as an intriguing class of neural networks since their introduction in 2015 [CourbariauxBNN_2015, Hubara2016_BNN]. The architectural simplicity and inherent advantages of 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 [RastegariXNORNet_2016, SunOBJDetection_2018, XiangSpeech2017].

Despite their great approximation capacities, general deep neural networks are sensitive to input perturbations [SzegedyIntriguing2014, Siam-News21].
BNNs are not any different in this regard. Indeed, quantized or binarized networks do not necessarily preserve the properties satisfied by their real-precision counterparts [Galloway2018_attackingBNN, GiacobbeQuantization_2020].
That is why verifying their robustness is one of the crucial aspects of their design and deployment.
A classifying 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 $\bm{x}$ satisfying
$P(\bm{x})\wedge Q(\textbf{BNN}(\bm{x}))$, where $P$ is a pre-condition on $\bm{x}$, e.g., stating a valid input perturbation, and $Q$ is a post-condition on $y=\textbf{BNN}(\bm{x})$, e.g., stating an (undesirable) alteration of the highest output score.
If both properties hold for some $\bm{x}$, the network is not robust.

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 verification frameworks do not exploit the bit-precise semantics of BNNs [GiacobbeQuantization_2020], and in parallel, those BNN-specific approaches for robustness verification often suffer from limited scalability [Lazarus2022_MILP, Narodytska2020_SAT_Friendly_BNN].
Two related methodological axes can be identified. Firstly, methods based on Satisfiability Modulo Theories (SAT/SMT), as in [AmirGuy2021_SMT, KaiJia2020_EV, Narodytska2018_V, Narodytska2020_SAT_Friendly_BNN], encode the BNN verification problem into Boolean formula satisfiability, and leverage modern off-the-shelf solvers to prove robustness or find counterexamples. Secondly, [Khalil2019_IProp, Lazarus2022_MILP] cast robustness verification as a Mixed Integer Linear Programming (MILP) optimization problem. Both approaches belong to the group of exact verification methods, i.e., they are sound and complete.
In this paper, instead of solving the BNN verification problem exactly, we rather examine it through the lens of (Sparse) Polynomial Optimization Problems (POP) [lasserre2015introduction, MagronSpop2023], that can be approximated with hierarchies of relaxations based on Semidefinite Programming (SDP).
Recent frameworks [chen2020, chen2021, Latorre2020Lipschitz, NEWTON2023] 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-algebraic nature of the $\operatorname{sign}$ activation function to encode the BNN verification 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 SDP-based 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. Knowing 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.
Consequently, our method can deliver robustness certificates over 20 times more rapidly than traditional MILP algorithms, which rely on linear relaxations that we demonstrate to be up to $55\%$ less accurate compared to the our SDP bounds.
- •
We demonstrate the effectiveness of our method, compatible with continuous input space, in verifying robustness against both $\|.\|_{\infty}$ and $\|.\|_{2}$-based adversarial attacks, the latter being much less studied in the BNN verification literature.

### 1.2 Related works

SDP-based verification methods: Certifying adversarial robustness using SDP relaxations has been first proposed in [RaghunathanSL18].
Tightening of the SDP bounds via linear reformulations and quadratic constraints has been proposed in
[Fazlyab2020IEEE, batten2021ijcai, lan2022tight].
Verification can also be tackled by computing upper bounds of Lipschitz constants [Fazlyab2019Lipsh, Latorre2020Lipschitz, chen2020].
Chordal and correlative sparsity can be exploited [AntonXue2024, NEWTON2023, chen2021] to design more efficient SDP relaxations.
The first-order dual SDP approach developed in [Dathathri2020] enables efficient verification of high-dimensional models. Note that these approaches have been mainly designed to verify full-precision ReLU networks.
BNN verification: Binarized weights and activation functions allow for the BNN verification problem to be exactly encoded into a 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 [Narodytska2018_V, narodytska2018formal]. Consequently, only small and medium-size networks can be handled within this framework. In order to 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 [Narodytska2020_SAT_Friendly_BNN], enforcing sparse patterns to increase the number of shared computations, neuron-factoring [Narodytska2020_SAT_Friendly_BNN, Cheng2018_Verif].
The SAT solver proposed in [KaiJia2020_EV, KaiJia2020_FPE] is tailored for BNN verification. By efficiently handling reified cardinality constraints and exploiting balanced weight sparsification, this solver could achieve significantly faster verification on large networks.
The SMT-based framework from [AmirGuy2021_SMT] extends the well-known Reluplex [GuyRPX_2017] framework to support binary activation functions.
Notice that these works are either incompatible with continuous input data or are restricted to $\|.\|_{\infty}$ 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 $\|.\|_{2}$ norm.

The sole nature of BNNs makes them convenient for being directly represented via linear inequalities and binary variables, enabling the verification problem to be cast as a MILP.
These properties are exploited in [Khalil2019_IProp], where big-M constraints model the neuron activations, and a heuristic named IProp decomposes the original problem into smaller MILP problems. However, the big-$M$ approach is also well-known to be sensitive to the $M$ parameter [GUROBI-Big-M].
Improved bounds for each neuron have been proposed by [HanGomez2021_CVX] that lead to tighter relaxations, but only on medium-sized networks.
This suggests that BNNs might also suffer from a convex relaxation barrier for tight verification [HadiBarrier_2019]. Another MILP-based approach has been discussed in [Lazarus2022_MILP, Lazarus2022_MILPThesis], where both input and output domain of a property to be verified are restricted to polytopes.
The set-reachability method from [Ivashchenko2023_StarR] extends the star set and Image star approaches from [Bak2017_Star, DungSTAR_2019, Tran2020_ImageStar].
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 to 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 [Baluta2019_QV, Narodytska2019_MC], quantitative robustness verification is reduced into a model counting problem over a Conjunctive Normal Form (CNF) expression. SAT-based approaches are derived from either (Ordered) Binary or Sentential Decision Diagrams in [ShiTractRep_2020, Shih2019_Angluin, Zhang2021_BDD4BNN].

### 1.3 Notations and preliminaries

We use Roman letters to denote scalars, and boldfaced letters to represent vectors and matrices. If $\bm{A}$ is a matrix, then $\bm{A}_{(k:,)}$ denotes its $k$-th row vector, and $\|\bm{A}\|_{F}$ denotes its Frobenius norm.
The Hadamard product is denoted by $\odot$, i.e., $(\bm{A}\odot\bm{B})_{ij}=\bm{A}_{ij}\bm{B}_{ij}$.
The ring of $n$-variate real polynomials (resp. of at most degree $d$) is denoted by $\mathbb{R}[\bm{x}]$ (resp. $\mathbb{R}[\bm{x}]_{d}$).
Let $\Sigma[\bm{x}]$ be the cone of multivariate Sum Of Squares (SOS) polynomials and $\Sigma[\bm{x}]_{d}:=\Sigma[\bm{x}]\cap\mathbb{R}[\bm{x}]_{2d}$. By $\langle\bm{x},\bm{y}\rangle=\sum_{i=1}^{n}x_{i}y_{i}$ we denote the standard inner product of vectors $\bm{x},\bm{y}\in\mathbb{R}^{n}$.
If $k_{1},k_{2}\in\mathbb{N}$ with $k_{1}\leq k_{2}$, then $\llbracket k_{1}\mkern 1.5mu,\mkern 1.5muk_{2}\rrbracket:=\{k_{1},\dots,k_{2}\}$.
Let $\mathbb{B}_{||.||}(\bar{\bm{x}},\varepsilon)$ be the $||.||$-ball of radius $\varepsilon$ centered at $\bar{\bm{x}}$. We denote by $\mathbb{S}_{+}^{n}$ the set of symmetric positive semidefinite matrices of size $n$.
We recall that $f\in\mathbb{R}[\bm{x}]_{2d}$ is SOS if and only if a
positive semidefinite (PSD) matrix $\bm{G}$ satisfies $f=\bm{v}_{d}^{\intercal}\bm{G}\bm{v}_{d}$, where $\bm{v}_{d}:=(1,x_{1},\dots,x_{n},\dots,x_{n}^{d})^{\intercal}$ is the vector of monomials of degree at most $d$ with size $s(d):=\binom{n+d}{d}$.

###### Definition 1.1 .

Let $\bm{g}:=(g_{j})_{j\in\llbracket 1\mkern 1.5mu,\mkern 1.5mum\rrbracket}$ and $\bm{h}:=(h_{k})_{k\in\llbracket 1\mkern 1.5mu,\mkern 1.5mul\rrbracket}$ denote families of polynomial functions. For all $j\in\llbracket 1\mkern 1.5mu,\mkern 1.5mum\rrbracket$, $k\in\llbracket 1\mkern 1.5mu,\mkern 1.5mul\rrbracket$, define $d_{j}:=\lceil\deg(g_{j})/2\rceil$ and $\bar{d}_{k}:=\deg(h_{k})$. Then,
the $d$-truncated quadratic module $\mathcal{Q}_{d}(\bm{g})$ generated by $\bm{g}$, and the $d$-truncated ideal $\mathcal{I}_{d}(\bm{h})$ generated by $\bm{h}$ are

$$ $\displaystyle\mathcal{Q}_{d}(\bm{g})$ $\displaystyle:=\left\{\sigma_{0}+\sum_{j=1}^{m}\sigma_{j}g_{j}\mid\sigma_{0} \in\Sigma[\bm{x}]_{d},\sigma_{j}\in\Sigma[\bm{x}]_{d-d_{j}},j\in\llbracket 1 \mkern 1.5mu,\mkern 1.5mum\rrbracket\right\}$ $\displaystyle\mathcal{I}_{d}(\bm{h})$ $\displaystyle:=\left\{\sum_{k=1}^{l}\psi_{k}h_{k},\psi_{k}\in\mathbb{R}[\bm{x} ]_{2d-\bar{d}_{k}},k\in\llbracket 1\mkern 1.5mu,\mkern 1.5mul\rrbracket\right\}$ $$

###### Definition 1.1 .

## 2 Main ingredients

### 2.1 Binary Neural Networks

Let $L\geq 1$ be the number of hidden layers of a classifying BNN, with layer widths being given by $\bm{n}=(n_{0},n_{1},\dots,n_{L},n_{L+1})^{\intercal}\in\mathbb{N}^{L+2}$
, where $n_{0}$ and $n_{L+1}$ are input and output dimensions. A feed-forward BNN is a mapping from the input region $\mathcal{R}_{n_{0}}\subset\mathbb{R}^{n_{0}}$ to the output set $\llbracket 1\mkern 1.5mu,\mkern 1.5mun_{L+1}\rrbracket$ realized via successive compositions of several internal blocks $(\text{{B}}_{i})_{i=1,\dots,L}$ and an output block $\textbf{B}_{o}$:

$$ $\displaystyle\begin{split}\text{\text{BNN}}:\mathcal{R}_{n_{0}}&\to\llbracket 1 \mkern 1.5mu,\mkern 1.5mun_{L+1}\rrbracket\\ \bm{x}^{0}&\mapsto\text{BNN}(\bm{x}^{0}):=\text{argmax}\left(\textbf{B}_{o}( \textbf{B}_{L}(\dots(\textbf{B}_{1}(\bm{x}^{0}))))\right).\end{split}$ (1) $$

For any $i\in\llbracket 1\mkern 1.5mu,\mkern 1.5muL\rrbracket$, the internal block $\textbf{B}_{i}$ implements successively three different operations: affine transformation, batch normalization(^1^11Since batch normalization can be understood as another affine transformation, it can be omitted throughout the technical modelling part, w.l.o.g.) and point-wise binarization, so that its output vector, denoted by $\bm{x}^{i}$, belongs to $\{-1,1\}^{n_{i}}$. These operations are described by a set of trainable parameters:
τ^1_tighter, cs=
&It is also possible to derive the corresponding dual relaxations.
Notice that a polynomial $f$ in the variable $\bm{x}=(x_{1},\dots,x_{n})$ can also be written as $f=\sum_{\alpha\in\mathcal{A}}f_{\alpha}\bm{x}^{\alpha}$ with $\mathcal{A}\subset\mathbb{N}^{n}$ and $f_{\alpha}\in\mathbb{R}$, where $\bm{x}^{\alpha}=x_{1}^{\alpha_{1}}\dotsc x_{n}^{\alpha_{n}}$. Then the *moment hierarchy* [Lasserre2001] for the POP introduced in Section LABEL:sec:_POPbasics corresponds to:

$$ (4ruvaaabbra) (4ruvaaabbre) $$

where $\bm{y}=(y_{\alpha})_{\alpha}$ is a sequence indexed by $\alpha\in\mathbb{N}^{n}$ and $L_{\bm{y}}$ the linear functional defined by

$$ $f\mapsto L_{\bm{y}}(f):=\sum_{\alpha}f_{\alpha}y_{\alpha}.$ (4ruvaaabbrbs) $$

For $d\in\mathbb{N}$, $\bm{M}_{d}(\bm{y})$ denotes the *moment matrix* of order $d$ associated with $\bm{y}$ and defined as follows

$$ $\bm{M}_{d}(\bm{y})({\beta,\gamma}):=L_{\bm{y}}(\bm{x}^{\beta}\bm{x}^{\gamma})= y_{\beta+\gamma},\quad\forall\beta,\gamma\in\mathbb{N}^{n}_{d}.$ (4ruvaaabbrbt) $$

Similarly, for $g=\sum_{\alpha}g_{\alpha}\bm{x}^{\alpha}\in\mathbb{R}[\bm{x}]$, $\bm{M}_{d}(g\bm{y})$ denotes the *localizing matrix* of order $d$ associated with $g$ and $\bm{y}$, defined as follows

$$ $\bm{M}_{d}(g\bm{y})({\beta,\gamma}):=L_{\bm{y}}(g\bm{x}^{\beta}\bm{x}^{\gamma} )=\sum_{\alpha}g_{\alpha}y_{\alpha+\beta+\gamma},\quad\forall\beta,\gamma\in \mathbb{N}^{n}_{d}.$ (4ruvaaabbrbu) $$

When the correlative sparsity is present, analogous hierarchies of sparse moment relaxations can be derived as well [LasserreCSP2006, MagronSpop2023]. Such reasoning was adopted in the following proof of Theorem LABEL:Thm:Hardness_first_order.

###### Proof of Theorem LABEL:Thm:Hardness_first_order .

Let $j\in\llbracket 1\mkern 1.5mu,\mkern 1.5mun_{L}\rrbracket$ and $c_{j}^{L}=\operatorname{nv}(\bm{W}^{[L]})_{j}+\bm{b}_{j}^{[L]}$ and define $f(\bm{x}^{0},\bm{x}^{1},\dots,\bm{x}^{L}):=\bm{x}^{L}_{j}-\left(\frac{2}{c_{j}
^{L}}\left(\left\langle\bm{W}^{[L]}_{(j:,)},\bm{x}^{L-1}\right\rangle+\bm{b}_{
j}^{[L]}\right)-1\right)$. Then,

$$ $\displaystyle\bm{M}=\hbox{}\vbox{\kern 0.86108pt\hbox{$\kern 0.0pt\kern 2.5pt \kern-5.0pt\left[\kern 0.0pt\kern-2.5pt\kern-5.55557pt\vbox{\kern-0.86108pt \vbox{\vbox{ \halign{\kern\arraycolsep\hfil\@arstrut$\kbcolstyle#$\hfil\kern\arraycolsep& \kern\arraycolsep\hfil$\@kbrowstyle#$\ifkbalignright\relax\else\hfil\fi\kern \arraycolsep&& \kern\arraycolsep\hfil$\@kbrowstyle#$\ifkbalignright\relax\else\hfil\fi\kern \arraycolsep\cr 5.0pt\hfil\@arstrut$\scriptstyle$\hfil\kern 5.0pt&5.0pt\hfil$ \scriptstyle 1$\hfil\kern 5.0pt&5.0pt\hfil$\scriptstyle\bm{x}^{L-1}$\hfil\kern 5 .0pt&5.0pt\hfil$\scriptstyle\bm{x}^{L}_{j}\\1$\hfil\kern 5.0pt&5.0pt\hfil$ \scriptstyle 1$\hfil\kern 5.0pt&5.0pt\hfil$\scriptstyle\left(\bm{W}^{[L]}_{(j: ,)}\right)^{\intercal}$\hfil\kern 5.0pt&5.0pt\hfil$\scriptstyle 0$\hfil\kern 5 .0pt&5.0pt\hfil$\scriptstyle\\\bm{x}^{L-1}$\hfil\kern 5.0pt&5.0pt\hfil$ \scriptstyle\bm{W}^{[L]}_{(j:,)}$\hfil\kern 5.0pt&5.0pt\hfil$\scriptstyle\bm{W }^{[L]}_{(j:,)}\left(\bm{W}^{[L]}_{(j:,)}\right)^{\intercal}$\hfil\kern 5.0pt& 5.0pt\hfil$\scriptstyle\bm{0}$\hfil\kern 5.0pt&5.0pt\hfil$\scriptstyle\\\bm{x} ^{L}_{j}$\hfil\kern 5.0pt&5.0pt\hfil$\scriptstyle 0$\hfil\kern 5.0pt&5.0pt \hfil$\scriptstyle\bm{0}$\hfil\kern 5.0pt&5.0pt\hfil$\scriptstyle 1$\hfil\kern 5 .0pt&5.0pt\hfil$\scriptstyle$\hfil\kern 5.0pt\crcr}}}}\right]$}}$ (4ruvaaabbrbw) $$

represents a feasible moment matrix for the sparse first-order moment relaxation of (LABEL:stdBNNV-prob), yielding the value of the objective function equal to $-1$ (because $||\bm{W}^{[L]}_{(j:,)}||_{2}^{2}=\operatorname{nv}(\bm{W}^{[L]})_{j})$, implying that $\tau^{1}\leq-1$.
However, since $f(\bm{x}^{0},\bm{x}^{1},\dots,\bm{x}^{L})\geq 0$ is one of the constraints in (LABEL:LP-relaxed-BNN), we deduce that $\tau_{\text{LP}}\geq 0$.
∎

As a direct consequence of Theorem LABEL:Thm:Hardness_first_order, we have the following corollary:

###### Corollary A.1.1 .

Consider an arbitrary BNN with depth $L\geq 2$, and let $j\in\llbracket 1\mkern 1.5mu,\mkern 1.5mun_{L}\rrbracket$. Then,

$$ $\bm{g}^{1}_{L,\text{LIN}}(\cdot)_{j}\notin\mathcal{Q}_{1}(\{\bm{g}_{L}(\cdot)_ {j}\}),$ (4ruvaaabbrbx) $$

thus the set $\left\{\bm{g}^{0}_{i,\text{LIN}},\bm{g}^{1}_{i,\text{LIN}},\bm{g}^{2}_{i,\text
{LIN}},i\in\llbracket 1\mkern 1.5mu,\mkern 1.5muL\rrbracket\right\}$
is not included in $\mathcal{Q}_{1}(\{\bm{g}_{1},\dots,\bm{g}_{L},\bm{g}_{\bm{B}}\})$.

###### Proof of Theorem LABEL:Thm:Hardness_first_order .

###### Corollary A.1.1 .

### A.2 Bounds from the second-order relaxation

###### Theorem A.2.1 .

If $(\bm{x}^{0},\bm{x}^{1},\dots,\bm{x}^{L})\mapsto f(\bm{x}^{0},\bm{x}^{1},\dots,
\bm{x}^{L})$ is affine, we have $\tau\geq\tau^{2}\geq\tau_{\textsc{LP}}$. Consequently, any dual-feasible solution of (LABEL:LP-relaxed-BNN) yields a valid SOS decomposition for the second-order SDP relaxation of (LABEL:stdBNNV-prob).

###### Proof of Theorem A.2.1 .

We proceed by analyzing the feasible sets of each problem. Firstly, both problems share the same input perturbation region given by (LABEL:constr_-_PerturbationLP). For the remaining constraints, let us consider three different cases:
(i) Single node bounds: Let $i\in\llbracket 1\mkern 1.5mu,\mkern 1.5muL\rrbracket$ and $j\in\llbracket 1\mkern 1.5mu,\mkern 1.5mun_{i}\rrbracket$. Then, the following equations on $\mathbb{R}[\bm{x}^{i}]$ hold true:

$$ $\displaystyle\bm{g}^{0}_{i,\text{LIN}}(\bm{x}^{i})_{j}=\frac{1}{2}(1-\bm{x}^{i }_{j})^{2}+\frac{1}{2}\bm{h}_{i}(\bm{x}^{i})_{j},\phantom{,}\text{and}\phantom {.}\bm{g}^{0}_{i,\text{LIN}}(\bm{x}^{i})_{n_{i}+j}=\frac{1}{2}(\bm{x}^{i}_{j}+ 1)^{2}+\frac{1}{2}\bm{h}_{i}(\bm{x}^{i})_{j}.$ (4ruvaaabbrby) $$

Thus $\{\bm{g}^{0}_{i,\text{LIN}},i\in\llbracket 1\mkern 1.5mu,\mkern 1.5muL
\rrbracket\}\subset\mathcal{Q}_{2}(\{\bm{g}_{1},\dots,\bm{g}_{L},\bm{g}_{\bm{B
}}\})$. \\
(ii) Interaction between two adjacent hidden layers: Fix $i\in\llbracket 2\mkern 1.5mu,\mkern 1.5muL\rrbracket$ and $j\in\llbracket 1\mkern 1.5mu,\mkern 1.5mun_{i}\rrbracket$. Let us define $c_{\pm,j}^{i}:=\operatorname{nv}(\bm{W}^{[i]})_{j}\pm\bm{b}^{[i]}_{j}>0$.
If we apply the substitution rules $\bm{x}^{i-1}\odot\bm{x}^{i-1}=\bm{1}$ and $(\bm{x}^{i}_{j})^{2}=1$, then the following equations always hold true on $\mathbb{R}[\bm{x}^{i-1},\bm{x}^{i}_{j}]$:

$$ $\displaystyle\bm{g}^{1}_{i,\text{LIN}}(\bm{x}^{i},\bm{x}^{i-1})_{j}=\frac{(1- \bm{x}^{i}_{j})^{2}}{2c_{+,j}^{i}}\bm{g}_{i}(\bm{x}^{i},\bm{x}^{i-1})_{j}+ \frac{(1+\bm{x}^{i}_{j})^{2}}{4c_{+,j}^{i}}\sum_{k=1}^{n_{i-1}}\left(1-\bm{W}^ {[i]}_{j,k}\bm{x}^{i-1}_{k}\right)^{2},$ (4ruvaaabbrbz) $$

$$ $\displaystyle\bm{g}^{2}_{i,\text{LIN}}(\bm{x}^{i},\bm{x}^{i-1})_{j}=\frac{(1+ \bm{x}^{i}_{j})^{2}}{2c_{-,j}^{i}}\bm{g}_{i}(\bm{x}^{i},\bm{x}^{i-1})_{j}+ \frac{(1-\bm{x}^{i}_{j})^{2}}{4c_{-,j}^{i}}\sum_{k=1}^{n_{i-1}}\left(1+\bm{W}^ {[i]}_{j,k}\bm{x}^{i-1}_{k}\right)^{2}.$ (4ruvaaabbrca) $$

Equations (4ruvaaabbrbz) and (4ruvaaabbrca) certify that
$\{\bm{g}^{1}_{i,\text{LIN}},\bm{g}^{2}_{i,\text{LIN}},i\in\llbracket 1\mkern 1
.5mu,\mkern 1.5muL\rrbracket\}\subset\mathcal{Q}_{2}(\{\bm{g}_{1},\dots,\bm{g}
_{L},\bm{g}_{\bm{B}}\})$. \\
\\(iii) Interaction between the input layer and the first hidden layer:
For any $j\in\llbracket 1\mkern 1.5mu,\mkern 1.5mun_{1}\rrbracket$, let us define $c_{\pm,j}^{1}:=\operatorname{nv}(\bm{W}^{[1]})_{j}\pm\bm{b}^{[1]}_{j}>0$. It follows that

$$ $\displaystyle\bm{g}^{1}_{1,\text{LIN}}(\bm{x}^{1},\bm{x}^{0})_{j}=\frac{(1-\bm {x}^{1}_{j})^{2}}{2c_{+,j}^{1}}\bm{g}_{1}(\bm{x}^{0},\bm{x}^{1})_{j}+\frac{(1+ \bm{x}^{1}_{j})^{2}}{2c_{+,j}^{1}}\sum_{k=1}^{n_{0}}\left(\left|\bm{W}^{[1]}_{ j,k}\right|-\bm{W}^{[1]}_{j,k}\bm{x}^{0}_{k}\right),$ (4ruvaaabbrcb) $$

$$ $\displaystyle\bm{g}^{2}_{1,\text{LIN}}(\bm{x}^{1},\bm{x}^{0})_{j}=\frac{(1+\bm {x}^{1}_{j})^{2}}{2c_{-,j}^{1}}\bm{g}_{1}(\bm{x}^{0},\bm{x}^{1})_{j}+\frac{(1- \bm{x}^{1}_{j})^{2}}{2c_{-,j}^{1}}\sum_{k=1}^{n_{0}}\left(\left|\bm{W}^{[1]}_{ j,k}\right|+\bm{W}^{[1]}_{j,k}\bm{x}^{0}_{k}\right),$ (4ruvaaabbrcc) $$

provide the $\mathcal{Q}_{2}\left(\{\bm{g}_{1}(\cdot)_{j}\}\right)$-based representations for $\bm{g}^{1}_{1,\text{LIN}}(\cdot)_{j}$ and $\bm{g}^{2}_{1,\text{LIN}}(\cdot)_{j}$, valid after substituting $(\bm{x}^{1}_{j})^{2}=1$.
∎

###### Example A.2.1 (Illustration of Theorem A.2.1 ) .

This theorem indicates that any dual-feasible solution of (LABEL:LP-relaxed-BNN) provides a feasible solution for the second-order SOS relaxation (LABEL:QCQPBNN-SDPrelaxation) of QCQP (LABEL:stdBNNV-prob).
For instance, let us consider the toy BNN from Example (LABEL:ToyBNN-exampleIntro). Recall that we aim to minimize the linear function $f_{1}^{\operatorname{adv}}(\bm{x})=2\bm{x}^{2}_{2}-1$. Since the
LP relaxation problem has following constraints:

$$ $\displaystyle-\frac{4\,\bm{x}^{1}_{2}}{3}+\frac{4\,\bm{x}^{1}_{1}}{3}+\bm{x}^{ 2}_{2}\geq-\frac{5}{3},~{}-\bm{x}^{1}_{1}\geq-1,~{}\bm{x}^{1}_{2}\geq-1,~{}\bm {x}^{2}_{2}\geq-1,$ (4ruvaaabbrcd) $$

the expression

$$ $\displaystyle\begin{split}\left(2\bm{x}^{2}_{2}-1\right)+4&=\frac{3}{10}\left( -\frac{4\,\bm{x}^{1}_{2}}{3}+\frac{4\,\bm{x}^{1}_{1}}{3}+\bm{x}^{2}_{2}+\frac{ 5}{3}\right)+\frac{2}{5}\left(-\bm{x}^{1}_{1}+1\right)\\ &+\frac{2}{5}\left(-\bm{x}^{1}_{2}+1\right)+\frac{17}{10}\left(\bm{x}^{2}_{2}+ 1\right)\geq 0\end{split}$ (4ruvaaabbrce) $$

gives one feasible dual solution of the LP relaxation problem. From this dual solution, we can recover the following SOS decomposition, certifying that $f_{1}^{\operatorname{adv}}\geq-3$:

$$ $\begin{split}\left(2\bm{x}^{2}_{2}-1\right)+4&=\frac{3}{10}\left(\frac{2}{3}( \bm{x}^{2}_{2}-1)\left(\bm{x}^{1}_{2}-\bm{x}^{1}_{1}-\frac{1}{2}\right)+\frac{ 2}{3}(1+\bm{x}^{2}_{2})(2-\bm{x}^{1}_{2}+\bm{x}^{1}_{1})\right)\\ &+\frac{2}{5}\cdot\frac{1}{2}\left(1-\bm{x}^{1}_{1}\right)^{2}+\frac{2}{5} \cdot\frac{1}{2}\left(1+\bm{x}^{1}_{2}\right)^{2}+\frac{17}{10}\cdot\frac{1}{2 }\left(1+\bm{x}^{2}_{2}\right)^{2}.\end{split}$ (4ruvaaabbrcf) $$

###### Theorem A.2.1 .

###### Proof of Theorem A.2.1 .

###### Example A.2.1 (Illustration of Theorem A.2.1 ) .

### A.3 Importance of tautologies

###### Proof of Theorem LABEL:Thm:adding-tautology .

Since all the variables are bounded, we have $\tau^{1}_{\operatorname{tighter},\operatorname{cs}}=\tau^{1}_{\operatorname{
tighter}}$. Moreover, the inequality $\tau^{1}_{\operatorname{tighter},\operatorname{cs}}\geq\tau^{1}$ is a consequence of the identity

$$ $\displaystyle\bm{g}_{i}(\bm{x}^{i},\bm{x}^{i-1})=\frac{1}{2}\tilde{\bm{g}}^{1} _{i}(\bm{x}^{i},\bm{x}^{i-1})+\frac{1}{2}\tilde{\bm{g}}^{2}_{i}(\bm{x}^{i},\bm {x}^{i-1}),\>i\in\llbracket 2\mkern 1.5mu,\mkern 1.5muL\rrbracket$ $$

In order to prove that $\tau^{1}_{\operatorname{tighter},\operatorname{cs}}\geq\tau_{\text{LP}}$ holds, we show that all linear functions $\bm{g}^{1}_{i,\text{LIN}},\bm{g}^{2}_{i,\text{LIN}},i\in\llbracket 1\mkern 1.5
mu,\mkern 1.5muL\rrbracket$, involved in the constraints (LABEL:LIN1-MILP) and (LABEL:LIN2-MILP) belong to
$\mathcal{Q}_{1}(\{\tilde{\bm{g}}^{1}_{i},\tilde{\bm{g}}^{2}_{i},\tilde{\bm{g}}
^{\text{t1}}_{i},\tilde{\bm{g}}^{\text{t2}}_{i},i\in\llbracket 1\mkern 1.5mu,
\mkern 1.5muL\rrbracket\})$.
We consider two different scenarios:
(i)  Let $i\in\llbracket 2\mkern 1.5mu,\mkern 1.5muL\rrbracket$, $j\in\llbracket 1\mkern 1.5mu,\mkern 1.5mun_{i}\rrbracket$ and $c_{\pm,j}^{i}:=\operatorname{nv}(\bm{W}^{[i]})_{j}\pm\bm{b}^{[i]}_{j}>0$. When we apply the substitution rules $\bm{x}^{i-1}\odot\bm{x}^{i-1}=\bm{1}$ and $(\bm{x}^{i}_{j})^{2}=1$, then the following equations always hold true on $\mathbb{R}[\bm{x}^{i-1},\bm{x}^{i}_{j}]$:

$$ $\displaystyle\bm{g}^{1}_{i,\text{LIN}}(\bm{x}^{i},\bm{x}^{i-1})_{j}=\frac{1}{c _{+,j}^{i}}\tilde{\bm{g}}^{2}_{i}(\bm{x}^{i},\bm{x}^{i-1})_{j}\color[rgb]{ 0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke {0}\pgfsys@color@gray@fill{0}+\frac{1}{c_{+,j}^{i}}\tilde{\bm{g}}^{\text{t1}}_ {i}(\bm{x}^{i},\bm{x}^{i-1})_{j},$ (4ruvaaabbrcg) $$

$$ $\displaystyle\bm{g}^{2}_{i,\text{LIN}}(\bm{x}^{i},\bm{x}^{i-1})_{j}=\frac{1}{c _{-,j}^{i}}\tilde{\bm{g}}^{1}_{i}(\bm{x}^{i},\bm{x}^{i-1})_{j}\color[rgb]{ 0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke {0}\pgfsys@color@gray@fill{0}+\frac{1}{c_{-,j}^{i}}\tilde{\bm{g}}^{\text{t2}}_ {i}(\bm{x}^{i},\bm{x}^{i-1})_{j}.$ (4ruvaaabbrch) $$

(ii)  Secondly, for any $j\in\llbracket 1\mkern 1.5mu,\mkern 1.5mun_{1}\rrbracket$, and $c_{\pm,j}^{1}=\operatorname{nv}(\bm{W}^{[1]})_{j}\pm\bm{b}^{[1]}_{j}>0$, substituting $(\bm{x}^{1}_{j})^{2}=1$ yields the following equalities on $\mathbb{R}[\bm{x}^{0},\bm{x}^{1}_{j}]$:

$$ $\displaystyle\bm{g}^{1}_{1,\text{LIN}}(\bm{x}^{1},\bm{x}^{0})_{j}=\frac{1}{c_{ +,j}^{1}}\bm{g}_{2}(\bm{x}^{1},\bm{x}^{0})_{j}\color[rgb]{0,0,0}\definecolor[ named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0} \pgfsys@color@gray@fill{0}+\frac{1}{c_{+,j}^{1}}\tilde{\bm{g}}^{\text{t2}}_{1} (\bm{x}^{1},\bm{x}^{0})_{j},$ (4ruvaaabbrci) $$

$$ $\displaystyle\bm{g}^{2}_{1,\text{LIN}}(\bm{x}^{1},\bm{x}^{0})_{j}=\frac{1}{c_{ +,j}^{1}}\bm{g}_{1}(\bm{x}^{1},\bm{x}^{0})_{j}\color[rgb]{0,0,0}\definecolor[ named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0} \pgfsys@color@gray@fill{0}+\frac{1}{c_{+,j}^{1}}\tilde{\bm{g}}^{\text{t1}}_{1} (\bm{x}^{1},\bm{x}^{0})_{j},$ (4ruvaaabbrcj) $$

certifying that $\bm{g}^{1}_{1,\text{LIN}}(\bm{x}^{0},\bm{x}^{1})_{j}$ and $\bm{g}^{2}_{1,\text{LIN}}(\bm{x}^{0},\bm{x}^{1})_{j}$ belong to
$\mathcal{Q}_{1}(\{\tilde{\bm{g}}^{1}_{i},\tilde{\bm{g}}^{2}_{i},\tilde{\bm{g}}
^{\text{t1}}_{i},\tilde{\bm{g}}^{\text{t2}}_{i},i\in\llbracket 1\mkern 1.5mu,
\mkern 1.5muL\rrbracket\})$.

Finally, Theorem LABEL:Thm:Hardness_first_order implies that there exists an affine $f$ such that $\tau^{1}_{\operatorname{tighter},\operatorname{cs}}\geq\tau_{\textsc{LP}}>\tau
^{1}.$

∎

###### Remark A.3.1 .

We insist that tautologies (LABEL:tautology_1) and (LABEL:tautology_2) are both important and necessary. If we consider the optimization problem without tautologies, where only (LABEL:LPofSign-1_bis) and (LABEL:LPofSign-2_bis) are used to replace (LABEL:StandardSign_-_Inequality), then we have the following strict containment relationship:

$$ $\displaystyle\mathcal{Q}_{1}(\{\bm{g}_{\bm{B}},\tilde{\bm{g}}_{i}^{1},\tilde{ \bm{g}}_{i}^{2},i\in\llbracket 1\mkern 1.5mu,\mkern 1.5muL\rrbracket\}) \subsetneqq\mathcal{Q}_{1}(\{\bm{g}_{\bm{B}},\tilde{\bm{g}}^{1}_{i},\tilde{\bm {g}}^{2}_{i},\tilde{\bm{g}}^{\text{t1}}_{i},\tilde{\bm{g}}^{\text{t2}}_{i},i \in\llbracket 1\mkern 1.5mu,\mkern 1.5muL\rrbracket\})$ $$

Indeed, following the same reasoning as in the proof of Theorem LABEL:Thm:Hardness_first_order, we obtain that

$$ $\displaystyle\bm{M}=\hbox{}\vbox{\kern 0.86108pt\hbox{$\kern 0.0pt\kern 2.5pt \kern-5.0pt\left[\kern 0.0pt\kern-2.5pt\kern-5.55557pt\vbox{\kern-0.86108pt \vbox{\vbox{ \halign{\kern\arraycolsep\hfil\@arstrut$\kbcolstyle#$\hfil\kern\arraycolsep& \kern\arraycolsep\hfil$\@kbrowstyle#$\ifkbalignright\relax\else\hfil\fi\kern \arraycolsep&& \kern\arraycolsep\hfil$\@kbrowstyle#$\ifkbalignright\relax\else\hfil\fi\kern \arraycolsep\cr 5.0pt\hfil\@arstrut$\scriptstyle$\hfil\kern 5.0pt&5.0pt\hfil$ \scriptstyle 1$\hfil\kern 5.0pt&5.0pt\hfil$\scriptstyle\bm{x}^{L-1}$\hfil\kern 5 .0pt&5.0pt\hfil$\scriptstyle\bm{x}^{L}_{j}\\1$\hfil\kern 5.0pt&5.0pt\hfil$ \scriptstyle 1$\hfil\kern 5.0pt&5.0pt\hfil$\scriptstyle a\left(\bm{W}^{[L]}_{( j:,)}\right)^{\intercal}$\hfil\kern 5.0pt&5.0pt\hfil$\scriptstyle 0$\hfil\kern 5 .0pt&5.0pt\hfil$\scriptstyle\\\bm{x}^{L-1}$\hfil\kern 5.0pt&5.0pt\hfil$ \scriptstyle a\bm{W}^{[L]}_{(j:,)}$\hfil\kern 5.0pt&5.0pt\hfil$\scriptstyle\bm {W}^{[L]}_{(j:,)}\left(\bm{W}^{[L]}_{(j:,)}\right)^{\intercal}$\hfil\kern 5.0 pt&5.0pt\hfil$\scriptstyle t\bm{W}^{[L]}_{(j:,)}$\hfil\kern 5.0pt&5.0pt\hfil$ \scriptstyle\\\bm{x}^{L}_{j}$\hfil\kern 5.0pt&5.0pt\hfil$\scriptstyle 0$\hfil \kern 5.0pt&5.0pt\hfil$\scriptstyle t\left(\bm{W}^{[L]}_{(j:,)}\right)^{ \intercal}$\hfil\kern 5.0pt&5.0pt\hfil$\scriptstyle 1$\hfil\kern 5.0pt&5.0pt \hfil$\scriptstyle$\hfil\kern 5.0pt\crcr}}}}\right]$}}$ (4ruvaaabbrcl) $$

with $a=\frac{1}{2}\sqrt{2-\frac{\left(\bm{b}^{[L]}_{j}\right)^{2}}{\left(
\operatorname{nv}(\bm{W}^{[L]})_{j}\right)^{2}}}-\frac{\bm{b}^{[L]}_{j}}{2
\operatorname{nv}(\bm{W}^{[L]})_{j}}$ and $t=\sqrt{1-a^{2}}$ is a feasible moment matrix for which the value of the objective function is $-\frac{\operatorname{nv}(\bm{W}^{[L]})_{j}}{\operatorname{nv}(\bm{W}^{[L]})_{j
}+\bm{b}^{[L]}_{j}}\left(\sqrt{2-\frac{\left(\bm{b}^{[L]}_{j}\right)^{2}}{
\left(\operatorname{nv}(\bm{W}^{[L]})_{j}\right)^{2}}}-1\right)<0$. To prove that $\bm{M}$ is positive semidefinite, we observe that $M$ has a $n_{L-1}$-dimensional null space corresponding to the direct sum of the sets $A$ and $B$, where

$$ $\displaystyle\begin{split}A:=&\left\{\left(0,\bm{v},0\right)^{\intercal}\in \mathbb{R}^{n_{L-1}+2}\>\big{|}\>\left<\bm{W}^{[L]}_{(j:,)},\bm{v}\right>=0 \right\},\\ B:=&\left\{\alpha\left(-a\operatorname{nv}(\bm{W}^{[L]})_{j},\bm{W}^{[L]}_{(j: ,)},-t\operatorname{nv}(\bm{W}^{[L]})_{j}\right)^{\intercal}\>\big{|}\>\alpha \in\mathbb{R}\right\}.\end{split}$ (4ruvaaabbrcm) $$

Thus, $\bm{M}$ has $n_{L-1}$ eigenvalues equal to zero, and one eigenvalue equal to $1$ corresponding to the eigenvector $\left(-t,\bm{0},a\right)^{\intercal}$. Since the trace of $\bm{M}$ is $\operatorname{nv}(\bm{W}^{[L]})_{j}+2$, we know that the maximal eigenvalue of $\bm{M}$ is $\operatorname{nv}(\bm{W}^{[L]})_{j}+1$.
Details from the previous discussion can be summarized in the following corollary:

###### Corollary A.3.1 .

Let $i\in\llbracket 2\mkern 1.5mu,\mkern 1.5muL\rrbracket$ and $j\in\llbracket 1\mkern 1.5mu,\mkern 1.5mun_{i}\rrbracket$. If the substitution rule $(\bm{x}^{i}_{j})^{2}=1$ is applied on the space $\mathbb{R}[\bm{x}^{i-1},\bm{x}^{i}_{j}]$,

$$ $\bm{g}^{1}_{i,\text{LIN}}(\cdot)_{j}\notin\mathcal{Q}_{1}(\{\bm{g}_{i}(\cdot)_ {j},\bm{g}^{0}_{i,\text{LIN}}(\cdot)_{j},\bm{g}^{0}_{i,\text{LIN}}(\cdot)_{n_{ i}+j}\}).$ (4ruvaaabbrcn) $$

Moreover, at least one of the polynomials defining the constraints from (LABEL:LPofSign-1_bis)-(LABEL:tautology_2) is not in $\mathcal{Q}_{1}(\{\bm{g}_{i}(\cdot)_{j},\bm{g}^{0}_{i,\text{LIN}}(\cdot)_{j},
\bm{g}^{0}_{i,\text{LIN}}(\cdot)_{n_{i}+j}\})$, and consequently

$$ $\mathcal{Q}_{1}(\{\bm{g}_{i}(\cdot)_{j},\bm{g}^{0}_{i,\text{LIN}}(\cdot)_{j}, \bm{g}^{0}_{i,\text{LIN}}(\cdot)_{n_{i}+j}\})\subsetneqq\mathcal{Q}_{1}(\{ \tilde{\bm{g}}^{1}_{i},\tilde{\bm{g}}^{2}_{i},\tilde{\bm{g}}^{\text{t1}}_{i}, \tilde{\bm{g}}^{\text{t2}}_{i},i\in\llbracket 1\mkern 1.5mu,\mkern 1.5muL \rrbracket\}).$ (4ruvaaabbrco) $$

To illustrate the importance of added tautologies, we report numerical comparison results in Table 3.
The problem $\tau_{\textsc{QCQP+LP}}$ is obtained by adding the linear constraints $(\bm{g}^{1}_{i,\text{LIN}},\bm{g}^{2}_{i,\text{LIN}})_{i\in\llbracket 1\mkern 1
.5mu,\mkern 1.5muL\rrbracket}$ to the original QCQP problem from (LABEL:stdBNNV-prob).
The bound $\tau_{\operatorname{tighter},\operatorname{cs}}^{1}$ is significantly better.

**Table 3: Behaviour of the bound corresponding to the first-order sparse relaxation with and without tautologies. Networks and $\|.\|_{\infty}$ verification instances were generated randomly.**
| Network size | $\tau_{\text{LP}}$ | $\tau_{\operatorname{tighter},\operatorname{cs}}^{1}$ | $\tau^{1}_{\textsc{QCQP+LP}}$ |  |  |  |
| --- | --- | --- | --- | --- | --- | --- |
| bound | $t\>(s)$ | bound | $t\>(s)$ | bound | $t\>(s)$ |  |
| $[100,50,50]$ | -42.20 | 0.03 | -28.74 | 19.59 | -42.00 | 25.10 |
| $[200,50,50]$ | -37.03 | 0.05 | -11.53 | 41.31 | -36.81 | 53.42 |
| $[300,50,50]$ | -40.92 | 0.03 | -20.88 | 69.60 | -40.77 | 70.45 |
| $[100,50,50,50]$ | -35.46 | 0.03 | -3.84 | 60.52 | -35.23 | 72.85 |
| $[200,50,50,50]$ | -34.67 | 0.03 | 1.66 | 67.84 | -34.40 | 73.30 |
| $[300,50,50,50]$ | -40.33 | 0.03 | -20.87 | 83.35 | -40.27 | 102.14 |
| $[100,50,50,50,50]$ | -35.01 | 0.05 | -4.52 | 82.32 | -34.98 | 93.37 |
| $[200,50,50,50,50]$ | -38.41 | 0.04 | -7.77 | 87.12 | -38.32 | 123.86 |
| $[300,50,50,50,50]$ | -38.94 | 0.05 | -13.82 | 109.94 | -38.76 | 140.45 |

###### Proof of Theorem LABEL:Thm:adding-tautology .

###### Remark A.3.1 .

###### Corollary A.3.1 .

### A.4 Cliques structure discussion

Let us describe in details the clique structure of the first-order sparse SDP relaxation of the problem (LABEL:QCQPBNN-refined). 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 a set of cliques $(I_{k})_{k\in\llbracket 1\mkern 1.5mu,\mkern 1.5mup\rrbracket}$ is said to satisfy the RIP property is

$$ $\displaystyle\left(I_{k+1}\cap\cup_{j\leq k}I_{j}\right)\subset I_{i},\>\text{ for some}\>i\leq k.$ (4ruvaaabbrda) $$

The RIP property (4ruvaaabbrda) is one of the essential requirements for the convergence of the sparse SOS-based hierarchy of SDP relaxations (see Assumption 3.1 in [MagronSpop2023]).

###### Theorem A.4.1 .

The clique structure of the standard BNN robustness verification problem is such that:

- •
If $L=1$, there are $n_{0}$ cliques of size $n_{1}+1$, given by $I_{k}=\{\bm{x}^{1}_{1},\dots,\bm{x}^{1}_{n_{1}},\bm{x}^{0}_{k}\},k\in
\llbracket 1\mkern 1.5mu,\mkern 1.5mun_{0}\rrbracket$.
- •
If $L=2$, there are $n_{0}+n_{2}$ cliques of size $n_{1}+1$, given by $I_{k}=\{\bm{x}^{1}_{1},\dots,\bm{x}^{1}_{n_{1}},\bm{x}^{0}_{k}\}$ for $k\in\llbracket 1\mkern 1.5mu,\mkern 1.5mun_{0}\rrbracket$ and $I_{n_{0}+k}=\{\bm{x}^{1}_{1},\dots,\bm{x}^{1}_{n_{1}},\bm{x}^{2}_{k}\}$ for $k\in\llbracket 1\mkern 1.5mu,\mkern 1.5mun_{2}\rrbracket$.
- •
If $L\geq 3$, there are $L-2+n_{0}+n_{L}$ cliques in total, and the maximum clique size is given by $\max\{n_{1}+1,n_{L-1}+1,\max_{j\leq L-2}\{n_{j}+n_{j+1}\}\}$. The cliques are given by $I_{k}=\{\bm{x}^{k}_{1},\dots,\bm{x}^{k}_{n_{k}},\bm{x}^{k+1}_{1},\dots,\bm{x}^
{k+1}_{n_{k+1}}\}$ for $k\in\llbracket 1\mkern 1.5mu,\mkern 1.5muL-2\rrbracket$, $I_{L-2+k}=\{\bm{x}^{0}_{k},\bm{x}^{1}_{1},\dots,\bm{x}^{1}_{n_{1}}\}$ for $k\in\llbracket 1\mkern 1.5mu,\mkern 1.5mun_{0}\rrbracket$ and $I_{L-2+n_{0}+k}=\{\bm{x}^{L-1}_{1},\dots,\bm{x}^{L-1}_{n_{L-1}},\bm{x}^{L}_{k}\}$ for $k\in\llbracket 1\mkern 1.5mu,\mkern 1.5mun_{L}\rrbracket$.

In any of the three cases, the defined clique structure satisfies the RIP property.

###### Proof of Theorem A.4.1 .

We consider different cases, depending on the depth of the BNN:

- •
$L=1$: All the nodes from the hidden layer form a separate clique with each individual input node, resulting in $n_{0}$ cliques of size $n_{1}+1$. Thus, we can set $I_{k}=\{\bm{x}^{1}_{1},\dots,\bm{x}^{1}_{n_{1}},\bm{x}^{0}_{k}\}$, for $k\in\llbracket 1\mkern 1.5mu,\mkern 1.5mun_{0}\rrbracket$. The RIP property is clearly satisfied, as the nodes from the hidden layer appear in each clique.
- •
$L=2$: All the nodes from the first hidden layer form a separate clique with each individual input node, resulting in $n_{0}$ cliques of size $n_{1}+1$. Thus, we can set $I_{k}=\{\bm{x}^{1}_{1},\dots,\bm{x}^{1}_{n_{1}},\bm{x}^{0}_{k}\}$, for $k\in\llbracket 1\mkern 1.5mu,\mkern 1.5mun_{0}\rrbracket$. Moreover, they also form a separate clique with each individual node from the second hidden layer, resulting in $n_{2}$ cliques of size $n_{1}+1$. Thus, we can set $I_{n_{0}+k}=\{\bm{x}^{1}_{1},\dots,\bm{x}^{1}_{n_{1}},\bm{x}^{2}_{k}\}$, for $k\in\llbracket 1\mkern 1.5mu,\mkern 1.5mun_{2}\rrbracket$. The RIP property is satisfied as the first hidden layer nodes appear in each clique.
- •
$L\geq 3$: For every $k\in\llbracket 1\mkern 1.5mu,\mkern 1.5muL-2\rrbracket$, a pair $(k,k+1)$ of adjacent hidden layers forms a clique $I_{k}=\{\bm{x}^{k}_{1},\dots,\bm{x}^{k}_{n_{k}},\bm{x}^{k+1}_{1},\dots,\bm{x}^
{k+1}_{n_{k+1}}\}$ of size $n_{k}+n_{k+1}$.
Furthermore, all the nodes from the first hidden layer form a separate clique with each individual input node, resulting in $n_{0}$ cliques of size $n_{1}+1$. Thus, we can set $I_{L-2+k}=\{\bm{x}^{1}_{1},\dots,\bm{x}^{1}_{n_{1}},\bm{x}^{0}_{k}\}$, for $k\in\llbracket 1\mkern 1.5mu,\mkern 1.5mun_{0}\rrbracket$.
Finally, all the nodes from the penultimate hidden layer form a separate clique with each individual node from the last hidden layer, resulting in $n_{L}$ cliques of size $n_{L-1}+1$. Thus, we can set $I_{L-2+n_{0}+k}=\{\bm{x}^{L-1}_{1},\dots,\bm{x}^{L-1}_{n_{L-1}},\bm{x}^{L}_{k}\}$, for $k\in\llbracket 1\mkern 1.5mu,\mkern 1.5mun_{L}\rrbracket$.\\
\\
Therefore, there are $L-2+n_{0}+n_{L}$ cliques in total, and the maximum clique size is given by $\max\{n_{1}+1,n_{L-1}+1,\max_{j\leq L-2}\{n_{j}+n_{j+1}\}\}$. Moreover, given this particular clique ordering (enumeration), the RIP property is satisfied. Indeed,
–
If $k\in\llbracket 2\mkern 1.5mu,\mkern 1.5muL-2\rrbracket$, then $I_{k}\cap\left(\cup_{j\leq k-1}I_{j}\right)=\{\bm{x}^{k-1}_{1},\dots,\bm{x}^{k
-1}_{n_{k-1}}\}\subset I_{k-1}$.
–
If $k\in\llbracket L-2+1\mkern 1.5mu,\mkern 1.5muL-2+n_{0}\rrbracket$, then $I_{k}\cap\left(\cup_{j\leq k-1}I_{j}\right)=\{\bm{x}^{1}_{1},\dots,\bm{x}^{1}_
{n_{1}}\}\subset I_{1}$.
–
If $k\in\llbracket L-2+n_{0}+1\mkern 1.5mu,\mkern 1.5muL-2+n_{0}+n_{L}\rrbracket$, then $I_{k}\cap\left(\cup_{j\leq k-1}I_{j}\right)=\{\bm{x}^{L-1}_{1},\dots,\bm{x}^{L
-1}_{n_{L-1}}\}\subset I_{L-2}$.

∎

An alternative clique structure, independent of the depth of the BNN, is to consider the cliques $\{\bm{x}^{i-1}_{j},\bm{x}^{i}_{k}\}^{1\leq i\leq L}_{1\leq j\leq n_{i-1},1\leq
k
\leq n_{i}}$. This option results in $\sum_{i=1}^{L}n_{i-1}\times n_{i}$ cliques of size two, since every node is coupled with all the other nodes form adjacent layers. The RIP property always holds in this case if cliques are enumerated in an order that mirrors the feed-forward structure of the BNN. Computations are generally faster for this clique structure, but the obtained bounds are much coarser.

###### Theorem A.4.1 .

###### Proof of Theorem A.4.1 .

## Appendix 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 [Geiger2020larq], an 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 [Kingma2014AdamAM].
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 to induce different sparsities of the weights matrices. Network parameters have been initialized from a uniform distribution.
Batch normalization layers have been added to all but the output layer. \\
All networks have achieved over $95\%$ accuracy on the test set.

#### Optimization details:

Semidefinite Programming (SDP) problems have been assembled using TSSOS [TSSOS2021], a 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 clique structure.
The SDP values have been computed via the interior-point solver Mosek [andersen2000mosek], 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 to zero, and adding $f(\cdot)\leq 0$ to the set of constraints. Infeasibility of the resulting problem provides a certificate of robustness.
These problems have then been solved using Gurobi, where the time limit was set to $600$ seconds. The upper bound presented in Figure LABEL:fig:epsilon_comparison 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 at [https://github.com/jty-AMSS/POP4BNN](https://github.com/jty-AMSS/POP4BNN).

#### More detailed experimental results:

We provide detailed verification results against $||.||_{\infty}$ (see Table 4 and Table 5) and $||.||_{2}$ (see Table 6 and Table 7) attacks.
Those results illustrate that the solving time of general branch and bound algorithms could be significantly improved if the LP bounds would be replaced by tighter SDP bounds, such as $\tau_{\operatorname{tighter},\operatorname{cs}}^{1}$. The improvement would be even more noticeable for $\|.\|_{2}$ verification.

**Table 4: Verification against $\|.\|_{\infty}$-attacks: detailed numerical results for $\textsc{BNN}_{1}:[784,500,500,10],w_{s}=34.34\%$. For example, image 72 illustrates that MILP methods can not handle severe attacks. Likewise, image 28 confirms the potential benefits of accommodating $\tau_{\operatorname{tighter},\operatorname{cs}}^{1}$ 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 | $\tau_{\operatorname{tighter},\operatorname{cs}}^{1}$ | $\tau_{\text{Soft-MILP}}$ |  |  |
| --- | --- | --- | --- | --- |
| bound | $t\>(s)$ | bound | $t\>(s)$ |  |
| $\delta_{||.||_{\infty}}=1.25$ |  |  |  |  |
| 14 | 1.08 | 11.53 | infeasible | 552.99 |
| 24 | 5.82 | 15.43 | timeout | $>600$ |
| 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 |
| $\delta_{||.||_{\infty}}=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 |
| $\delta_{||.||_{\infty}}=1.75$ |  |  |  |  |
| 28 | 0.20 | 42.46 | timeout | $>600$ |
| 72 | 13.50 | 37.79 | timeout | $>600$ |
| 83 | 22.14 | 44.61 | infeasible | 16.26 |

**Table 5: Verification against $\|.\|_{\infty}$-attacks: detailed numerical results for $\textsc{BNN}_{2}:[784,500,500,10],w_{s}=19.07\%$. Remarkable improvements can be observed for images $20,28,29$ and $33$.**
| Image Index | $\tau_{\operatorname{tighter},\operatorname{cs}}^{1}$ | $\tau_{\text{Soft-MILP}}$ |  |  |
| --- | --- | --- | --- | --- |
| bound | $t\>(s)$ | bound | $t\>(s)$ |  |
| $\delta_{||.||_{\infty}}=0.75$ |  |  |  |  |
| 11 | 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 |
| 33 | 7.31 | 49.35 | timeout | $>600$ |
| 55 | 25.14 | 28.96 | infeasible | 4.67 |
| 72 | 35.33 | 35.80 | infeasible | 6.85 |
| 83 | 22.14 | 44.61 | infeasible | 16.26 |

**Table 6: Verification against $\|.\|_{2}$-attacks: detailed numerical results for $\textsc{BNN}_{1}:[784,500,500,10],w_{s}=34.34\%$. Notice that the number of timeouts is significant. On the other hand, the verification time associated to $\tau^{1}_{\operatorname{tighter},\operatorname{cs}}$ remains relatively stable.**
| Image Index | $\tau_{\operatorname{tighter},\operatorname{cs}}^{1}$ | $\tau_{\text{Soft-MINP}}$ |  |  |
| --- | --- | --- | --- | --- |
| bound | $t\>(s)$ | bound | $t\>(s)$ |  |
| $\delta_{\|.\|_{2}}=20$ |  |  |  |  |
| 4 | 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 | $>600$ |
| 94 | 7.13 | 14.75 | infeasible | 62.56 |
| 98 | 2.64 | 13.02 | infeasible | 165.10 |
| 99 | 13.27 | 12.16 | infeasible | 100.43 |
| 100 | 42.32 | 8.95 | infeasible | 0.09 |
| $\delta_{\|.\|_{2}}=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 |

**Table 7: Verification against $\|.\|_{2}$-attacks: detailed numerical results for $\textsc{BNN}_{2}:[784,500,500,10],w_{s}=19.07\%$. Images 57 and 89 demonstrate that $\tau_{\operatorname{tighter},\operatorname{cs}}^{1}$ can typically certify robustness more than 20 times faster.**
| Image Index | $\tau_{\operatorname{tighter},\operatorname{cs}}^{1}$ | $\tau_{\text{Soft-MINP}}$ |  |  |
| --- | --- | --- | --- | --- |
| bound | $t\>(s)$ | bound | $t\>(s)$ |  |
| $\delta_{\|.\|_{2}}=15$ |  |  |  |  |
| 2 | 2.74 | 31.34 | infeasible | 279.66 |
| 4 | 0.14 | 47.94 | timeout | $>600$ |
| 11 | 50.95 | 17.32 | infeasible | 12.99 |
| 14 | 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 |

## Peer Reviews

confidence: 3
contribution: 3
initial_rating: 6
presentation: 3
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.
soundness: 3
strengths: -  Introduces a new SDP-based approach that enhances the scalability and precsion of BNN verification.
 - Efficiently handles continuous input spaces without requiring input quantization.
 -  Theoretical contributions, including tighter SDP relaxations, improve the accuracy of robustness bounds.
  - Experimental validation across benchmarks highlights the method’s advantages in speed and robustness certification.
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.
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.

---

confidence: 3
contribution: 3
initial_rating: 6
presentation: 3
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?
soundness: 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.

2. **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.

3. **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.

4. **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.
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.
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.

4. **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.

---

confidence: 4
contribution: 2
initial_rating: 3
presentation: 3
questions: See the weakness raised in **Weaknesses**.

Other minor comments:

- I failed to find the explanation for what the data in parentheses in Column $\tau_{tighter,cs}^1$ represent in Tables 1 and 2.
- 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.
soundness: 3
strengths: - The problem (verification of Transformers) is important.
- A novel method based on SDP to verify the robustness of BNN.
- Compared to LP-based methods, a more precise lower bound is obtained.
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.
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.
- 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.
- For $L_\infty$ experiments, it would be beneficial to include comparisons with other SOTA methods, such as the SMT-based approach (Amir et al.). 
- As Gurobi supports multi-threaded solving, presenting experimental results on multiple threads would also strengthen the evaluation.
- 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).

---

confidence: 3
contribution: 3
initial_rating: 6
presentation: 2
questions: - Can you provide the missing details about the evaluation I mentioned above?
- 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?
- Why can the weights take values {-1,0,1} but the bias any value in |R?
- Why does you appraoch not suffer from floating-point inaccuracies?
soundness: 2
strengths: - the considered problem is highly relevant
- deep theoretical analysis that goes beyond simple linear relaxations and rather design the verification algorithm to exploit certain properties of the considered network architecture
- The theoretical results show strictly better bounds (Thm. 3.1 & 4.1), which proves the point of using the more complex verification algorithm.
- 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.
summary: The paper considers the formal verification of binary neural networks in the classification setting.
Formal verification is necessary as (any) neural network is inherently prone to adversarial attacks.
In the paper, the robustness of binary neural networks is verified using semidefinite programming derived from polynomial optimizations.
In 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.
The 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.
weaknesses: Main points:
It 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:
- 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). 
- 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).
- 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. 
- Steps to derive the constraints are rather quick and more explanations could help to follow along

Additionally, 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.

Minor points:
- 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)).
- 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.
- 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.
- Similarily, give an intuitive explanation why adding those tautologies are necessary
- Only the classification setting is considered. This could be stated more clearly.
- 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.
- Fig 2: misses a label and ticks of the x axis.
- no repeatability package is provided

Further points that could help improve the paper but did not directly influence the score:
- give a real-life example where binary neural networks are used and verifying the robustness is necessary
- 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.

Meta-review: The paper proposes a new approach for verifying binary neural networks. It is based on a novel formulation of semidefinite programming (SDP), derived from sparse polynomial optimization. The angle to develop this new formulation is novel, and the paper also includes good insights on how it compares to linear programming and how to strengthen this formulation. The numerical results are also promising, although conducted on limited settings only. The AC believes the theoretical contribution is novel and sufficient for publication.

The AC shares the same opinion as Reviewer o79c that **more related work from the broad neural network verification community should be discussed in this paper** in Section 1.2 (VNN-COMP reports should be good starting points to find relevant references). The current scope of related work is too narrow.

Decision: Accept (Poster)