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.

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

神经网络全局鲁棒性验证

Verification of Neural Networks' Global Robustness

Neural network verification mainly focuses on local robustness properties.
However, often it is important to know whether a given property holds globally
for the whole input domain, and if not then for what proportion of the input
the property is true. While exact preimage generation can construct an
equivalent representation of neural networks that can aid such (quantitative)
global robustness verification, it is intractable at scale. In this work, we
propose an efficient and practical anytime algorithm for generating symbolic
under-approximations of the preimage of neural networks based on linear
relaxation. Our algorithm iteratively minimizes the volume approximation error
by partitioning the input region into subregions, where the neural network
relaxation bounds become tighter. We further employ sampling and differentiable
approximations to the volume in order to prioritize regions to split and
optimize the parameters of the relaxation, leading to faster improvement and
more compact under-approximations. Evaluation results demonstrate that our
approach is able to generate preimage approximations significantly faster than
exact methods and scales to neural network controllers for which exact preimage
generation is intractable. We also demonstrate an application of our approach
to quantitative global verification.

研究了神经网络的全局鲁棒性问题，提出了一种在量化验证中高效的、基于线性松弛的生成符号下逼近的先验图像的算法。

神经网络中的原像逼近

On Preimage Approximation for Neural Networks

Many recent works have proposed methods to train classifiers with local
robustness properties, which can provably eliminate classes of evasion attacks
for most inputs, but not all inputs. Since data distribution shift is very
common in security applications, e.g., often observed for malware detection,
local robustness cannot guarantee that the property holds for unseen inputs at
the time of deploying the classifier. Therefore, it is more desirable to
enforce global robustness properties that hold for all inputs, which is
strictly stronger than local robustness.
In this paper, we present a framework and tools for training classifiers that
satisfy global robustness properties. We define new notions of global
robustness that are more suitable for security classifiers. We design a novel
booster-fixer training framework to enforce global robustness properties. We
structure our classifier as an ensemble of logic rules and design a new
verifier to verify the properties. In our training algorithm, the booster
increases the classifier's capacity, and the fixer enforces verified global
robustness properties following counterexample guided inductive synthesis.
We show that we can train classifiers to satisfy different global robustness
properties for three security datasets, and even multiple properties at the
same time, with modest impact on the classifier's performance. For example, we
train a Twitter spam account classifier to satisfy five global robustness
properties, with 5.4% decrease in true positive rate, and 0.1% increase in
false positive rate, compared to a baseline XGBoost model that doesn't satisfy
any property.

本文提出了一个框架和工具来训练满足全局鲁棒性的分类器，并通过逐步引导综合来强制验证全局鲁棒性属性，同时结构分类器作为逻辑规则的集合，并在三个安全数据集上展示了在对分类器性能的影响较小的情况下，训练分类器满足不同的全局鲁棒性属性。

使用验证的全局鲁棒性属性学习安全分类器

Learning Security Classifiers with Verified Global Robustness Properties

The threat of adversarial examples has motivated work on training certifiably
robust neural networks to facilitate efficient verification of local robustness
at inference time. We formalize a notion of global robustness, which captures
the operational properties of on-line local robustness certification while
yielding a natural learning objective for robust training. We show that
widely-used architectures can be easily adapted to this objective by
incorporating efficient global Lipschitz bounds into the network, yielding
certifiably-robust models by construction that achieve state-of-the-art
verifiable accuracy. Notably, this approach requires significantly less time
and memory than recent certifiable training methods, and leads to negligible
costs when certifying points on-line; for example, our evaluation shows that it
is possible to train a large robust Tiny-Imagenet model in a matter of hours.
Our models effectively leverage inexpensive global Lipschitz bounds for
real-time certification, despite prior suggestions that tighter local bounds
are needed for good performance; we posit this is possible because our models
are specifically trained to achieve tighter global bounds. Namely, we prove
that the maximum achievable verifiable accuracy for a given dataset is not
improved by using a local bound.

通过在网络中加入全局 Lipschitz 边界，文中提出的方法可以快速训练大型强健的神经网络，实现了可证明的最先进的可验证准确性。同时，该方法比最近的可证方法需要的时间和内存少得多，并在在线认证时产生可忽略的成本。