FocusBranch: Combinatorial Branch-and-Bound for $\ell_0$ Neural Network Robustness Verification

Verifying the local robustness of neural networks under $\ell_0$ perturbations is inherently combinatorial: a verifier must reason over all sparse subsets of perturbed pixels. This paper presents FocusBranch, a combinatorial branch-and-bound framework for $\ell_0$ robustness verification. The key insight is to decompose the $\ell_0$-ball using nodes, where each node consists of a focus pixel set $\mathcal{S}$ and a level $l$, requiring at least $l$ perturbed pixels to lie in $\mathcal{S}$. This abstraction unifies two branching mechanisms: concrete nodes branch through upper shadows to fix additional perturbed locations, while super nodes branch through covering designs to cover many perturbation cases with fewer child nodes. FocusBranch proves node safety by concretizing linear relaxations over node-constrained $\ell_0$-balls and recursively branches on unknown nodes. Rather than relying on a fixed verification strategy, it samples nodes across levels to estimate success rates and costs, then selects a starting level and branching strategy predicted to minimize verification time. Experiments on fully connected and convolutional classifiers for MNIST, Fashion-MNIST, and CIFAR-10 show that FocusBranch verifies $\ell_0$ local robustness effectively across architectures and outperforms state-of-the-art verifiers.