Neural networks are successful in various applications but are also
susceptible to adversarial attacks. To show the safety of network classifiers,
many verifiers have been introduced to reason about the local robustness of a
given input to a given perturbation. While successful, local robustness cannot
generalize to unseen inputs. Several works analyze global robustness
properties, however, neither can provide a precise guarantee about the cases
where a network classifier does not change its classification. In this work, we
propose a new global robustness property for classifiers aiming at finding the
minimal globally robust bound, which naturally extends the popular local
robustness property for classifiers. We introduce VHAGaR, an anytime verifier
for computing this bound. VHAGaR relies on three main ideas: encoding the
problem as a mixed-integer programming and pruning the search space by
identifying dependencies stemming from the perturbation or network computation
and generalizing adversarial attacks to unknown inputs. We evaluate VHAGaR on
several datasets and classifiers and show that, given a three hour timeout, the
average gap between the lower and upper bound on the minimal globally robust
bound computed by VHAGaR is 1.9, while the gap of an existing global robustness
verifier is 154.7. Moreover, VHAGaR is 130.6x faster than this verifier. Our
results further indicate that leveraging dependencies and adversarial attacks
makes VHAGaR 78.6x faster.

本研究提出了一种全局鲁棒性验证方法，用于确定网络分类器不改变其分类的情况，通过利用依赖关系和对未知输入进行的对抗性攻击，该验证方法相较于现有的验证方法在计算精确度和速度方面有显著提升。