Differential Zonotopes for Verifying Global Robustness of DNNs
The robustness of deep neural networks (DNNs) is critical in security-sensitive applications, where small input perturbations should not alter model predictions. This property is commonly formalized as local or global robustness: the former considers perturbations around a single input, while the latter -- strictly stronger -- quantifies over all input pairs. While local robustness can be expressed as a safety property, global robustness is a 2-safety property, making it substantially more challenging to verify. We present a novel static analysis technique for verifying the global robustness of DNNs. Our approach is based on differential halo zonotopes, a new abstract domain that extends zonotopes to jointly propagate pairs of perturbed inputs in lock-step while tightly bounding their divergence. In addition, we introduce a symmetric variant of confidence-based global robustness that disregards perturbations leading to differing but low-confidence predictions. This relaxation yields a practically meaningful notion of robustness that applies to a broader class of networks. We implement our approach in a new tool, called TwoSafe, and evaluate it on standard DNN verification benchmarks, including widely deployed models. Our results show that TwoSafe significantly outperforms the state of the art in both precision and scalability, enabling the verification of networks an order of magnitude larger than those handled by prior techniques.