Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization
Binary Neural Networks;Sparse Polynomial Optimization;Semidefinite Programming;Robustness Verification
Yes
/
No ethics review needed.
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.
-  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.
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.
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.
Yes
No ethics review needed.
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?
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.
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.
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.
Yes
No ethics review needed.
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.
- 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.
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.
- 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).
Yes
No ethics review needed.
- 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?
- 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.
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.
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.
@inproceedings{
anonymous2024verifying,
title={Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization},
author={Anonymous},
booktitle={Submitted to The Thirteenth International Conference on Learning Representations},
year={2024},
url={https://openreview.net/forum?id=9c96mGtQVR},
note={under review}
}
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.
I certify that there is no URL (e.g., github page) that could be used to find authors’ identity.
I acknowledge that I and all co-authors of this work have read and commit to adhering to the ICLR Code of Ethics.
Binary Neural Networks Sparse Polynomial Optimization Semidefinite Programming Robustness Verification
I certify that there is no acknowledgement section in this submission for double blind review.
/pdf/c3fca48ffb5fefb03f1a8613c6fda1c2125aba51.pdf
optimization
I understand the reciprocal reviewing requirement as described on https://iclr.cc/Conferences/2025/CallForPapers. If none of the authors are registered as a reviewer, it may result in a desk rejection at the discretion of the program chairs. To request an exception, please complete this form at https://forms.gle/Huojr6VjkFxiQsUp6.
I certify that this submission complies with the submission instructions as described on https://iclr.cc/Conferences/2025/AuthorGuide.
/attachment/55b3eaf02175dc05159d5397f096f8c2ca03cfa1.zip
Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization
ICLR 2025 Conference Submission
ICLR.cc/2025/Conference/Submission