Falsification of Autonomous Systems in Rich Environments

📄 arXiv: 2412.17992v1 📥 PDF

作者: Khen Elimelech, Morteza Lahijanian, Lydia E. Kavraki, Moshe Y. Vardi

分类: cs.RO, eess.SY

发布日期: 2024-12-23

💡 一句话要点

提出基于元规划的自主系统验证方法，提升复杂环境下神经网络控制器的安全性。

🎯 匹配领域: 支柱一：机器人控制 (Robot Control)

关键词: 自主系统验证 神经网络控制器 黑盒测试 元规划 运动规划

📋 核心要点

  1. 现有黑盒测试方法验证自主系统时，依赖大量高保真仿真，计算成本高昂，尤其当控制器训练良好时。
  2. 论文提出一种基于元规划的验证方法，将系统验证问题转化为元系统的轨迹规划问题，利用运动规划技术求解。
  3. 实验表明，在具有神经网络控制器的自动驾驶汽车避障场景中，该方法优于其他验证方法，验证效率更高。

📝 摘要（中文）

验证自主网络物理系统(CPS)和人工智能(AI)代理的行为至关重要，尤其当它们依赖于自动控制器时。近年来，神经网络(NN)控制器展现出巨大潜力，但其未经认证的特性可能导致系统出现不可预测或不安全的行为。为了解决这个问题，大量工作致力于系统的自动验证，特别是“黑盒测试”方法，它依赖于重复的系统仿真来寻找违反规范的反例。由于高保真仿真计算量大，验证方法的目标是最小化仿真工作量(NN推理查询)以找到反例。当被测控制器训练良好时，这通常是一个巨大的挑战。本文提出了一种新的自主系统验证方法，用于在不确定环境中运行的正式规范下的系统。我们特别关注在语义定义的开放环境中运行的CPS，这些环境产生高维、依赖于仿真的传感器观测。我们的方法将验证问题重新表述为“元系统”的轨迹规划问题，该元系统封装了被测系统；我们称之为元规划。这种公式可以使用标准的基于采样的运动规划技术(如RRT)解决，并可以逐步整合领域知识以改进搜索。我们通过对具有NN控制器的避障自动驾驶汽车的验证实验，证明了元规划优于其他方法。

🔬 方法详解

问题定义：论文旨在解决自主系统，特别是使用神经网络控制器的自主系统，在复杂、不确定环境中运行时的安全性验证问题。现有黑盒测试方法需要大量的仿真来寻找违反安全规范的反例，计算成本高昂，难以有效验证训练良好的控制器。

核心思路：论文的核心思路是将原始系统的验证问题转化为一个“元系统”的轨迹规划问题。元系统封装了原始系统，并通过规划元系统的轨迹来探索原始系统可能出现的危险行为。这种转变使得可以使用成熟的运动规划算法来解决验证问题。

技术框架：该方法的核心是构建一个“元系统”，该系统包含原始系统（例如，自动驾驶汽车及其控制器）以及环境模型。然后，使用基于采样的运动规划算法（例如RRT）在元系统的状态空间中搜索轨迹。轨迹的成本函数被设计为反映违反安全规范的程度。通过优化轨迹，可以找到导致系统违反安全规范的反例。整体流程包括：1. 定义原始系统和环境；2. 构建元系统；3. 使用运动规划算法搜索元系统轨迹；4. 评估轨迹的安全性；5. 如果找到反例，则输出；否则，继续搜索。

关键创新：该方法最重要的创新点在于将验证问题转化为轨迹规划问题。这种转变使得可以使用现有的运动规划算法来解决验证问题，并可以方便地整合领域知识来指导搜索过程。与传统的黑盒测试方法相比，该方法能够更有效地探索系统的状态空间，从而更快地找到反例。

关键设计：关键设计包括：1. 元系统的状态空间定义，需要包含原始系统的状态和环境的状态；2. 轨迹的成本函数设计，需要能够准确地反映违反安全规范的程度；3. 运动规划算法的选择，需要能够有效地探索高维状态空间；4. 领域知识的整合方式，例如，可以使用启发式函数来指导搜索过程。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，在自动驾驶汽车避障场景中，基于元规划的验证方法比其他黑盒测试方法表现更优。具体来说，该方法能够更快地找到违反安全规范的反例，从而减少了仿真所需的计算资源。论文中虽然没有给出具体的性能数据和提升幅度，但强调了元规划方法在效率上的优势。

🎯 应用场景

该研究成果可应用于各种自主系统的安全性验证，例如自动驾驶汽车、无人机、机器人等。通过在设计阶段进行验证，可以及早发现潜在的安全隐患，从而提高系统的可靠性和安全性。此外，该方法还可以用于评估不同控制器的性能，并选择最适合特定应用场景的控制器。未来，该方法有望成为自主系统开发流程中的一个重要组成部分。

📄 摘要（原文）

Validating the behavior of autonomous Cyber-Physical Systems (CPS) and Artificial Intelligence (AI) agents, which rely on automated controllers, is an objective of great importance. In recent years, Neural-Network (NN) controllers have been demonstrating great promise. Unfortunately, such learned controllers are often not certified and can cause the system to suffer from unpredictable or unsafe behavior. To mitigate this issue, a great effort has been dedicated to automated verification of systems. Specifically, works in the category of black-box testing'' rely on repeated system simulations to find a falsifying counterexample of a system run that violates a specification. As running high-fidelity simulations is computationally demanding, the goal of falsification approaches is to minimize the simulation effort (NN inference queries) needed to return a falsifying example. This often proves to be a great challenge, especially when the tested controller is well-trained. This work contributes a novel falsification approach for autonomous systems under formal specification operating in uncertain environments. We are especially interested in CPS operating in rich, semantically-defined, open environments, which yield high-dimensional, simulation-dependent sensor observations. Our approach introduces a novel reformulation of the falsification problem as the problem of planning a trajectory for ameta-system,'' which wraps and encapsulates the examined system; we call this approach: meta-planning. This formulation can be solved with standard sampling-based motion-planning techniques (like RRT) and can gradually integrate domain knowledge to improve the search. We support the suggested approach with an experimental study on falsification of an obstacle-avoiding autonomous car with a NN controller, where meta-planning demonstrates superior performance over alternative approaches.