AAAIJan, 2023

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

PDF
TL;DR该论文提出了一种基于 Lipschitzian 优化的 NNCS 验证框架，通过证明闭环 NNCS 的 Lipschitz 连续性并消除循环来实现，相比最先进的验证方法，DeepNNC 在各种 NNC 的效率和准确性方面表现更加优秀，并通过实际的案例展示了 DeepNNC 处理复杂系统的能力。
neural network controllersverificationlipschitzian optimisationcyber-physical systemsadaptive cruise control
发现论文，激发创造
  • ReachNN: 神经网络控制系统的可达性分析

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

    Jun, 2019

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

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

    Oct, 2018

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

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

    Feb, 2024

  • 利用保证神经网络模型简化进行神经网络控制系统的安全验证

    本文提出了一种神经网络模型减缩的方法，通过精确计算模型减缩精度，将减缩后的神经网络控制器替换成封闭回路系统，进而提高安全验证的计算效率，并通过自适应巡航控制系统的案例验证了方法的有效性。

    Jan, 2023

  • 连续时间下神经网络控制系统的验证

    通过为连续驱动的神经网络控制系统添加抽象层，我们开发了第一个连续驱动的神经网络控制系统验证方法，并通过应用于基于视觉的自主飞机滑行系统，并与固定频率分析基线进行比较，展示了该方法的有效性。

    May, 2024

  • NNV: 面向深度神经网络和学习增强型的网络物理系统的神经网络验证工具

    本文介绍神经网络验证（NNV）软件工具，该工具为深度神经网络（DNN）和学习启用的控制系统（CPS）提供了一套基于集合的验证框架。NNV 的核心是一组可达性算法，这些算法利用了多种集合表示，例如，多面体、恒星集、zono topes 和抽象域表示。

    Apr, 2020

  • 基于组合归纳不变式的神经网络控制系统验证

    本文介绍了一种针对神经网络控制系统（NNCS）安全验证的新方法，利用归纳不动点方法，并配合自动推断必要的分解谓词的算法，将验证过程从数小时（甚至超时）缩短至几秒钟，在案例研究中显著提高了验证性能。

    Dec, 2023

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

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

    Aug, 2021

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

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

    Apr, 2020

  • 深度神经网络上的模型无关可达性分析

    本文提出一种模型无关的验证框架 DeepAgn，通过 reachability analysis，可以解决计算给定输入的最大安全半径和生成地面实际的例子等多个已知鲁棒性问题，尤其适用于处理包括 FNN 和 RNN 在内的复杂深层神经网络的验证。

    Apr, 2023