Interval Certifications for Multilayered Perceptrons via Lattice Traversal

通过格遍历实现多层感知机的区间认证

Abstract: In this work we present a rigorous theoretical framework to a foundational problem of AI safety, namely adversarial robustness. In particular, we show that the adversarial robustness problem can be reduced to a lattice traversal problem. Each element of this lattice corresponds to an interval, i.e., an axis-aligned hyper-rectangle, containing an input point $\mathbf{x}$.

摘要： 在这项工作中，我们针对人工智能安全的一个基础问题——对抗鲁棒性，提出了一个严谨的理论框架。具体而言，我们证明了对抗鲁棒性问题可以归约为一个格遍历（lattice traversal）问题。该格中的每个元素对应一个区间，即包含输入点 $\mathbf{x}$ 的轴对齐超矩形。

Consider a multilayered perceptron classifier (MLP). An interval $I$ constitutes a sound certification if $\mathbf{x} \in I$ and $\mathbf{x}$ can be freely perturbed in $I$ without changing the MLP’s prediction. Complementarily, an interval $I$ constitutes a complete certification if $\mathbf{x} \in I$ and when $\mathbf{x}$ moves outside of $I$ the MLP’s prediction is guaranteed to change.

考虑一个多层感知机（MLP）分类器。如果 $\mathbf{x} \in I$ 且 $\mathbf{x}$ 在 $I$ 内可以自由扰动而不改变 MLP 的预测结果，则称区间 $I$ 为一个可靠认证（sound certification）。与之互补的是，如果 $\mathbf{x} \in I$ 且当 $\mathbf{x}$ 移出 $I$ 时，MLP 的预测结果必然发生改变，则称区间 $I$ 为一个完备认证（complete certification）。

While the sound certification problem corresponds to the well-studied adversarial robustness, complete certifications have not been examined in the literature. We develop lattice traversal operators, which we apply in a refine & verify iterative scheme. Using formal MLP verifiers, sound maximality and complete minimality are guaranteed.

虽然可靠认证问题对应于已被广泛研究的对抗鲁棒性，但完备认证在现有文献中尚未得到探讨。我们开发了格遍历算子，并将其应用于一种“细化与验证”（refine & verify）的迭代方案中。通过使用形式化 MLP 验证器，我们保证了可靠最大性和完备最小性。

Moreover, we examine objective optimization problems. There we discover some interesting asymmetries. For complete certifications, the minimum solution is obtained in polynomial oracle calls. This does not hold for sound certifications, where we prove strong intractability results. Additionally, we examine optimization problems in symmetric intervals (i.e., $\ell_\infty$-spheres), where we provide logarithmic algorithms. Finally, we present an empirical evaluation, using the novel ParallelepipedoNN system.

此外，我们研究了目标优化问题，并发现了一些有趣的非对称性。对于完备认证，其最小解可以通过多项式次数的预言机调用（oracle calls）获得；而对于可靠认证，情况则不然，我们证明了其具有极强的难解性。此外，我们还研究了对称区间（即 $\ell_\infty$ 球）中的优化问题，并提供了对数时间复杂度的算法。最后，我们使用全新的 ParallelepipedoNN 系统进行了实证评估。