FocusBranch turns ℓ0 robustness verification into branchable nodes: 2,799 candidate instances verified across 13 networks, versus 375 for the strongest baseline
Synopsis
For ℓ0 perturbations that change only a few pixels, FocusBranch rewrites the “at most k perturbed pixels” constraint as a node made of a focus pixel set and a level, so verification can branch across levels. It builds super nodes through covering designs and concrete nodes through upper shadows, and picks a starting level from sampling estimates. Across 13 networks and 3,189 candidate instances it verified 2,799; in a 740-instance comparison it verified 641, against 375 for CoVerD+top-k-GP.
Interpretation
FocusBranch replaces a fixed decomposition plan with a branch-and-bound process that chooses a starting level and branching strategy per instance, so one framework both decomposes by covering designs and fixes perturbed pixel locations one at a time. CoVerD+top-k-GP always starts from the initial node at the largest level k, which is the special case of FocusBranch fixed at level k; Calzone and CoVerD instead require every subproblem to place all perturbed pixels in one set. On 740 candidate instances, FocusBranch verified 641, CoVerD+top-k-GP verified 375 and CoVerD verified 100; on fully connected networks the three verified 367, 179 and 1, and on CNNs 274, 196 and 99.
A node pairs a focus pixel set with a level that caps how many pixels outside the focus set may be perturbed, so each node describes one constrained perturbation input space. Concrete nodes branch through upper shadows, fixing one additional perturbed location into the focus set per child; super nodes branch through covering designs that refine the focus set and cover many perturbation cases with fewer children. In the ablation on afc5 at k=5, the full method verified 61 of 70 instances, the variant with only concrete branching verified 49, and the variant with only super-node branching verified 56.
Node safety is decided with LiRPA-style linear relaxations, but each concretization is solved in closed form over the node-constrained ℓ0 ball, without enumerating perturbation subsets. Concretization over the full ℓ0 ball takes the globally top-k contributing pixels; under a node constraint it first takes the top contributors inside the focus set and fills the remaining budget from outside it. Across 13 networks on MNIST, Fashion-MNIST and CIFAR-10, it verified 952 candidate instances at k=3, 839 at k=4, 641 at k=5 and 367 at k=6; only 7.4% of verified instances invoked the MILP fallback.
Perspective
The evaluation covers 13 image-classification networks on MNIST, Fashion-MNIST and CIFAR-10 under pixel-level ℓ0 budgets; bcv4 and bcv5 are evaluated only at k=3 because their bounds are too loose, and all tools use a 1800 s timeout (3600 s for bcv4). The authors list extension of ℓ0 verification to domains such as language models as future work.
The authors note that exact verification is inherently combinatorial and computationally hard, so within practical time and memory budgets they evaluate networks with up to thousands of neurons; covering-design super branching may duplicate bounding effort because different child super nodes cover overlapping perturbation cases; and breadth-first node management delays exploration of deep unbranchable nodes, which can postpone MILP finding a counterexample.