May, 2023

神经网络中的原像逼近

PDF
TL;DR研究了神经网络的全局鲁棒性问题，提出了一种在量化验证中高效的、基于线性松弛的生成符号下逼近的先验图像的算法。
发现论文，激发创造
  • 可证明边界的神经网络原像

    本文介绍了第一个有效的边界传播算法 INVPROP，用于在神经网络的线性约束输出集的原像上验证属性，并可以与分支和限制相结合以实现完整性。我们的算法在安全控制区域量化和神经网络中检测超出分配的输入方面具有应用价值，并且在相同硬件上比先前的工作快 2.5 倍，可以找到超过 2500 倍的最紧近似。

    Feb, 2023

  • 神经网络的逆问题

    利用神经网络和分段线性激活函数计算集合的原像问题，证明了多面体集合的原像仍然是多面体集合的并集且可有效计算，展示了计算神经网络原像在分析和解释性方面的几个应用。

    Aug, 2023

  • 使用超属性验证全局神经网络规范

    本研究引入超属性形式主义，提供了表达全局规范的方法，可以通过利用验证通用计算图形的能力验证全局规范，从而扩大了使用现有方法提供的保证范围。

    Jun, 2023

  • 神经网络验证的基于抽象的框架

    本研究提出了一种通过使用过度逼近来减小神经网络规模，以提高神经网络验证技术的框架，并使用反例引导调整逼近，以验证大型神经网络。实验证明，该方法对验证大型神经网络具有很大的潜力。

    Oct, 2019

  • 生成模型的鲁棒性认证

    本论文提出了一种可扩展的证明方法 ——ApproxLine，可用于验证涉及生成模型和分类器的非平凡规范，并提供有限的非凸集合或这些集合上的分布的确定性和概率保证。

    Apr, 2020

  • 神经网络中的鲁棒性验证

    我们研究了神经网络计算的形式验证问题，探讨了其各种鲁棒性和最小化问题。我们提供了一个理论框架，使我们能够在神经网络中转换安全性和效率问题，并分析它们的计算复杂性。我们发现，在半线性设置中，对于分段线性激活函数和使用求和或最大度量时，大多数问题都属于 P 类或最多属于 NP 类。

    Mar, 2024

  • 学习神经网络验证的最小 NAP 规范

    给定一个神经网络，找到足以形式验证网络鲁棒性的最小（最粗略）NAP。

    Apr, 2024

  • 两种近似算法的故事：通过欠 - 过估算收紧 DNN 的稳健性验证

    本文研究了神经网络鲁棒性的形式化验证，提出了一种新的双重逼近方法，利用激活函数的低估区间来定义紧逼近边界，并将其实现到了名为 DualApp 的工具中，在不同体系结构的深度神经网络基准测试中，DualApp 方法得到了明显的优化

    May, 2023

  • 神经网络对不变映射的通用逼近

    我们将神经网络的普适逼近定理推广到对于线性表示组不变或等变的映射，以建立一种像网络一样的计算模型，能够在能够逼近任何连续不变 / 等变映射的同时保持不变 / 等变。我们提出了完备的不变 / 等变网络的构造，通过引入中间多项式层，通过 Hilbert 和 Weyl 的定理证明了我们的构造方法。我们提出了适用于 SE（2）群的 “电荷守恒卷积” 模型，并证明其是连续 SE（2）等变信号变换的通用逼近器。

    Apr, 2018

  • 神经网络验证的优化符号化区间传播

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

    Dec, 2022