DNN 认证器 soundness 验证的自动化方法
编程语言
2025-04-08 v1
摘要
深度神经网络（DNN）的不可解释性阻碍了其在安全关键应用中的使用。基于抽象解释的 DNN 认证器为建立对 DNN 信任提供了有前景的途径。这些认证器的这些数学逻辑中的不严谨性可能导致错误结果。然而，当前确保其严谨性的做法依赖于手动、专家驱动的证明，这些证明繁琐且难以开发，限制了新认证器开发的速度。对于任意 DNN 架构和处理多样化抽象分析的认证器验证工作具有挑战性。我们引入了 ProveSound，这是一个新的验证程序，用于自动化 DNN 认证器的严谨性验证，适用于任意 DNN 架构。我们的核心贡献是引入符号 DNN 的概念，通过 ProveSound 将严谨性属性——即对任意 DNN 的全称量化——化简为可处理的符号表示，从而可使用标准 SMT 求解器进行验证。通过形式化 ConstraintFlow——一种用于指定认证器的 DSL——的语法和操作语义，ProveSound 能高效验证现有和新认证器，处理任意 DNN 架构。我们的代码已在 https://github.com/uiuc-focal-lab/constraintflow.git 上提供。
引用
@article{arxiv.2504.04542,
title = {Automated Verification of Soundness of DNN Certifiers},
author = {Avaljot Singh and Yasmin Chandini Sarita and Charith Mendis and Gagandeep Singh},
journal= {arXiv preprint arXiv:2504.04542},
year = {2025}
}