Jun, 2023

numpy 快速区间算术工具箱及其在神经网络控制系统形式验证中的应用

PDF
TL;DR本文介绍了一个基于 numpy 的区间分析工具箱，用于神经网络控制系统的形式验证，利用自然包容函数系统地构建了一般映射的区间边界，并通过自然包容函数的组合，提供了一种用于动态神经网络控制器的形式验证的方法。
interval analysisnumpy toolboxformal verificationneural network controlled systemsnatural inclusion functions
发现论文，激发创造
  • 神经网络控制系统中的正向不变性

    本论文提出了一种基于区间分析和单调系统理论的框架，用于在具有神经网络控制器的非线性系统中证明和搜索正向不变集。

    Sep, 2023

  • 神经网络反馈循环的高效交互感知区间分析

    本研究提出了一种计算效率高的方法，用于神经网络控制系统的区间可达性问题。通过引入包含函数来构建神经网络控制器和开环系统，并基于函数雅各比矩阵的边界介绍并分析了一类适用于捕获系统和神经网络控制器之间相互作用的开环动力学的包含函数。基于包含函数，构建了一个比原系统状态数多两倍的嵌入系统，并证明该嵌入系统的单一轨迹提供了可达集的超矩形过估计。最后，通过两种不同的方式构建了一个闭环嵌入系统，以考虑系统和控制器之间的交互作用。实验证明了本方法在现有基准测试中优于已有方法，同时在一个包含多达 200 个状态的车队编组示例中显示了可扩展性。

    Jul, 2023

  • 神经网络的区间算法基本限制

    本文讨论了区间分析（或区间边界传播，IBP）用于验证和训练可靠机器学习的深度神经网络的可行性问题。研究发现，对于任何深度神经网络分类只有三个点，存在 IBP 无法证明的有效规范。此外，在单隐藏层神经网络的限制情况下，存在一组点，无论采用多少隐藏层，都无法通过区间分析来证明其分类鲁棒性。

    Dec, 2021

  • 使用符号区间对神经网络进行形式化安全分析

    利用区间算法和符号区间分析代替 SMT solver，可以更高效地实现对 DNN 的安全性质进行正式验证，ReluVal 系统相比现有最先进的 solver-based 系统 Reluplex，平均可以提升 200 倍验证效率。

    Apr, 2018

  • 神经网络验证的优化符号化区间传播

    本文提出了一种新的基于符号区间传播和变量分裂的分支定界求解器 DPNeurifyFV，该方法采用新的启发式算法来选择区间变量，以改善变量相关性问题，在结合其他改进措施的情况下，可以显著提高深度学习神经网络验证的效率，并在空中碰撞避免网络 ACAS Xu 上实现了运行时改进。

    Dec, 2022

  • 基于抽象的神经网络输出值范围分析

    本研究探讨了基于 ReLU 激活函数的前馈神经网络的输出范围分析问题，并提出了使用区间神经网络作为抽象技术来简化计算的方法，该方法能够将输出范围分析问题转化为混合整数线性规划问题。实验结果表明了计算时间和计算输出范围精度之间的权衡关系。

    Jul, 2020

  • TIRA: 区间可达性分析工具箱

    TIRA 是 Matlab 库，可用于计算连续和离散非线性系统的可达集区间过估计，通过构造增长 / 收缩界限和单调性概念的结果，当前版本包含四种可达性方法，是一种简单且可扩展的工具。

    Feb, 2019

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

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

    May, 2024

  • 超区间：用超网络方法训练连续学习中的权重区间

    通过嵌入空间内的区间算术和超网络将连续学习中的遗忘问题纳入控制范围，HyperInterval 模型在多项基准测试中获得显著优于 InterContiNet 的结果，并能够训练出一个适用于所有任务的统一网络。

    May, 2024

  • 区间逻辑张量网络

    本文介绍了一种名为 Interval Real Logic（IRL）的两重逻辑，该逻辑使用具有实际特征数据序列来解释知识，我们使用模糊逻辑解释连接词，使用梯形模糊间隔解释事件持续时间，使用间隔面积之间的关系解释模糊时间关系，同时介绍了 Interval Logic Tensor Networks（ILTN）—— 一种通过 IRL 的梯度传播来进行学习的神经符号系统。

    Mar, 2023