Apr, 2020

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

PDF
TL;DR本文介绍神经网络验证（NNV）软件工具，该工具为深度神经网络（DNN）和学习启用的控制系统（CPS）提供了一套基于集合的验证框架。NNV 的核心是一组可达性算法，这些算法利用了多种集合表示，例如，多面体、恒星集、zono topes 和抽象域表示。
neural network verificationset-based verification frameworkreachability algorithmslearning-enabled cyber-physical systemsfeed-forward neural networks
发现论文，激发创造
  • UR4NNV：神经网络验证，欠估计可达性研究！

    该研究介绍了 UR4NNV 验证框架，它首次利用了 DNN 的欠逼近可达性分析方法，针对具有 ReLU 激活函数的 DNN 并采用基于二叉树分支的欠逼近算法。UR4NNV 有效验证 DNN 属性且在达到验证轮数和未能证伪属性时提供置信水平，实验比较结果显示 UR4NNV 在解决 “未知困境” 方面的有效性和效率，显著减少了影响。

    Jan, 2024

  • 验证友好的深度神经网络

    提出了一种生成可验证的神经网络（VNNs）的新框架，该框架通过后训练优化在保留预测性能和鲁棒性之间取得平衡，使得生成的网络在预测性能方面与原始网络相当，并且可以进行验证，以更加高效地建立 VNNs 的强大性。

    Dec, 2023

  • 使用高效的边界传播和并行计算扩展深度神经网络验证工具的规模

    深度神经网络在安全方面的正式验证问题已经扩展到计数版本 (DNN-Verification)，为了在给定安全属性的领域中计算不安全区域的数量。为了解决这个问题的复杂性，本研究提出了一种基于可达性分析、符号线性松弛和并行计算的新策略，以增强现有的精确和近似 DNN 计数的形式验证的效率。在标准的形式验证基准和现实的机器人场景上进行的实证评估表明，在可扩展性和效率方面都取得了显著的改进，使得这种技术能够用于复杂的机器人应用。

    Dec, 2023

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

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

    Jan, 2023

  • 基于集合边界分析的神经网络安全验证

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

    Oct, 2022

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

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

    Oct, 2018

  • 二值化神经网络的高效精确验证

    本文提出了一种基于 Binarized Neural Networks（BNNs）的验证技术（EEV），可以具有可比较的鲁棒性，并且通过使用一种策略来训练鲁棒性 BNNs，可以实现更快，更准确的验证。EEV 有效，通过在 MNIST 和 CIFAR10 数据集上展示非平凡卷积 BNN 的 L-inf-bounded 对抗性鲁棒性的首个确切验证结果可以进行性能优化。

    May, 2020

  • 神经网络验证的基于抽象的框架

    本研究提出了一种通过使用过度逼近来减小神经网络规模，以提高神经网络验证技术的框架，并使用反例引导调整逼近，以验证大型神经网络。实验证明，该方法对验证大型神经网络具有很大的潜力。

    Oct, 2019

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

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

    Feb, 2024

  • 从拓扑学角度验证神经网络的安全性

    本文提出了一种基于拓扑视角的集边界可达性方法，通过利用神经网络的同胚性质和开映射性质来实现对神经网络输入集合和输出集合之间边界特性的研究，从而实现安全验证问题的解决。

    Jun, 2023