Apr, 2018

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

PDF
TL;DR利用区间算法和符号区间分析代替 SMT solver，可以更高效地实现对 DNN 的安全性质进行正式验证，ReluVal 系统相比现有最先进的 solver-based 系统 Reluplex，平均可以提升 200 倍验证效率。
deep neural networkssecurity testingsatisfiability modulo theory solversinterval arithmeticreluval
发现论文，激发创造
  • 神经网络验证的优化符号化区间传播

    本文提出了一种新的基于符号区间传播和变量分裂的分支定界求解器 DPNeurifyFV，该方法采用新的启发式算法来选择区间变量，以改善变量相关性问题，在结合其他改进措施的情况下，可以显著提高深度学习神经网络验证的效率，并在空中碰撞避免网络 ACAS Xu 上实现了运行时改进。

    Dec, 2022

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

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

    Feb, 2019

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

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

    Oct, 2016

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

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

    Feb, 2023

  • 神经网络的有效形式安全分析

    本文提出了一种有效的方法来严格检查神经网络的不同安全属性，可以检查不同的安全属性并找到具体的反例，比现有方法的性能提高了数个数量级，这种方法也有助于提高神经网络的可解释性并指导训练更加稳健的神经网络。

    Sep, 2018

  • 深度神经网络的神经符号验证

    文章介绍了一种基于神经网络和逻辑规范的神经符号验证框架 Neuro-symbolic Verification，使得现有的神经网络验证基础设施可用于分析复杂的实际特性，从而避免现有神经网络验证技术的严重局限。

    Mar, 2022

  • 使用高效的边界传播和并行计算扩展深度神经网络验证工具的规模

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

    Dec, 2023

  • 神经网络的自动修复

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

    Jul, 2022

  • 以符号区间增强基于梯度的攻击

    本文提出了一种新技术即区间攻击来评估神经网络的鲁棒性，利用符号区间传播技术来定位包含对抗性实例的潜在区域，研究表明区间攻击可以比现有的渐进式梯度下降攻击发现更多的违规情况达 47%。

    Jun, 2019

  • 使用 iSAT 验证 S 形人工神经网络

    本文提出了一种用于验证非线性人工神经网络（ANNs）行为的方法，并将一种专用的区间约束传播器与 iSAT SMT 求解器相结合，将其与通过 iSAT 中可用的基本算术特征对 S 型函数进行编码的组合方法和逼近方法进行比较。实验结果表明，专用方法和组合方法明显优于逼近方法，并且在所有基准测试中，专用方法的性能与组合方法相当或更好。

    Jul, 2022