Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization

Authors: Jianting Yang, Srecko Durasinovic, Jean B. Lasserre, Victor Magron, Jun Zhao
Primary area: optimization
Keywords: Binary Neural Networks, Sparse Polynomial Optimization, Semidefinite Programming, Robustness Verification

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.

Decision: accept (poster)
Reviewer scores: 6, 6, 5, 6

Reviews and discussion:
<thread>
creation date:
1729757962944

thread_type:
official_review

<thread_object>
creator: reviewer_o79c

<content>
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.

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.

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.

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?
</content>
</thread_object>

</thread>
<thread>
creation date:
1730675980672

thread_type:
official_review

<thread_object>
creator: reviewer_7uz5

<content>
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.

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.

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).

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.
</content>
</thread_object>

</thread>
<thread>
creation date:
1730679898777

thread_type:
official_review

<thread_object>
creator: reviewer_rj7x

<content>
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.

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.

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.

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?
</content>
</thread_object>

</thread>
<thread>
creation date:
1730698290026

thread_type:
official_review

<thread_object>
creator: reviewer_tkgw

<content>
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.

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.

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.

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.
</content>
</thread_object>

</thread>
<thread>
creation date:
1732332545592

thread_type:
official_comment

<thread_object>
creator: authors

<content>
title:
Common Reply - Part 3

comment:
## __Conclusion:__
 For more detailed responses regarding all specific comments, we refer the reviewers to the individual response sections. 

 We greatly appreciate the constructive feedback and will incorporate these insights to enhance the clarity, completeness, and applicability of our work.
</content>
</thread_object>

</thread>
<thread>
creation date:
1732332588526

thread_type:
official_comment

<thread_object>
creator: authors

<content>
title:
Common Reply - Part 2

comment:
### -  __MILP-related:__
Reviewers 7uz5 and o79c  raised concerns about the performance superiority of MILP methods in certain scenarios. MILP/MINP methods are exact (capable of proving both robustness and non-robustness), thus it is not surprising to observe them solving more instances within relatively long  time. Despite this, as displayed in Table 1 and Table 2, the gap in terms of number of solved instances significantly reduces for more severe or  $||.||_2$ attacks, favoring our method. 


To further demonstrate the versatility of our method, we provide additional illustrative experiments involving more complex data sets and larger scale optimization problems, as suggested by reviewers TkGW and Rj7X. More precisely, we introduce  $BNN_3: [3072,5000,800,10], w_s=55.97$%, achieving  the test accuracy of $47.66$% on CIFAR-10 data set.
 

