Feb, 2023

深度神经网络验证的递增式理论可满足性

PDF
TL;DR本文提出基于增量可满足性模理论算法（SMT）的 Reluplex 框架的增量深度神经网络验证问题和算法，实现了一个称为 DeepInc 的增量求解器。该算法在大多数情况下都比传统算法更高效，并且还提出了一种多目标 DNN 修复问题和算法。
deep neural networksai safetyincremental verificationsatisfiability modulo theorydnn repair
发现论文，激发创造
  • 深度神经网络的安全验证

    本研究提出一种基于 Satisfiability Modulo Theory (SMT) 的新型自动化验证框架，旨在保证深度神经网络对于图像操作的安全性，能够发现对于给定操作范围和家族，对抗性样本是否存在，同时比较现有的相关技术。

    Oct, 2016

  • 神经网络的自动修复

    提出了一种通过使用 SMT 求解器修复有关安全规范的不安全神经网络，以防止对抗攻击，并且通过修改少量的权重值来寻找新的安全神经网络表示，从而最大限度地保持决策边界相似性，同时保证只有轻微的准确度损失，证明了该方法的实用性。

    Jul, 2022

  • Reluplex：用于验证深度神经网络的高效 SMT 求解器

    我们提出了一种基于单纯形方法的技术，用于验证深度神经网络的属性，该方法可以处理非凸的修正线性单元（ReLU）激活函数，成功地验证相对于现有方法已知的规模更大的神经网络，以及用于无人机的下一代空中碰撞避免系统（ACAS Xu）的深度神经网络原型实现。

    Feb, 2017

  • 使用符号区间对神经网络进行形式化安全分析

    利用区间算法和符号区间分析代替 SMT solver，可以更高效地实现对 DNN 的安全性质进行正式验证，ReluVal 系统相比现有最先进的 solver-based 系统 Reluplex，平均可以提升 200 倍验证效率。

    Apr, 2018

  • 用于验证深度神经网络的 DPLL (T) 框架

    引入一种新的约束求解方法 NeuralSAT，用作深度神经网络 (DNN) 验证的符号化求解器。

    Jul, 2023

  • 神经网络的增量验证

    该研究提出了一种基于新颖理论、数据结构和算法设计的增量和完全的 DNN 验证框架，旨在提高完全验证器在更新后的 DNN 上的验证效率。将其实现在名为 IVAN 的工具中，可以在 MNIST 和 CIFAR10 分类器上实现总体几何平均加速比为 2.4 倍，在 ACAS-XU 分类器上实现总体几何平均加速比为 3.8 倍。

    Apr, 2023

  • 分段线性神经网络验证的统一视角

    本文介绍了一种统一的深度学习模型形式验证的框架，利用分段线性结构和形式方法，结合现有方法的优势以实现两个数量级的加速。并提出了一组新的基准数据集，通过实验比较现有算法并确定影响验证问题难度的因素。

    Nov, 2017

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

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

    Apr, 2021

  • 分段线性前馈神经网络的形式化验证

    本文提出了一种针对具备分段线性激活函数的前向神经网络进行验证的方法，并使用全局线性逼近对 SMT 求解器和 ILP 求解器进行推理，通过专门设计的验证算法利用推理出的相位信息对网络进行冲突检测和安全节点约束，并在碰撞避免和手写数字识别案例研究中进行了评价。

    May, 2017

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

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

    Jul, 2023