- 基于图像的神经网络控制系统的可扩展代理验证：组合和展开方法
通过使用条件生成对抗网络和系统动力学，我们提出了一种针对神经网络控制系统安全验证的方法，减少了单步误差和多步误差，并通过计算准确的可达集来实现较好的可扩展性。
- 深度神经网络控制系统的定性与定量安全验证统一
通过定性和定量安全性验证问题的综合合成有效的神经屏障证书，本文提出了一种用于 DNN 控制系统的新型框架，并通过 $ extsf {UniQQ}$ 工具在四个经典 DNN 控制系统上展示了其有效性。
- DRNet：基于深度强化学习的自动车道变更决策方法
机器学习在自主驾驶车辆的决策制定中优于许多基于规则的方法，我们通过提出一种基于强化学习的框架 'DRNet'，使用深度强化学习 (DRL) 来改进车道切换，并结合安全验证来确保只选择安全动作。
- ReLU 神经控制屏障函数的精确验证
通过使用 ReLu 激活函数的前馈神经控制屏障函数，本研究提出了一种新颖的确保安全性的条件和算法，解决了难以在非光滑控制屏障函数上进行传统安全验证的问题。
- 从拓扑学角度验证神经网络的安全性
本文提出了一种基于拓扑视角的集边界可达性方法，通过利用神经网络的同胚性质和开映射性质来实现对神经网络输入集合和输出集合之间边界特性的研究，从而实现安全验证问题的解决。
- 利用保证神经网络模型简化进行神经网络控制系统的安全验证
本文提出了一种神经网络模型减缩的方法，通过精确计算模型减缩精度，将减缩后的神经网络控制器替换成封闭回路系统，进而提高安全验证的计算效率，并通过自适应巡航控制系统的案例验证了方法的有效性。
- 可达多面体线性搜索 (RPM)：深度学习控制系统的精确分析工具
本篇文章介绍了使用一种新的算法来计算具有 ReLU 激活的深层神经网络的正向和反向可达性集，通过对输入空间中的每个多面体区域的逐步枚举来建立可达集，进而得出控制系统中具有神经网络的不变集和吸引域（ROAs），并且还提出了一种加速 ROAs - 基于集合边界分析的神经网络安全验证
本文提出了一种基于拓扑学视角的集合边界可达性方法，通过利用神经网络的同胚性质，仅需对输入集合的边界进行可达性分析，从而实现神经网络在安全验证问题上的应用。
- 验证学习为基础的安全关键航空系统的认证框架
本文提出了一种针对航空系统中基于学习的组件进行设计时间和运行时保证的安全验证框架，该框架整合了两种新方法：同时考虑了离线和在线验证机制，并且允许各个模块使用独立的方法和技术进行开发，以满足系统不同阶段的安全性要求，从而实现系统产品的持续学习 - OVERT：面向非线性系统神经网络控制策略安全验证的算法
使用 OVERT 算法结合经典形式化方法和新型神经网络验证方法，为验证深度学习控制策略的非线性闭环离散动态系统提供了一种确定性算法。该方法通过计算可达集或直接解决可行性查询来实现有界时间安全性证明，并在计算时间和可达集的精度方面优于现有的方 - 通过半定规划实现具有神经网络控制器的闭环系统的可达性分析
本文提出使用新颖的前向可达性分析方法以验证具有神经网络的时间变化系统的安全性，并举例证明其在四旋翼控制系统中的实用性。
- ReachNN: 神经网络控制系统的可达性分析
本篇研究论文提出了一种新的 reachability analysis 方法，通过 Bernstein 多项式可以验证具有广泛的激活函数形式的神经网络控制系统的安全性，同时基于 Lipschitz 连续性提供了理论误差界估计和实际采样误差界 - 利用二次约束和半定规划进行神经网络的安全验证和鲁棒性分析
通过半定规划的框架来解决对于神经网络在输入不确定性和对抗攻击下的安全性和强鲁棒性认证的问题，通过抽象出激活函数的各种性质，分析其安全性质，解决了保守性和计算效率的平衡问题，并且可以应用于安全认证以外的问题。
- AAAI前馈神经网络符合规范的安全验证
该论文提出了一种基于规范引导的安全验证方法，针对具有一般激活函数的前馈神经网络进行验证，使用区间分析方法进行计算，并开发了一个高效的算法来完成安全验证，实验结果表明该方法具有更高的效率和更少的计算代价。
- IJCAI使用可证明保证的方式对深度神经网络进行可达性分析
本文研究针对前馈深度神经网络的通用可达性问题，通过计算输出函数值的下限和上限，得到区间范围内的可达值，从而得出安全性验证问题、输出范围分析问题和鲁棒性度量，并通过自适应嵌套优化的新算法，有效地解决了可达性问题。
- 具有神经网络控制器的分段线性系统可达集估计与安全验证
本文提出了使用神经网络控制器的分段线性系统的可达集估算和安全性验证问题，并开发了一种逐层方法来计算修正线性单位激活函数神经网络的输出可达集。基于神经网络控制器输出可达集，可以迭代地为给定的有限时间间隔估算分段线性反馈控制系统的输出可达集，并 - 使用 ReLU 激活函数的神经网络可达集计算与安全验证
该论文探讨了一类由 ReLU 激活函数构成的神经网络的输出可达集计算和安全验证问题，并提出了一种逐层计算输出可达集的方法，通过计算输出可达集的结果，可以通过检查不安全区域与由一组多面体描述的输出可达集的交集来执行简单有效的安全验证。