**Table 1: Verifying robustness of BNN_3 on CIFAR-10, for an input region determined by $\delta_{||.||_\infty}=0.2/255$. Data were scaled to $[-1,1]^{3072}$, and a time limitation of $3600 s$ was used.  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 |$\tau_\text{tighter, cs}^{1}$ - bound | $\tau_\text{tighter, cs}^{1}$ - $t\phantom{1}(s)$ | $\tau_{\text{Soft-MILP}}$ - bound | $\tau_{\text{Soft-MILP}}$ - $t\phantom{1}(s)$ |
| --- | --- | --- | --- | --- |
1  | **20.46 (robust)** |  1179.55  |timeout | $>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.92 (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 |-52.82 (unknown) |650.79 |timeout |$>3600$ |



 
As presented in the supplementary Table 1, our approach demonstrates comparable performance even on larger datasets, such as CIFAR-10, and for larger networks involving nearly 9000 neurons.  

Specifically, $\tau_{tighter, cs}^{1}$ proves the robustness of images 1, 2 and 35 at least 3x, 6x, and 5.5x faster, respectively. In contrast, the low quality of LP bounds prevents MILP from providing an answer within a 1-hour time limit. These additional experimental results confirm that our method keeps providing high-quality lower bounds even, even for large-scale problems, which is consistent with the results presented in Table 3 of our paper.
 
However, for instances 8 and 10, our method is unable to provide an answer, while MILP can certify **non-robustness** efficiently. This difference arises because MILP methods do not solve the optimization problems to optimality but instead focus on determining the feasibility of an attack, which is inherently less demanding. 


We believe that incorporating our 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. 

We will include a more comprehensive set of large-scale experiments in the subsequent versions of our work. 

We would also like to emphasize that we did not require branch-and-bound based MILP/MINP methods to compute *exact* optimal values of the involved optimization problems, as it would have resulted in much more timeouts, making this approach impractical. Rather, we required the MILP/MINP solver to stop as soon as the nonnegative bound could be obtained, while the SDP solver was required to compute $\tau_{tighter,cs}^1$ exactly.

To conclude, our approach should be understood to complementary to the exact MILP/MINP approach, especially for providing robustness certificates (not for finding valid adversarial attacks) in cases where the increased complexity of exact computations prevents MILP/MINP from providing a valid answer. Since availability of precise bounds is essential for robustness verification, we believe that our proposed tight and reliable bounds would yield promising result if efficiently coupled with MILP/MINP methods.
</content>
</thread_object>

</thread>
<thread>
creation date:
1732332637258

thread_type:
official_comment

<thread_object>
creator: authors

<content>
title:
Common Reply - Part 1

comment:
## __Strengths:__

We greatly appreciate the reviewers’ recognition of the key strengths of our work. 

Reviewers generally highlighted the relevance of research works attempting to develop scalable verification algorithms that leverage the unique structure of BNNs, avoiding the complexity of exact SAT/SMT/MILP methods.


Both Reviewers o79c and TkGW  noted the strong theoretical foundation and empirical evidence supporting our tight first-order SDP relaxation.


Moreover, reviewers also appreciated the novelty of our method, as we are the first to employ SDP relaxations for BNN verification, effectively exploiting the sparse structure of BNNs and
providing reliable and tighter lower bounds capable of certifying robustness.


The ability to handle $||\cdot||_2$ -attacks and continuous input data was also noted as a significant strength, notably by the reviewers 079c, Rj7X and TkGW. 

## __Limitations:__
 We would also like to express our gratitude to all the reviewers for their meaningful critiques and suggestions. Below, we address some common points and concerns that were raised.
### - __Additional experiments:__
As pointed out by reviewers TkGW and Rj7X, we acknowledge the need for results on deeper networks with more layers and more complex data sets to better understand scalability. At the same time, we are not aware of any scalable methods specifically tailored for BNN verification that can successfully operate on continuous input spaces and handle both $||\cdot||_\infty$ and $||\cdot||_2$ attacks. Our relaxation-based method yields optimization problems with number of constraints being polynomial in the number of (clique) variables, which gives us confidence that for larger-scale problems, it would demonstrate significantly better efficiency compared to existing algorithms such as exact SAT/SMT-based methods. Moreover, we anticipate that while the quality of our bound may degrade with increased network depth, it would still outperform the LP bound used in the MILP approach, as supported by Theorem 4.1 and insights from Table 3 in Appendix A.3. 

Finally, we have included additional experiments (see **Table 1** in **Common Reply - Part 2**)  from the CIFAR-10 data set, with another network of more than 9000 nodes, which is quite important with respect to other methods relevant to our framework. We observe the similar type of behavior of our method - it can provide robustness guarantees for instances where MILP fails due to the extremely increased complexity. 

We hope that our work can inspire further research into developing easily parallelizable and scalable SDP solvers, or BNN-verification-tailored branch-and-bound algorithms, as this would address the raised limitations of our POP-based approach.

### - **Continuous input and $||\cdot||_2$-robustness**
 Relevance of $||\cdot||_2$ attacks and continuous input spaces was questioned by the reviewer 7uz5. However, verifying $||\cdot||_2$ robustness of  neural networks has been widely studied in the standard neural network literature since $||\cdot||_2$ perturbations allow to model attacks with coordinate inter-dependence, which is typical in many real-life cases (blurring, noise, etc...). Additional complexity introduced by these non-linearities prevents most currently available BNN verification tools from being applicable without significant modifications. 

Verifying BNNs on continuous input spaces is uniquely challenging due to joint impact of binary weights, discontinuous activation functions, and increased sensitivity to floating-point errors induced by non-discretization. All these factors make the verification problem highly combinatorial and ill-conditioned, as noted on Line 222. Input quantization, while improving scalability, sacrifices precision, often leading to false negatives or inconsistent results depending on the discretization level. In contrast, our method avoids artificial discretization and provides reliable bounds accounting for all possible input states.
</content>
</thread_object>

</thread>
<thread>
creation date:
1733307613480

thread_type:
official_comment

<thread_object>
creator: authors

<content>
title:
Post-rebuttal Summary

comment:
Dear Reviewers, 

We would like to use this opportunity to provide a short summary following the discussion period.

First of all, we thank you all for your time, valuable feedback and constructive comments. It has been very useful for enhancing the overall quality of our paper.

Secondly, we express our sincere gratitude to the Reviewers for recognizing the strengths of our contribution. 

Specifically, Reviewers 7uz5 and o79c highlighted the significance of addressing the BNN robustness verification problems, while all Reviewers acknowledged the novelty of our approach, which is the *first  SDP relaxation based* BNN verification framework that efficiently exploits the sparse structure of the network. Moreover, our proposed method has a strong theoretical foundation and has been supported experimentally, which has been emphasized by Reviewers  TkGW, Rj7X and o79c. 

Furthermore, our method does not rely on input quantization and is capable of handling various types of adversarial attacks, such as $||\cdot||_2$-norm attacks, which have been studied in the context of general DNN verification, but have never been discussed in BNN verification literature. This distinctive feature in the domain of BNN verification was particularly recognized by Reviewers Rj7X, TkGW, and o79c.

We have also addressed the following important points raised by the Reviewers:

- *Additional results:* Reviewers Rj7X, TkGW, and 7uz5 suggested incorporating additional experiments and comparisons to further substantiate our findings. In response, we included Table 8, containing new results about verification queries from the CIFAR-10 dataset. These results confirm our previous conclusions: exact methods, such as MILP, may be efficient for finding adversarial attacks but *cannot provide certified robustness guarantees* within a relatively short time limitation due to their reliance on extremely coarse LP bounds. Similarly, other exact methods, such as the current SAT-based approaches, are highly dependent on heuristic simplifications introduced by input discretization and assumptions of attack linearity.
- *Continuous input:* In *Detailed Response to Reviewer 7uz5 - Continuation 2*, we have provided stronger arguments supporting the importance of verifying BNNs on continuous input spaces. Indeed, BNNs are typically trained and deployed on continuous data, underscoring the need for verification methods that are compatible with continuous input as well. Input quantization, while used as an artificial heuristic to enhance scalability, fails to account for all possible input configurations. 
- *Other remarks:* The revised version of our paper contains many improvements in phrasing, notations, and overall clarity, which was recognized by the Reviewer o79c. 

We believe that these revisions and additional explanations address your concerns and significantly enhance the clarity and completeness of our paper. Furthermore, we are confident that our work has the potential to convince the research community of the necessity of developing more efficient optimization solvers, thereby facilitating the resolution of many important industrial problems, including the robustness verification of BNNs.

Sincerely,

The Authors
</content>
</thread_object>

</thread>


Metareview:
metareview:
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.