Nov, 2023

将神经网络验证扩展到更大的分段线性激活函数家族

PDF
TL;DR本文扩展了一种现有的神经网络验证技术，以支持更广泛的分段线性激活函数类别，并将原始的算法扩展以提供对以起始集表示的有界输入集的精确结果或上估计结果，并允许无界输入集。我们实施了我们的算法，并在一些案例研究中展示了它们的有效性。
发现论文，激发创造
  • 分段线性前馈神经网络的形式化验证

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

    May, 2017

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

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

    Nov, 2017

  • 神经网络中 S 形非线性函数的线性界限函数自动设计

    通过使用一种简单的搜索方法，精心地根据最先进的算法配置技术调整给定的验证问题，我们提出了一种新颖的参数搜索方法来改进这些线性逼近的质量，进而在几个常用的本地鲁棒性验证基准上平均提高了 25% 的全局下界。

    Jun, 2024

  • 分支定界用于分段线性神经网络验证

    研究了深度学习的形式验证以及提出了一种基于分支定界的族算法，并提出了新型的组合方法，以及新的有效的分支策略，将之用于高维输入上的问题，并提出包含以前发布的测试案例的全面测试数据集和基准测试。

    Sep, 2019

  • 具有神经网络控制器的分段线性系统可达集估计与安全验证

    本文提出了使用神经网络控制器的分段线性系统的可达集估算和安全性验证问题，并开发了一种逐层方法来计算修正线性单位激活函数神经网络的输出可达集。基于神经网络控制器输出可达集，可以迭代地为给定的有限时间间隔估算分段线性反馈控制系统的输出可达集，并通过检查不安全区域和输出到达集的交集的存在来执行带有神经网络控制器的分段线性系统的安全性验证。

    Feb, 2018

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

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

    Mar, 2024

  • 分段线性激活显著地塑造了神经网络的损失曲面

    本文介绍分段线性激活函数对神经网络损失曲面的形状有较大的影响，证明了许多神经网络的损失曲面具有无限的虚假局部极小值，将神经网络损失曲面分为多个平滑和多线性细胞。

    Mar, 2020

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

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

    Mar, 2018

  • 分段线性激活函数的神经网络热带方法

    本研究使用热带代数中 generalization 的概念对神经网络中的分段线性激活函数进行统一且独特的处理，将神经网络层看做是一个 tropical polynomial，进一步优化计算线性区域的上界，并提出了一种使用随机抽样有效计算线性区域数量的几何方法。

    May, 2018

  • 神经网络非线性规范的验证

    本文介绍在神经网络验证中如何利用凸松弛来证明一系列比较丰富的非线性规约，包括物理系统学习到的动力学模型的能量守恒，分类器的输出标签在对抗性扰动下的语义一致性以及预测手写数字求和的系统所包含的误差等，实验验证了该方法的有效性。

    Feb, 2019