arXiv:2505.05235v1 Announce Type: new 摘要：传统的深度神经网络（DNN）形式化验证（FV）方法受限于对安全属性的二进制编码，其中模型被分类为安全或不安全（稳健或不稳健）。这种二进制编码无法捕捉模型中的细微安全程度，往往导致过于严格的或过于宽松的要求。在本文中，我们提出了一个新的问题形式化称为抽象DNN验证，它可以验证不安全输出的分层结构，为给定的DNN提供更精细的安全性分析。关键的是，通过利用抽象解释并推理输出可达集，我们的方法在形式化验证过程中能够评估多个安全性级别，所需计算努力（在最坏情况下）与传统的二进制验证方法相当，甚至可能更少。具体来说，我们展示了这种形式化如何根据其抽象安全性级别违规对对抗性输入进行排名，提供了对模型安全性和稳健性的更详细评估。我们的贡献包括对我们的新型抽象安全性形式化与现有使用抽象解释进行稳健性验证的方法的关系的理论探索，对所引入的新问题的复杂性分析，以及考虑基于Habitat 3.0的复杂深度强化学习任务和标准DNN验证基准的实证评估。