Feb, 2024

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

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

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

    Oct, 2018

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

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

    Jan, 2023

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

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

    Dec, 2023

  • 深度神经网络控制系统的定性与定量安全验证统一

    通过定性和定量安全性验证问题的综合合成有效的神经屏障证书，本文提出了一种用于 DNN 控制系统的新型框架，并通过 $ extsf {UniQQ}$ 工具在四个经典 DNN 控制系统上展示了其有效性。

    Apr, 2024

  • 应用 Lyapunov 障碍证书对深度强化学习控制器进行形式化验证

    我们提出了一种新的方法来训练和验证基于 NLB 的证书，通过证书的序列设计和过滤来简化验证过程，并与神经网络验证引擎一起提供正式保证，以确保 DRL 代理实现其目标并避免不安全行为，通过在 DRL 控制的航天器上进行案例研究展示了该方法的优点。

    May, 2024

  • 系统级安全防护：通过不确定的神经网络动力学模型实现安全跟踪控制

    利用神经网络作为预测模型来解决具有不确定性的动力系统的轨迹跟踪问题，并通过混合整数线性规划方法提供了整体系统的安全保证。

    Dec, 2023

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

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

    Oct, 2022

  • 面向安全关键深度神经网络的可扩展验证

    本篇论文介绍了在安全重要应用领域中使用深度神经网络的问题，针对其可靠性和安全性的担忧，提出了采用形式化验证来保证其运行符合预期，并通过两个方向，即设计可扩展性的验证技术和识别可验证的深度学习系统的设计选择来缓解这一挑战。

    Jan, 2018

  • 基于图像的神经网络控制系统的可扩展代理验证：组合和展开方法

    通过使用条件生成对抗网络和系统动力学，我们提出了一种针对神经网络控制系统安全验证的方法，减少了单步误差和多步误差，并通过计算准确的可达集来实现较好的可扩展性。

    May, 2024

  • 深入探究：机器学习验证和验证综述及在汽车工业中的挑战探讨

    本文回顾了关于深度神经网络在安全关键系统中验证和验证方面的现有技术，并建议飞行器到汽车的知识转移和系统级的安全方法，例如安全笼架架构和模拟的系统测试案例。

    Dec, 2018