Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization
Not on the map. Why?
Abstract (arXiv)
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 |.|_∞ and |.|2-based adversarial attacks.
Key facts. Cited by 1 paper in the map (data through 7 Oct 2026). Builds on 35 of its 68 references that are in the map. First posted on arXiv 27 May 2024.
Builds on
35 of 68 references.
References · 35
- 2013Intriguing properties of neural networkscited by 5,114
- 2016XNOR-Net: ImageNet Classification Using Binary Convolutional Neural Networkscited by 829
- 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 739
- 2015BinaryConnect: Training Deep Neural Networks with binary weights during propagationscited by 571
- 2019Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networkscited by 290
- 2019Algorithms for Verifying Deep Neural Networkscited by 221
- 2020Binary Neural Networks: A Surveycited by 184
- 2020Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifierscited by 183
- 2018Semidefinite relaxations for certifying robustness to adversarial examplescited by 178
- 2019A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networkscited by 124
- 2019Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programmingcited by 100
- 2020Lipschitz constant estimation of Neural Networks via sparse polynomial optimizationcited by 87
23 more
- 2017Verifying Properties of Binarized Deep Neural Networkscited by 77
- 2020Verification of Deep Convolutional Neural Networks Using ImageStarscited by 75
- 2020Enabling certification of verification-agnostic networks via memory-efficient semidefinite programmingcited by 65
- 2019Quantitative Verification of Neural Networks And its Security Applicationscited by 56
- 2020An SMT-Based Approach for Verifying Binarized Neural Networkscited by 47
- 2021A comprehensive review of Binary Neural Networkcited by 44
- 2020Exploiting Verified Neural Networks via Floating Point Numerical Errorcited by 35
- 2020On Tractable Representations of Binary Neural Networkscited by 34
- 2020Efficient Exact Verification of Binarized Neural Networkscited by 33
- 2017Attacking Binarized Neural Networkscited by 28
- 2021BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networkscited by 17
- 2021Semialgebraic Representation of Monotone Deep Equilibrium Models and Applications to Certificationcited by 16
- 2019Verification of Non-Linear Specifications for Neural Networkscited by 14
- 2019TSSOS: A Moment-SOS hierarchy that exploits term sparsitycited by 14
- 2021Towards Practical Robustness Analysis for DNNs based on PAC-Model Learningcited by 12
- 2018Combinatorial Attacks on Binarized Neural Networkscited by 11
- 2022Sparse Polynomial Optimisation for Neural Network Verificationcited by 8
- 2022Chordal Sparsity for SDP-based Neural Network Verificationcited by 4
- 2023Taming Binarized Neural Networks and Mixed-Integer Programscited by 4
- 2021TSSOS: a Julia library to exploit sparsity for large-scale polynomial optimizationcited by 3
- 2022A Mixed Integer Programming Approach for Verifying Properties of Binarized Neural Networkscited by 3
- 2023On-Device Learning with Binary Neural Networkscited by 3
- 2014Formal Proofs for Nonlinear Optimizationcited by 2
Built on by
Citing papers per year: 2025: 1.
1 paper.