神经网络的安全性质作为决策问题
Security Properties of Neural Networks as Decision Problems
浏览论文内容
中文总结 AI 辅助
本文形式化并分类了神经网络验证中的八个决策问题，证明无干扰、单调性、反事实公平性和反转抵抗等为co-NP-完全，后门检测为Sigma_2^P-完全，参数量化故障模型下验证为exists-R-完全，揭示了不同安全性质的复杂性层级。
中文摘要 AI 辅助
对已部署的神经网络进行认证引出了验证文献尚未分类的决策问题：模型是否携带在其训练数据中植入的后门，其存储参数中的故障是否可能将其驱动到不安全状态，其输出是否泄露其输入的私有部分。我们形式化了八个此类问题，并尽可能对其进行分类。组织性观察是一个逻辑性的观察。由分段线性网络计算的函数，连同其所有节点值，可由一个大小与网络线性相关的实数加法的无量词公式定义，因此网络的一个性质是一个量词交替句子，根据Sontag 1985年的定理，该句子位于多项式层次结构中其前缀对应的层级。因此，成员资格结果是推论，并且论证清楚地表明了它们所需的条件：量化对象是输入而非网络自身的参数。无干扰性、单调性和反事实公平性恰好具有网络等价性和区间验证的复杂性，在ReLU上均为co-NP-完全。从量化字母表检测后门触发器是Sigma_2^P-完全的，比鲁棒性认证高一个层级，因此除非层次结构崩溃，否则它不会归约为多项式多个鲁棒性查询。对于每个l_p度量（p为固定正整数），反转抵抗是co-NP-完全的。对参数而非输入进行量化——位翻转攻击、辐射扰动和模拟加速器的故障模型——使得验证对于恒等节点网络已经是exists-R-完全的，而对于这些网络，所有先前研究的问题都在P中，并且当每个参数被限制在逆多项式宽度的盒子中时，该复杂性仍然成立；相应的安全问题对于ReLU是forall-R-完全的。
英文摘要
Certifying a deployed neural network raises decision problems that the verification literature has not classified: whether the model carries a backdoor planted in its training data, whether a fault in its stored parameters can drive it into an unsafe state, whether its output leaks a private part of its input. We formalise eight such problems and classify what we can. The organising observation is a logical one. The function computed by a piecewise linear network, together with all its node values, is definable by a quantifier-free formula of real addition of size linear in the network, so a property of the network is a quantifier-alternation sentence, which Sontag's 1985 theorem places in the polynomial hierarchy at the level of its prefix. Membership results are thus corollaries, and the argument makes plain what they need: that the quantified objects are inputs rather than the network's own parameters. Non-interference, monotonicity and counterfactual fairness have exactly the complexity of network equivalence and of interval verification, all co-NP- complete over ReLU. Detection of backdoor triggers from a quantised alphabet is Sigma_2^P-complete, one level above robustness certification, so it does not reduce to polynomially many robustness queries unless the hierarchy collapses. Inversion resistance is co-NP-complete for every l_p metric, p a fixed positive integer. Quantifying over parameters instead of inputs - the fault model of bit-flip attacks, radiation upsets and analog accelerators - makes verification exists-R-complete already for networks of identity nodes, for which every previously studied problem is in P, and it stays so when each parameter is confined to a box of inverse-polynomial width; the corresponding safety question is forall-R-complete for ReLU.
发表机构
- BTU Cottbus–Senftenberg（科特布斯-森夫滕贝格勃兰登堡工业大学）
机构由 AI 辅助整理，请以论文原文为准。
