发表机构
University of Crete; Catalan Institution for Research and Advanced Studies; University of Lleida（克里特大学; 加泰罗尼亚研究与高级研究所; 莱里达大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
研究人工智能安全中对抗鲁棒性问题，通过格遍历将其转化为区间认证问题，开发格遍历算子并用于细化与验证迭代方案，保证合理最大化和完全最小化，研究了优化问题的不对称性及对称区间优化问题，还进行了实证评估。
AI 中文摘要
在这项工作中，我们为人工智能安全的一个基本问题——对抗鲁棒性，提出了一个严格的理论框架。我们表明对抗鲁棒性问题可简化为格遍历问题。格中的每个元素对应一个包含输入点\(\mathbf{x}\)的区间（即轴对齐超矩形）。对于多层感知器分类器（MLP），若\(\mathbf{x} \in I\)且\(\mathbf{x}\)在\(I\)中可自由扰动而不改变MLP预测，则区间\(I\)构成合理认证；若\(\mathbf{x} \in I\)且\(\mathbf{x}\)移出\(I\)时MLP预测必然改变，则区间\(I\)构成完全认证。我们开发了格遍历算子并应用于细化与验证迭代方案，使用形式化MLP验证器保证了合理最大化和完全最小化。此外，我们研究了目标优化问题，发现了一些有趣的不对称性，对于完全认证，可在多项式预言机调用中获得最小解，而合理认证则有强难解性结果。我们还研究了对称区间（即\(\ell_\infty\)球）中的优化问题并提供了对数算法。最后，我们使用新颖的ParallelepipedoNN系统进行了实证评估。
英文摘要
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}$. 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. 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. 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.
