使用 ReLU 激活函数的神经网络可达集计算与安全验证
本文提出了使用神经网络控制器的分段线性系统的可达集估算和安全性验证问题,并开发了一种逐层方法来计算修正线性单位激活函数神经网络的输出可达集。基于神经网络控制器输出可达集,可以迭代地为给定的有限时间间隔估算分段线性反馈控制系统的输出可达集,并通过检查不安全区域和输出到达集的交集的存在来执行带有神经网络控制器的分段线性系统的安全性验证。
Feb, 2018
研究使用 ReLU 函数实现激活函数的前馈神经网络系统的可达性问题,并通过线性问题对其进行表征,并提出了一种基于最先进的线性规划求解器解决实际问题的方法。通过分析文献中的多个基准测试来评估所提出技术的性能。
Jun, 2017
论文探讨了多层感知器神经网络的输出可达性估计和安全验证问题,引入最大灵敏度的概念,并通过解决凸优化问题计算了一类多层感知器的最大灵敏度。然后,使用基于模拟的方法将神经网络的输出可达集估计问题转化为一系列优化问题,并基于输出可达集估计结果开发了一种自动化的安全验证方法。最后,给出了将所提出的方法应用于具有两个关节的机器人臂模型的安全验证的案例,证明了方法的有效性。
Aug, 2017
本文提出了一种基于拓扑学视角的集合边界可达性方法,通过利用神经网络的同胚性质,仅需对输入集合的边界进行可达性分析,从而实现神经网络在安全验证问题上的应用。
Oct, 2022
本文研究针对前馈深度神经网络的通用可达性问题,通过计算输出函数值的下限和上限,得到区间范围内的可达值,从而得出安全性验证问题、输出范围分析问题和鲁棒性度量,并通过自适应嵌套优化的新算法,有效地解决了可达性问题。
May, 2018
本文提出了一种基于拓扑视角的集边界可达性方法,通过利用神经网络的同胚性质和开映射性质来实现对神经网络输入集合和输出集合之间边界特性的研究,从而实现安全验证问题的解决。
Jun, 2023
本篇研究论文提出了一种新的 reachability analysis 方法,通过 Bernstein 多项式可以验证具有广泛的激活函数形式的神经网络控制系统的安全性,同时基于 Lipschitz 连续性提供了理论误差界估计和实际采样误差界估计方法。与之前的方法相比,这种方法可以应用于包含多种类型激活函数的异构神经网络,实验结果表明有效性。
Jun, 2019
该研究介绍了 UR4NNV 验证框架,它首次利用了 DNN 的欠逼近可达性分析方法,针对具有 ReLU 激活函数的 DNN 并采用基于二叉树分支的欠逼近算法。UR4NNV 有效验证 DNN 属性且在达到验证轮数和未能证伪属性时提供置信水平,实验比较结果显示 UR4NNV 在解决 “未知困境” 方面的有效性和效率,显著减少了影响。
Jan, 2024
本文考虑了使用神经网络控制器的自主机器人的安全性问题。通过构建系统的一个有限状态抽象并使用标准的可达性分析方法,计算出一组安全的初始状态,使得从这些初始状态开始的机器人轨迹能够避开多面体障碍物。
Oct, 2018
该论文提出了一种基于规范引导的安全验证方法,针对具有一般激活函数的前馈神经网络进行验证,使用区间分析方法进行计算,并开发了一个高效的算法来完成安全验证,实验结果表明该方法具有更高的效率和更少的计算代价。
Dec, 2018