Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization
Authors: Jianting Yang, Srecko Durasinovic, Jean Bernard Lasserre, Victor Magron, Jun ZHAO
ICLR 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We demonstrate the effectiveness of our method in verifying robustness against both . and . 2-based adversarial attacks. NUMERICAL EXPERIMENTS In this section, we provide numerical results for BNN robustness verification problems with respect to different perturbations. All experiments are run on a desktop with a 12-core i7-12700 2.10 GHz CPU and 32GB of RAM. The tightened first-order sparse SDP relaxation is modeled with TSSOS (Magron & Wang, 2021) and solved with Mosek (Andersen & Andersen, 2000). Gurobi (Gurobi Optimization, LLC, 2023) is used to solve MILP. BNNs were trained on standard benchmark datasets, using Larq Geiger & Team (2020). The full experimental setup is detailed in Appendix B. |
| Researcher Affiliation | Academia | Jianting Yang Academy of Mathematics and Systems Science Chinese Academy of Sciences EMAIL Sre cko Đurašinovi c CNRS@CREATE Singapore CCDS, NTU Singapore EMAIL Jean-Bernard Lasserre LAAS-CNRS Toulouse School of Economics EMAIL Victor Magron LAAS-CNRS Université de Toulouse EMAIL Jun Zhao CCDS, NTU Singapore EMAIL |
| Pseudocode | No | The paper describes mathematical formulations and theoretical aspects of sparse polynomial optimization, but it does not present any explicitly labeled pseudocode or algorithm blocks. |
| Open Source Code | Yes | Our code is available via the following following link: POP4BNN Git Hub Repository. |
| Open Datasets | Yes | MNIST dataset was used to train two sparse networks BNN1 and BNN2, where sparsity refers to weights sparsity defined by ws =: 1 PL i=0 W [i+1] 2 F PL i=0 nini+1 . We assess the performance of our method (number of solved cases (cert.) and verification time t (s)) in verifying robustness of the first 100 images from the test set. Additional experimental results on robustness verification on CIFAR-10 data set are presented in Appendix B, Table 8. |
| Dataset Splits | Yes | We assess the performance of our method (number of solved cases (cert.) and verification time t (s)) in verifying robustness of the first 100 images from the test set. 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. |
| Hardware Specification | Yes | All experiments are run on a desktop with a 12-core i7-12700 2.10 GHz CPU and 32GB of RAM. Finally, due to their increased computational complexity, the experiments from Table 3 were run on a server with a 26-core Intel(R) Xeon(R) Gold 6348 CPU @ 2.60GHz and a RAM of 756GB. |
| Software Dependencies | Yes | The tightened first-order sparse SDP relaxation is modeled with TSSOS (Magron & Wang, 2021) and solved with Mosek (Andersen & Andersen, 2000). Gurobi (Gurobi Optimization, LLC, 2023) is used to solve MILP. BNNs were trained on standard benchmark datasets, using Larq Geiger & Team (2020). |
| Experiment Setup | Yes | The training process, lasting 300 epochs, has consisted of minimizing the sparse categorical cross-entropy, using the Adam optimizer (Kingma & Ba, 2014). The learning rate has been handled by the exponential decay learning scheduler, whose initial value has been set to be 0.001. Ste Tern 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. |