# Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization

arXiv: https://arxiv.org/abs/2405.17049 · HTML: https://mlsanity.com/paper/2405.17049/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 35 of its 68 references that are in the map.
- First posted on arXiv 27 May 2024.

## Builds on (most cited first, 30 of 35)

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [XNOR-Net: ImageNet Classification Using Binary Convolutional Neural Networks](https://mlsanity.com/paper/1603.05279/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [BinaryConnect: Training Deep Neural Networks with binary weights during propagations](https://mlsanity.com/paper/1511.00363/) (2015)
- [Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networks](https://mlsanity.com/paper/1906.04893/) (2019)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Binary Neural Networks: A Survey](https://mlsanity.com/paper/2004.03333/) (2020)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Semidefinite relaxations for certifying robustness to adversarial examples](https://mlsanity.com/paper/1811.01057/) (2018)
- [A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks](https://mlsanity.com/paper/1902.08722/) (2019)
- [Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming](https://mlsanity.com/paper/1903.01287/) (2019)
- [Lipschitz constant estimation of Neural Networks via sparse polynomial optimization](https://mlsanity.com/paper/2004.08688/) (2020)
- [Verifying Properties of Binarized Deep Neural Networks](https://mlsanity.com/paper/1709.06662/) (2017)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming](https://mlsanity.com/paper/2010.11645/) (2020)
- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [An SMT-Based Approach for Verifying Binarized Neural Networks](https://mlsanity.com/paper/2011.02948/) (2020)
- [A comprehensive review of Binary Neural Network](https://mlsanity.com/paper/2110.06804/) (2021)
- [Exploiting Verified Neural Networks via Floating Point Numerical Error](https://mlsanity.com/paper/2003.03021/) (2020)
- [On Tractable Representations of Binary Neural Networks](https://mlsanity.com/paper/2004.02082/) (2020)
- [Efficient Exact Verification of Binarized Neural Networks](https://mlsanity.com/paper/2005.03597/) (2020)
- [Attacking Binarized Neural Networks](https://mlsanity.com/paper/1711.00449/) (2017)
- [BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks](https://mlsanity.com/paper/2103.07224/) (2021)
- [Semialgebraic Representation of Monotone Deep Equilibrium Models and Applications to Certification](https://mlsanity.com/paper/2106.01453/) (2021)
- [Verification of Non-Linear Specifications for Neural Networks](https://mlsanity.com/paper/1902.09592/) (2019)
- [TSSOS: A Moment-SOS hierarchy that exploits term sparsity](https://mlsanity.com/paper/1912.08899/) (2019)
- [Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning](https://mlsanity.com/paper/2101.10102/) (2021)
- [Combinatorial Attacks on Binarized Neural Networks](https://mlsanity.com/paper/1810.03538/) (2018)
- [Sparse Polynomial Optimisation for Neural Network Verification](https://mlsanity.com/paper/2202.02241/) (2022)
- [Chordal Sparsity for SDP-based Neural Network Verification](https://mlsanity.com/paper/2206.03482/) (2022)

## Built on by (most cited first, 1 of 1)

- [Stochastic Sample Approximations of (Local) Moduli of Continuity](https://mlsanity.com/paper/2509.15368/) (2025)

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