Aug, 2023

具有可证明的概率保证的深度神经网络中的安全区域枚举

PDF
TL;DR鉴于深度神经网络 (DNNs) 所基于的系统的可信保证，识别安全区域是一个关键问题。为此，我们提出了 AllDNN-Verification 问题：给定一个安全属性和一个 DNN，列举出在属性输入域中所有安全的区域，即属性成立的区域。由于该问题是 #P - 难问题，我们提出了一种高效的近似方法，名为 epsilon-ProVe。我们的方法利用对输出可达集合进行的统计预测容限限制的可控低估，并能够提供安全区域的一个紧凑的 (具有可证明的概率保证) 下界估计。我们在不同的标准基准测试上进行了实证评估，展示了我们方法的可扩展性和有效性，并为这种新类型的 DNN 验证提供了有价值的洞见。
发现论文，激发创造
  • 使用高效的边界传播和并行计算扩展深度神经网络验证工具的规模

    深度神经网络在安全方面的正式验证问题已经扩展到计数版本 (DNN-Verification)，为了在给定安全属性的领域中计算不安全区域的数量。为了解决这个问题的复杂性，本研究提出了一种基于可达性分析、符号线性松弛和并行计算的新策略，以增强现有的精确和近似 DNN 计数的形式验证的效率。在标准的形式验证基准和现实的机器人场景上进行的实证评估表明，在可扩展性和效率方面都取得了显著的改进，使得这种技术能够用于复杂的机器人应用。

    Dec, 2023

  • DeepSafe: 基于数据驱动的神经网络对抗鲁棒性检测方法

    本文提出了一种利用聚类方法自动识别神经网络输入空间安全区域的方法，并借助验证技术来确认这些区域是否安全或提供不安全的反例，并引入了目标鲁棒性的概念，以确保神经网络不会将任何输入映射到目标标签，利用 MNIST 数据集以及控制下一代无人机避撞系统的神经网络实施的空中碰撞预防系统（ACAS Xu）进行验证。

    Oct, 2017

  • 使用可证明保证的方式对深度神经网络进行可达性分析

    本文研究针对前馈深度神经网络的通用可达性问题，通过计算输出函数值的下限和上限，得到区间范围内的可达值，从而得出安全性验证问题、输出范围分析问题和鲁棒性度量，并通过自适应嵌套优化的新算法，有效地解决了可达性问题。

    May, 2018

  • 深度神经网络的可证明修复

    本文提出了可证明修复问题，即在发现不安全行为后修复神经网络 (DNN) 的问题，并介绍了可用于有限点和凸多面体等安全规范的 Provable Point 和 Provable Polytope 修复算法，以及 Decoupled DNN 结构，它允许将可证明修复减少至线性规划问题。实验结果证明了我们的算法在各种具有挑战性的任务中的有效性和效率。

    Apr, 2021

  • DNN - 验证问题：计算深度神经网络的不安全输入数量

    本文介绍了 DNN-Verification 问题，分析了其复杂性并提出了一种新颖的方法，该方法返回违反特定安全属性的 DNN 输入配置的确切计数。考虑到问题的 #P 完备性，我们还提出了一种随机的、近似的方法，该方法提供了一个可证明的概率界限，同时显著减少了计算需求。我们在一组安全关键基准上呈现了实验结果，证明了我们的近似方法的有效性，并评估了界限的紧密度。

    Jan, 2023

  • 验证深度学习对于超出分布领域的泛化能力

    通过使用 DNN 验证技术，我们引入了一种新的方法来识别具有稳健泛化能力的 DNN 决策规则，并在真实世界环境中进行了广泛评估，为部署 DNN 驱动系统提供了新的验证目标。

    Jun, 2024

  • 深度神经网络控制系统的定性与定量安全验证统一

    通过定性和定量安全性验证问题的综合合成有效的神经屏障证书，本文提出了一种用于 DNN 控制系统的新型框架，并通过 $ extsf {UniQQ}$ 工具在四个经典 DNN 控制系统上展示了其有效性。

    Apr, 2024

  • 使用符号传播分析深度神经网络：实现更高的精度和更快的验证

    本文提出通过符号传播技术，以符号方式表示神经元值，并在抽象域上由输入层向前传播，用于分析深度神经网络，从而提高系统安全性验证精度。该方法相较于其他方法具有显著优势。

    Feb, 2019

  • 深度神经网络验证的认证证明检查器

    本文介绍了一种基于 Imandra 的 DNN 验证证明检查器的新实现，该实现通过使用 Imandra 的两个关键功能：无限精度实数算术和形式化验证基础设施来提高数字稳定性和验证性能，并在实现验证正确性属性和性能优化方面继续开展工作。

    Jul, 2023

  • 深度网络可扩展验证的双重方法

    本文提出了一种通用的神经网络形式验证框架，通过将验证问题转化为最优化问题，并通过我们提出的松弛算法得到可靠的上界，从而可对神经网络的输入和输出属性满足的规范进行形式化验证。

    Mar, 2018