Mar, 2023

POLAR-Express: 神经网络控制系统的高效而精确的正式可达性分析

PDF
TL;DR本文介绍了 POLAR-Express，一种用于验证神经网络控制系统的安全性的高效而精确的正式可达性分析工具。该工具使用泰勒模型算术来跨越神经网络层层传播泰勒模型从而计算神经网络函数的近似值，能够分析任何具有连续激活函数的前馈神经网络。文章中还提出了一种在 ReLU 激活函数上更加高效和精确传播泰勒模型的新方法。在多个数据集上的对比实验表明，POLAR-Express 在可达性分析中取得了最佳的效率和可靠性。
发现论文，激发创造
  • ReachNN: 神经网络控制系统的可达性分析

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

    Jun, 2019

  • 使用符号卓诺托普和多边形卓诺托普验证神经网络控制系统

    本文提出了一种基于包含保持长期符号依赖性建模的组合方法，旨在分析神经网络控制系统的验证和安全评估，并通过数值实例和基准测试来评估该方法的有效性。

    Jun, 2023

  • 神经网络控制自主系统的形式化验证

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

    Oct, 2018

  • 通过半定规划实现具有神经网络控制器的闭环系统的可达性分析

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

    Apr, 2020

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

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

    Feb, 2018

  • 神经反馈回路的可达性分析

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

    Aug, 2021

  • 神经网络控制系统可达性分析

    该论文提出了一种基于 Lipschitzian 优化的 NNCS 验证框架，通过证明闭环 NNCS 的 Lipschitz 连续性并消除循环来实现，相比最先进的验证方法，DeepNNC 在各种 NNC 的效率和准确性方面表现更加优秀，并通过实际的案例展示了 DeepNNC 处理复杂系统的能力。

    Jan, 2023

  • 安全控制策略的神经证书

    本文提出一种方法，通过联合学习障碍函数和类李亚普诺夫函数的神经网络来实现动态系统的安全和目标控制，该方法在摆、小车倒立杆和无人机等动态系统中得到了有效应用。

    Jun, 2020

  • 通过差分动态逻辑证明安全的神经网络控制器

    通过使用差分动态逻辑（dL）和神经网络验证相结合的方法，我们引入了 VerSAILLE（通过逻辑链接的包络来确保安全的人工智能）来解决神经网络控制系统（NNCS）的安全性验证问题，同时提出了 Mosaic 来处理多项式实数算术性质在分段线性神经网络上的验证问题。我们的方法支持无限时间范围的安全性认证以及详尽枚举反例区域，并且在关闭环路的 NNV 中明显胜过现有的工具。

    Feb, 2024

  • 高维可达性形式化安全保证生成

    提供自治系统的正式安全性和性能保证变得越来越重要，本文提出一种提供可达管的可证安全近似解的方法，该方法可以通过计算 DeepReach 解的误差界来进行可达管的修正，并通过基于情景优化的方法来推导 DeepReach 解的误差界等.

    Sep, 2022