现有神经网络验证方法在真实环境失效，因理论严谨不等于实际可靠。
No Soundness in the Real World: On the Challenges of the Verification of Deployed Neural Networks
- 提出理论严谨与实际可靠的区别，指出现有验证方法忽略部署环境影响。
- 实测显示所有测试验证器均被新型部署攻击攻破，暴露实际漏洞。
- 适合关注模型安全落地的研究者和工程师，尤其重视生产环境可靠性者。
验证的终极目标是保障部署后神经网络的安全性。本文指出，目前所有已知的先进验证器均未能实现这一目标。核心洞察在于：理论上的严谨性（用浮点数计算时对全精度输出的边界约束）并不等同于实际中的可靠性（在可能具有随机性的环境中对浮点输出进行边界约束）。我们证明了当前实现可证明理论严谨性的方法——如区间分析及其变体——均无法保证实际安全性。同时认为实现实际安全性在计算上更困难。通过评估多个知名验证方法，我们以实证支持该观点。我们构造出能探测并利用部署环境特征（如浮点运算顺序与精度）的对抗性网络，成功误导验证器。实验表明，所有测试验证器均易受此类新部署特异性攻击，证明其不具备实际可靠性。
原文摘要 · Abstract (English)
The ultimate goal of verification is to guarantee the safety of deployed neural networks. Here, we claim that all the state-of-the-art verifiers we are aware of fail to reach this goal. Our key insight is that theoretical soundness (bounding the full-precision output while computing with floating point) does not imply practical soundness (bounding the floating point output in a potentially stochastic environment). We prove this observation for the approaches that are currently used to achieve provable theoretical soundness, such as interval analysis and its variants. We also argue that achieving practical soundness is significantly harder computationally. We support our claims empirically as well by evaluating several well-known verification methods. To mislead the verifiers, we create adversarial networks that detect and exploit features of the deployment environment, such as the order and precision of floating point operations. We demonstrate that all the tested verifiers are vulnerable to our new deployment-specific attacks, which proves that they are not practically sound.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。