利用 Z3 对 FNN 全局鲁棒性进行形式化建模与验证
机器学习
2023-04-25 v2 人工智能
计算机科学中的逻辑
摘要
尽管前馈神经网络（FNNs）在各种任务中取得了显著成功，它们仍易受对抗样本攻击。已有多种技术用于验证 FNN 的对抗鲁棒性，但多数聚焦于针对单个数据点局部扰动邻域的鲁棒性验证。全局鲁棒性分析仍存在较大研究空白。可验证全局鲁棒性的框架 DeepGlobal 已被提出，用于识别 FNN 的\textit{所有}可能的对抗危险区域（ADRs），而不限于测试集中的数据样本。在本文中，我们利用 SMT 求解器 Z3 对 DeepGlobal 进行了更明确完整的规约与实现，并提出了若干改进以提升验证效率。为评估我们的实现与改进的有效性，我们在一组基准数据集上进行了大量实验。实验结果的可视化显示了该方法的有效性与实用性。
引用
@article{arxiv.2304.10558,
title = {Using Z3 for Formal Modeling and Verification of FNN Global Robustness},
author = {Yihao Zhang and Zeming Wei and Xiyue Zhang and Meng Sun},
journal= {arXiv preprint arXiv:2304.10558},
year = {2023}
}
备注
Accepted By SEKE 2023