Feb, 2017

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

PDF
TL;DR我们提出了一种基于单纯形方法的技术，用于验证深度神经网络的属性，该方法可以处理非凸的修正线性单元（ReLU）激活函数，成功地验证相对于现有方法已知的规模更大的神经网络，以及用于无人机的下一代空中碰撞避免系统（ACAS Xu）的深度神经网络原型实现。
deep neural networksformal guaranteesverificationrectified linear unitairborne collision avoidance system
发现论文，激发创造
  • 深度神经网络验证的递增式理论可满足性

    本文提出基于增量可满足性模理论算法（SMT）的 Reluplex 框架的增量深度神经网络验证问题和算法，实现了一个称为 DeepInc 的增量求解器。该算法在大多数情况下都比传统算法更高效，并且还提出了一种多目标 DNN 修复问题和算法。

    Feb, 2023

  • 通过网络简化加快神经网络验证

    通过消除稳定的 ReLU 神经元并将其转化为由 ReLU 和仿射层组成的顺序神经网络，我们提出了一种网络削减技术作为预处理方法以便于验证，实验证明这种技术能够显著减小神经网络规模并加快验证过程。

    Aug, 2023

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

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

    Mar, 2018

  • 深度神经网络的安全验证

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

    Oct, 2016

  • 神经网络的自动修复

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

    Jul, 2022

  • 通过诱导 ReLU 稳定性进行更快的对抗鲁棒性验证训练

    本篇论文研究神经网络验证中的协同设计概念，并通过改进权重稀疏性和 ReLU 稳定性的方法，将计算困难的验证问题转化为可处理的问题，并改善了验证的速度，该方法具有普适性。

    Sep, 2018

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

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

    Jul, 2023

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

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

    May, 2017

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

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

    Nov, 2017

  • 面向安全关键深度神经网络的可扩展验证

    本篇论文介绍了在安全重要应用领域中使用深度神经网络的问题，针对其可靠性和安全性的担忧，提出了采用形式化验证来保证其运行符合预期，并通过两个方向，即设计可扩展性的验证技术和识别可验证的深度学习系统的设计选择来缓解这一挑战。

    Jan, 2018