Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization

TL;DR

This work targets robustness verification for Binary Neural Networks (BNNs) under adversarial perturbations with continuous inputs. It encodes the BNN verification problem as a sparse polynomial optimization problem leveraging the semi-algebraic sign activation and solves the first-order SDP relaxation to obtain lower bounds, achieving tighter certificates by adding tautologies to enlarge the first-order quadratic module. The approach yields up to 55% tighter bounds than linear relaxations and delivers substantial speedups (e.g., ~4.5x for $\|\cdot\|_\infty$ and ~11.4x for $\|\cdot\|_2$) while handling both $\|\cdot\|_\infty$ and $\|\cdot\|_2$ perturbations in continuous input spaces. These results indicate scalable, rigorous verification for larger BNNs and motivate integrating SDP relaxations into MILP/MINP-based verification pipelines for enhanced performance.

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.

Figures (2)

• Figure 1: A toy BNN with $L=2$ and $(n_0,n_1,n_2,n_3)=(3,2,2,2)$. The subsets of interacting variables $I_1=\{x_{0,1},x_{1,1},x_{1,2}\}, I_2=\{x_{0,2},x_{1,1},x_{1,2}\}, I_3=\{x_{0,3},x_{1,1},x_{1,2}\}$ (represented by red polygons) and $I_4=\{x_{1,1},x_{1,2},x_{2,1}\}, I_5=\{x_{1,1},x_{1,2},x_{2,2}\}$ (represented by blue polygons) are used to compute $\tau^{1}_{\mathop{\mathrm{tighter}}\nolimits, \mathop{\mathrm{cs}}\nolimits}$.
• Figure 2: Comparing $\tau_\textsc{LP}$ and $\tau^{1}_{\mathop{\mathrm{tighter}}\nolimits, \mathop{\mathrm{cs}}\nolimits}$ bounds for $\textsc{BNN}_1$ and different $\delta_{||.||_\infty}$. Each subplot $x$-axis represents indices of test set images sorted in the descending order of $\tau^1_{\mathop{\mathrm{tighter}}\nolimits, \mathop{\mathrm{cs}}\nolimits}$ values. The upper bound $\mathop{\mathrm{ub}}\nolimits$ is obtained by random sampling. The relative improvement over LP is estimated through $\frac{\tau^{1}_{\mathop{\mathrm{tighter}}\nolimits,\mathop{\mathrm{cs}}\nolimits}-\tau_{\textsc{LP}}}{\mathop{\mathrm{ub}}\nolimits-\tau_{\textsc{LP}}}$. On average, $\tau^{1}_{\mathop{\mathrm{tighter}}\nolimits, \mathop{\mathrm{cs}}\nolimits}$ bounds are $21, 33, 46$ and $53$ percent more accurate, respectively.

Theorems & Definitions (8)

• Definition 1.1
• Remark 2.1: Adversarial attacks
• Example 2.1
• Remark 3.1: Encoding of $\operatorname{sign}(\cdot)$
• Theorem 3.1
• proof : Sketch of proof
• Theorem 4.1
• proof : Proof of Theorem \ref{['Thm:Hardness_first_order']}