用于深度神经网络验证的增量可满足性模理论
人工智能
2023-02-14 v1 形式语言与自动机理论
摘要
约束求解是深度神经网络（DNN）验证的基本方法。在 AI 安全领域，DNN 可能因其修复或攻击而在结构与参数上被修改。针对此类情形，我们提出增量 DNN 验证问题，即询问在安全属性在 DNN 被修改后是否仍然成立。为解决该问题，我们提出一种基于 Reluplex 框架的增量可满足性模理论（SMT）算法。我们模拟了旧求解过程（针对原始网络）中推断搜索分支验证结果配置的最重要特征，并启发式地检查这些证明对修改后的 DNN 是否仍然有效。我们将算法实现为名为 DeepInc 的增量求解器，实验结果表明 DeepInc 在大多数情况下更高效。对于修改前后性质均成立的情况，加速可达数个数量级，表明 DeepInc 在增量搜索反例方面表现突出。此外，基于该框架，我们提出多目标 DNN 修复问题，并给出基于增量 SMT 求解算法的修复方法。与现有最优方法相比，我们的修复方法在修复后的 DNN 上保留了更多潜在安全性质。
引用
@article{arxiv.2302.06455,
title = {Incremental Satisfiability Modulo Theory for Verification of Deep Neural Networks},
author = {Pengfei Yang and Zhiming Chi and Zongxin Liu and Mengyu Zhao and Cheng-Chao Huang and Shaowei Cai and Lijun Zhang},
journal= {arXiv preprint arXiv:2302.06455},
year = {2023}
}