该论文探讨了一类由 ReLU 激活函数构成的神经网络的输出可达集计算和安全验证问题，并提出了一种逐层计算输出可达集的方法，通过计算输出可达集的结果，可以通过检查不安全区域与由一组多面体描述的输出可达集的交集来执行简单有效的安全验证。

Dec, 2017

论文探讨了多层感知器神经网络的输出可达性估计和安全验证问题，引入最大灵敏度的概念，并通过解决凸优化问题计算了一类多层感知器的最大灵敏度。然后，使用基于模拟的方法将神经网络的输出可达集估计问题转化为一系列优化问题，并基于输出可达集估计结果开发了一种自动化的安全验证方法。最后，给出了将所提出的方法应用于具有两个关节的机器人臂模型的安全验证的案例，证明了方法的有效性。

Aug, 2017

本文提出使用新颖的前向可达性分析方法以验证具有神经网络的时间变化系统的安全性，并举例证明其在四旋翼控制系统中的实用性。

Apr, 2020

本研究提出了一种用于神经网络控制的闭环系统的可触及性分析的凸优化框架，通过新的输入集分割技术，该框架大大减少了紧密间隔，从而显著提高了计算速度。该方法还提供了一种新的用于反向可达性分析的算法，以确保系统从某个状态达到目标状态。数值实验表明，与最先进的方法相比，该方法在更短的计算时间内具有更少的保守性，能够处理各种难以处理的系统，例如具有非线性动力学和不确定性源的系统。

Aug, 2021

研究使用 ReLU 函数实现激活函数的前馈神经网络系统的可达性问题，并通过线性问题对其进行表征，并提出了一种基于最先进的线性规划求解器解决实际问题的方法。通过分析文献中的多个基准测试来评估所提出技术的性能。

Jun, 2017

本篇研究论文提出了一种新的 reachability analysis 方法，通过 Bernstein 多项式可以验证具有广泛的激活函数形式的神经网络控制系统的安全性，同时基于 Lipschitz 连续性提供了理论误差界估计和实际采样误差界估计方法。与之前的方法相比，这种方法可以应用于包含多种类型激活函数的异构神经网络，实验结果表明有效性。

Jun, 2019

本文考虑了使用神经网络控制器的自主机器人的安全性问题。通过构建系统的一个有限状态抽象并使用标准的可达性分析方法，计算出一组安全的初始状态，使得从这些初始状态开始的机器人轨迹能够避开多面体障碍物。

Oct, 2018

本文提出了一种基于拓扑学视角的集合边界可达性方法，通过利用神经网络的同胚性质，仅需对输入集合的边界进行可达性分析，从而实现神经网络在安全验证问题上的应用。

Oct, 2022

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

Nov, 2017

本文研究针对前馈深度神经网络的通用可达性问题，通过计算输出函数值的下限和上限，得到区间范围内的可达值，从而得出安全性验证问题、输出范围分析问题和鲁棒性度量，并通过自适应嵌套优化的新算法，有效地解决了可达性问题。

May, 2018