# Some Complexity Results for Robustness Verification for Binarized Neural Networks

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 3 of its 4 references that are in the map.
- First posted on arXiv 17 Jun 2026.

## Builds on (most cited first, 3 of 3)

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Verifying Properties of Binarized Deep Neural Networks](https://mlsanity.com/paper/1709.06662/) (2017)
- [OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep Neural Networks](https://mlsanity.com/paper/2301.11912/) (2023)

## Abstract (arXiv)

This paper investigates the computational complexity of verification problems for Binarized Neural Networks (BNNs), in which activations and weights are binary. Specifically, we study three verification problems. First, we prove that checking the satisfiability of a linear property for a BNN is NP-complete via a reduction from the Boolean Satisfiability (SAT) problem. Second, we show that verifying robustness under non-uniform image occlusion is NP-complete through a reduction from SAT. Finally, we demonstrate that uniform occlusion induces a piecewise-constant structure in the network output, which enables the design of a polynomial-time algorithm for robustness verification.