1. 论文基本信息

1.1. 标题

统一深度神经网络控制系统定性与定量安全验证 (Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems)

1.2. 作者

• Dapeng Zhi (East China Normal University)
• Pei Wang (Nanyang Technological University)
• Long Li (Nanyang Technological University)
• Min Zhang (East China Normal University)
• Si Liu (ETH Zurich)

1.3. 发表期刊/会议

该论文发布在 arXiv 预印本平台 (arXiv:2404.01769v1)，并根据致谢部分，该工作已得到 CAV 2024 (Computer Aided Verification) 的评审。CAV 是形式化验证领域顶级的国际会议之一，享有极高的声誉和影响力。

1.4. 发表年份

2024年4月2日 (UTC)。

1.5. 摘要

深度强化学习 (Deep Reinforcement Learning, DRL) 技术的迅速发展使得利用深度神经网络 (Deep Neural Networks, DNNs) 监督安全关键系统成为可能，这迫切需要为这类 DNN 控制系统建立经过认证的安全保证。现有的大多数验证方法依赖于定性方法，主要采用可达性分析 (reachability analysis)。然而，当 DNN 控制系统在开放和对抗性环境中运行时，其行为表现出随机性 (stochastic tendencies)，这使得定性验证显得不足。

本文提出了一种新颖的框架，用于统一 DNN 控制系统的定性与定量安全验证问题。该框架通过将验证任务表述为合成有效的神经障碍证书 (Neural Barrier Certificates, NBCs) 来实现这一目标。首先，该框架尝试通过定性验证建立几乎肯定安全 (almost-sure safety) 保证。如果定性验证失败，则会调用其定量验证方法，在无限和有限时间范围内提供概率安全的精确下界和上界。为了促进 NBC 的合成，本文引入了它们的 $k$-归纳 (k-inductive) 变体。此外，作者还设计了一种仿真引导 (simulation-guided) 方法来训练 NBC，旨在计算精确认证下界和上界的紧密度 (tightness)。作者将所提出的方法原型化为工具 UniQQ，并在四个经典的 DNN 控制系统上展示了其有效性。

1.6. 原文链接

• 原文链接 (arXiv abstract page): https://arxiv.org/abs/2404.01769v1
• PDF 链接: https://arxiv.org/pdf/2404.01769v1.pdf

2. 整体概括

2.1. 研究背景与动机

论文试图解决的核心问题： 本文旨在解决深度神经网络 (DNN) 控制系统在复杂、开放且存在不确定性的环境中运行时，如何提供可信赖、可认证的安全性保证问题。传统的定性安全验证方法（如可达性分析）在处理 DNN 控制系统固有的随机性和不确定性（例如环境噪声、传感器误差、甚至恶意攻击）时存在局限性，无法提供足够的保证。

为什么这个问题在当前领域是重要的： 随着深度强化学习 (DRL) 技术在自动驾驶、机器人、航空航天等安全关键领域中的广泛应用，确保由 DNN 驱动的自主系统能够安全运行变得至关重要。一个 DNN 控制系统如果不能保证其行为的安全性，可能会导致灾难性的后果。因此，建立一套能够量化和认证这些系统安全性的方法，是推动其在实际应用中落地的关键。

现有研究存在的具体挑战或空白 (Gap)：

1. 定性验证的局限性： 大多数现有方法仅提供定性结果（例如，系统是否几乎肯定安全），但当系统存在随机性时，仅知道“安全或不安全”是不够的，需要知道“有多大可能安全”。
2. 定量验证的挑战： 针对 DNN 控制系统的定量验证面临巨大困难：
   • DNN 模型的复杂性和不可解释性： 难以构建忠实的基于自动机的概率模型。
   • 连续和无限状态空间： 传统模型检测方法容易遭受状态空间爆炸问题。
   • 非线性动力学： 使得分析更加复杂。
   • 状态探索问题： 即使在有界步骤和状态抽象下，验证也可能耗时巨大。
3. 缺乏统一框架： 现有方法往往专注于定性或定量验证的某一方面，缺乏一个能够统一处理这两种需求，并能适应不同时间范围（有限/无限）和提供不同形式（线性/指数）安全界限的综合性框架。

这篇论文的切入点或创新思路： 本文通过利用神经障碍证书 (Neural Barrier Certificates, NBCs) 作为核心工具，将定性验证和定量验证统一到一个框架中。NBCs 结合了障碍证书的形式化保证和神经网络强大的表达能力，可以有效处理 DNN 的非线性和连续状态空间。通过为不同类型的安全验证问题（定性、无限时间定量、有限时间定量）设计特定的 NBC 条件，并引入 $k$-归纳变体来放松验证条件，以及通过仿真引导训练来提高界限的紧密度，从而构建了一个全面且实用的验证方法。

2.2. 核心贡献/主要发现

论文的主要贡献概括如下：

1. 统一的验证框架： 提出了一个新颖的框架，通过将所有验证问题（定性与定量）归结为合成神经障碍证书 (NBCs) 的任务，实现了 DNN 控制系统的定性与定量安全验证的统一。
2. 丰富的理论基础：
   • 为定性安全验证和定量安全验证（包括无限和有限时间范围）建立了新的 NBC 约束条件。
   • 提出了用于量化安全概率的线性形式和指数形式的下界和上界。
3. 加速 NBC 合成：
   • 引入了 NBC 的 $k$-归纳 (k-inductive) 变体，通过放松约束条件来加速训练过程，同时仍能提供安全保证。
   • 提出了一种仿真引导 (simulation-guided) 训练方法，旨在提高 NBC 计算安全界限的紧密度。
4. 原型工具与实证验证： 开发了名为 UniQQ 的原型工具，并在四个经典的 DNN 控制系统上验证了其有效性，展示了在各种噪声场景下提供定性与定量安全保证的能力。实验结果表明 $k$-归纳变体平均减少了 25% 的验证开销，仿真引导训练方法将界限的紧密度提高了高达 47.5%。

3. 预备知识与相关工作

3.1. 基础概念

为了理解本文提出的统一安全验证框架，需要掌握以下几个基础概念：

3.1.1. 深度神经网络控制系统 (DNN-Controlled Systems)

这是本文研究的对象。一个 DNN 控制系统 (DNN-controlled system) $M = (S, S_0, A, \pi, f, R)$ 是一个决策系统，它持续与环境交互。

• $S \subseteq \mathbb{R}^n$：系统的状态空间，可能是连续和无限的。

• $S_0 \subseteq S$：初始状态集合。

• $A$：动作集合。

• $\pi: S \to A$：由神经网络实现的控制策略 (policy)，它根据当前状态决定采取什么动作。

• $f: S \times A \to S$：系统动力学 (system dynamics)，描述了在给定当前状态和动作后，系统如何演变为下一个状态。

• $R: S \times A \times S \to \mathbb{R}$：奖励函数 (reward function)。

  轨迹 (Trajectories)：从初始状态 $s_0 \in S_0$ 开始，系统在每个时间步 $t \in \mathbb{N}_0$ 观察状态 $s_t$，通过策略 $\pi$ 计算动作 a_t = \pi(s_t)，然后通过系统动力学 $f$ 转移到下一个状态 $s_{t+1} = f(s_t, a_t)$。由此产生的一系列状态序列 $\omega = \{s_t\}_{t \in \mathbb{N}_0}$ 称为轨迹。

状态扰动 (State Perturbations)：由于传感器误差、设备不准确或对抗性攻击，系统观测到的状态 $\hat{s}_t$ 可能会受到扰动。形式上，$\hat{s}_t := s_t + \delta_t$，其中 $\delta_t \sim \mu$ 是一个随机噪声 (random noise)，$\mu$ 是 $\mathbb{R}^n$ 上的概率分布。$\mathsf{supp}(\mu)$ 表示 $\mu$ 的支持集 (support set)，记为 $W$。因此，实际的后继状态是 $s_{t+1} := f(s_t, \hat{a}_t)$，其中 $\hat{a}_t := \pi(\hat{s}_t)$。一个被噪声分布 $\mu$ 扰动的 DNN 控制系统记作 $M_\mu = (S, S_0, A, \pi, f, R, \mu)$。

概率空间 (Probability Space)：对于每个初始状态 $s_0 \in S_0$，存在一个概率空间 $(\Omega_{s_0}, \mathcal{F}_{s_0}, \mathbb{P}_{s_0})$，其中 $\Omega_{s_0}$ 是从 $s_0$ 开始的所有轨迹的集合，$\mathcal{F}_{s_0}$ 是其上的 $\sigma$-代数，$\mathbb{P}_{s_0}$ 是一个概率测度。

3.1.2. 障碍证书 (Barrier Certificates, BCs)

障碍证书 (Barrier Certificates, BCs) 是用于形式化验证系统安全性的强大工具。本文主要关注离散时间 BCs。 定义 1 (离散时间障碍证书)：给定一个 DNN 控制系统 $M = (S, S_0, A, f, \pi, R)$ 和一个不安全集合 $S_u \subseteq S$ (满足 $S_u \cap S_0 = \emptyset$)。一个离散时间障碍证书是一个实值函数 $B: S \to \mathbb{R}$，使得对于某个常数 $\lambda \in (0, 1]$，满足以下条件：

1. $B(s) \leq 0 \quad \text{for all } s \in S_0$

2. $B(s) > 0 \quad \text{for all } s \in S_u$

3. $B(f(s, \pi(s))) - B(s) + \lambda \cdot B(s) \leq 0 \quad \text{for all } s \in S$

   直观解释 (Intuition)：

• 条件 (1) 保证初始状态 $s_0$ 在 $B(s) \leq 0$ 的区域内。
• 条件 (2) 保证不安全状态 $s_u$ 在 $B(s) > 0$ 的区域内。
• 条件 (3) 表明 B(s) 的值在系统演化时（从 $s$ 到 $f(s, \pi(s))$）不会从 $\leq 0$ 区域“跳”到 $> 0$ 区域，即如果 $B(s) \leq 0$，那么 $B(f(s, \pi(s))) \leq (1-\lambda)B(s) \leq 0$。 如果存在这样的 BC，则系统是安全的，即系统从初始集合 $S_0$ 永远不会到达不安全集合 $S_u$。

3.1.3. 神经障碍证书 (Neural Barrier Certificates, NBCs)

由于传统 BCs 的表达能力受限于预设模板（如多项式），并且寻找它们可能很困难，最近的工作提出使用神经网络来实现 BCs，称为 神经障碍证书 (Neural Barrier Certificates, NBCs)。NBCs 能够利用神经网络强大的表达能力来学习复杂的障碍函数。

• 训练 (Training)： 学习器训练一个神经网络，使其在有限的样本集上拟合 BC 的条件。
• 验证 (Validation)： 训练完成后，通过验证器（如使用 SMT 求解器或和平方规划等方法）检查 NBC 是否满足 BC 的形式化条件。
• CEGIS 范式 (CEGIS Paradigm)： 训练和验证过程通常采用 反例引导归纳综合 (CounterExample-Guided Inductive Synthesis, CEGIS) 迭代进行。如果验证失败，会生成反例用于下一轮的再训练，直到找到有效的 NBC 或达到超时。

3.1.4. 定性验证 (Qualitative Verification) 与 定量验证 (Quantitative Verification)

• 定性验证 (Qualitative Verification)：关注系统是否“几乎肯定”或“可能”满足某个性质，而不关心具体的概率数值。例如，几乎肯定安全 (almost-sure safety)（系统以概率 1 永远不会进入不安全区域）。
• 定量验证 (Quantitative Verification)：关注系统满足某个性质的概率数值，通常以给出概率的下界和上界形式。例如，概率安全 (probabilistic safety)（系统在特定时间范围内不进入不安全区域的概率）。

3.1.5. $k$-归纳 (k-Induction)

$k$-归纳 (k-induction) 是形式化验证领域的一种归纳证明技术，用于证明系统在所有时间步长上的不变性 (invariants)。它通过检查一个性质在初始 $k$ 步内成立，并且如果在任意连续 $k$ 步内成立，则在第 $k+1$ 步也成立，从而证明该性质在所有时间步都成立。本文引入了 $k$-归纳变体的 NBCs，旨在放松原始 BC 条件的严格性，使得 NBC 更容易被合成，同时仍能提供安全保证。

3.1.6. 超鞅 (Supermartingale) 与 次鞅 (Submartingale)

这些是随机过程中的概念，对于理解概率安全界限的推导至关重要：

• 超鞅 (Supermartingale)：一个随机过程 $\{X_t\}_{t \in \mathbb{N}_0}$ 如果满足 $\mathbb{E}[X_{t+1} | X_t, X_{t-1}, \dots, X_0] \leq X_t$，则称其为超鞅。直观地，其未来期望值不大于当前值，表现出“下降”或“非增”趋势。在本文中，用于推导概率安全下界。
• 次鞅 (Submartingale)：一个随机过程 $\{X_t\}_{t \in \mathbb{N}_0}$ 如果满足 $\mathbb{E}[X_{t+1} | X_t, X_{t-1}, \dots, X_0] \geq X_t$，则称其为次鞅。直观地，其未来期望值不小于当前值，表现出“上升”或“非减”趋势。在本文中，用于推导概率安全上界。
• $c$-鞅 (c-Martingale)：是超鞅和次鞅的推广，其期望值可以增加或减少一个常数 $c$，即 $\mathbb{E}[X_{t+1} | \dots] \leq X_t + c$ 或 $\mathbb{E}[X_{t+1} | \dots] \geq X_t + c$。

3.2. 前人工作

• 随机系统障碍证书： Prajna 等人 [40, 41, 42] 最早提出了在随机系统中使用障碍证书进行安全验证。这一思想通过数据驱动方法 [44] 和 $k$-归纳变体 [4] 得到了进一步扩展。
• 可达性概率： 作为计算安全概率的对偶问题，随机动力系统中的可达性概率已在无限 [20, 61, 62] 和有限时间范围 [60, 59] 内进行了研究。
• 概率程序分析： 概率程序的可达性和终止概率已通过证明规则 [19] 和基于鞅的方法 [14, 15, 5] 进行研究，后者随后通过序理论不动点方法 [52, 49, 50] 得到统一。
• DNN 控制系统形式化验证：
  • 基于 MDP 的定量验证： 将 DNN 控制系统建模为马尔可夫决策过程 (Markov Decision Processes, MDPs)，并使用 Prism [30] 和 Storm [25] 等概率模型检测器进行验证。Bacci 和 Parker [8, 7] 使用抽象解释构建区间 MDPs 以获取有界时间内的安全概率。Carr 等人 [13] 提出通过将分析限制在部分可观察的有限状态模型上来进行概率验证。
  • 可达性分析 (Qualitative)： DNN 控制系统安全验证中的一个关键定性方法。Bacci 等人 [6] 引入了一种基于线性过近似的方法，用于计算 DNN 控制系统在无限时间范围内的可达集不变式。Verisig [28] 和 Polar [27] 等其他可达性分析方法仅关注有界时间。这些方法通常不考虑扰动，假设状态动作是确定性的。
• 基于 BC 的 DNN 控制器训练和验证： 最近，基于 BC 的方法 [1, 39] 已被用于训练和验证 DNN 控制器。核心思想是通过交互式计算相应的障碍证书来训练安全的 DNN 控制器，以确保定性安全 [63, 17]。现有的基于 BC 的 DNN 控制系统验证方法主要关注定性方面，但忽略了扰动的影响 [47, 64]。

3.3. 技术演进

该领域的技术演进可以概括为：

1. 从传统控制到深度学习控制： 早期控制系统主要依赖于经典控制理论，但随着深度学习的发展，DNNs 因其强大的学习能力和适应性被引入到控制策略中，形成了 DNN 控制系统。
2. 从确定性到随机性： 传统的控制理论和形式化验证多关注确定性系统。然而，现实世界中的传感器噪声、环境不确定性以及对抗性攻击使得 DNN 控制系统表现出随机行为。这推动了对随机系统形式化验证的需求。
3. 从定性到定量： 早期形式化验证多提供定性保证（例如“是”或“否”安全）。但对于安全关键系统，仅知道系统是“几乎肯定安全”可能不够，需要知道具体的安全概率数值及其上下界，从而促使定量验证方法的兴起。
4. 从数学模板到神经网络： 障碍证书作为一种形式化工具，其有效性早期受限于手动构造或预设数学模板（如多项式）。随着神经网络的兴起，神经障碍证书 (NBCs) 利用神经网络的强大拟合能力来自动学习和表示复杂的障碍函数，大大提高了 BCs 的表达能力和适用性。
5. 从单一性质到多维保证： 本文的工作代表了从单一的定性或定量验证，向提供多维度安全保证（定性/定量、有限/无限时间、线性/指数界限）的统一框架发展。

3.4. 差异化分析

本文的方法与相关工作的主要区别和创新点在于：

1. 统一性： 现有工作通常单独处理定性或定量安全验证，或者在处理 DNN 控制系统时忽略了随机扰动。本文首次提出了一个统一的框架，能够在一个连贯的流程中解决定性安全（几乎肯定安全）和定量安全（概率上下界）问题，并涵盖了有限和无限时间范围。
2. 处理随机性： 与许多假设确定性动作或不考虑扰动的 DNN 控制系统验证方法（如 Verisig [28], Polar [27]）不同，本文明确将状态扰动（由噪声分布 $\mu$ 建模）纳入到 BC 的条件中，使其更适用于开放和对抗性环境中的 DNN 控制系统。
3. 障碍证书的扩展：
   • 为 DNN 控制系统在存在随机扰动的情况下，推导并验证了一系列新的离散时间障碍证书条件，用于定性、无限时间定量和有限时间定量安全验证。
   • 特别是，提出了提供线性/指数形式概率界限的 BC 条件，这在现有文献中并不常见，尤其是在 DNN 控制系统背景下。
4. $k$-归纳 NBCs： 引入了 $k$-归纳 NBC 变体，这是一种重要的优化，它放松了标准 BC 的严格归纳条件，使得 NBCs 的合成更加容易和高效，同时仍能提供形式化保证。
5. 仿真引导训练： 提出了一种新颖的仿真引导损失项，将其整合到 NBC 的训练过程中，以提高所计算安全界限的紧密度，这是对传统 NBC 训练方法的改进。
6. 实用工具与广泛验证： 通过开发 UniQQ 工具并在多个经典 DNN 控制系统上进行实验，验证了理论和方法的有效性，展示了其在实际应用中的潜力。

4. 方法论

本文提出了一种统一的框架，旨在解决 DNN 控制系统的定性与定量安全验证问题。其核心思想是将所有验证任务转化为合成特定神经障碍证书 (NBCs) 的问题。本节将详细阐述这一框架的原理、核心方法及其构成。

4.1. 方法原理

该方法的核心直觉是将不同类型的安全验证问题（几乎肯定安全、无限时间概率安全、有限时间概率安全）都归结为寻找一个满足特定数学条件的函数——障碍证书 (BC)。当这个 BC 以神经网络的形式实现时，即成为神经障碍证书 (NBC)。神经网络的强大表达能力使其能够学习复杂的非线性函数，从而适应 DNN 控制系统的复杂动力学。

框架工作流程如下：

1. 问题转化： 将定性安全验证问题 (QV)、无限时间概率安全定量验证问题 (QVITH) 和有限时间概率安全定量验证问题 (QVFTH) 分别转化为合成满足相应理论条件（如定理1-7）的 NBCs。
2. 迭代合成： 采用反例引导归纳综合 (CEGIS) 范式来迭代地训练和验证 NBCs。
3. 条件放松： 为了缓解 NBC 合成的难度和提高效率，引入了 $k$-归纳变体 (Theorem 8-10)，放宽了对 BC 的归纳条件。
4. 紧密度优化： 为了使定量验证得到的概率界限更精确，设计了仿真引导 (simulation-guided) 训练方法，将模拟结果的统计信息融入到 NBC 的损失函数中。
5. 统一流程： 整个框架遵循一个统一的流程：首先尝试定性验证；如果失败或不满足要求，则转向无限时间定量验证；如果仍不满足，则进行有限时间定量验证。

4.2. 核心方法详解

4.2.1. 问题定义

本文首先明确了 DNN 控制系统的三种安全验证问题：

定义 2 (Almost-Sure Safety, 几乎肯定安全)： 系统 $M_\mu$ 是几乎肯定安全 (almost-surely safe) 的，如果从任何初始状态 $s_0 \in S_0$ 开始，几乎肯定 (a.s.) 没有轨迹会进入不安全集合 $S_u$。形式化表示为： $$\forall s_0 \in S_0. \omega \in \Omega_{s_0} \implies \omega_t \notin S_u \forall t \in \mathbb{N}.$$ 符号解释：

• $s_0$: 任意初始状态。
• $\Omega_{s_0}$: 从 $s_0$ 开始的所有轨迹的集合。
• $\omega \in \Omega_{s_0}$: 从 $s_0$ 开始的一条轨迹。
• $\omega_t$: 轨迹 $\omega$ 在时间步 $t$ 时的状态。
• $S_u$: 不安全状态集合。
• $\forall t \in \mathbb{N}$: 对于所有时间步 $t$。 这是一种定性性质，因状态扰动引入的随机性而被称作“几乎肯定”。

定义 3 (Probabilistic Safety over Infinite Time Horizons, 无限时间范围概率安全)： 系统 $M_\mu$ 在无限时间范围上是概率安全 (probabilistically safe) 的，其概率范围为 $[l_{\mathrm{inf}}, u_{\mathrm{inf}}]$ (其中 $0 \leq l_{\mathrm{inf}} \leq u_{\mathrm{inf}} \leq 1$)，如果从任何初始状态 $s_0 \in S_0$ 开始，不进入 $S_u$ 的概率落入 $[l_{\mathrm{inf}}, u_{\mathrm{inf}}]$ 范围内。形式化表示为： $$\forall s_0 \in S_0. \mathbb{P}_{s_0}\left[\left\{\omega \in \Omega_{s_0} \mid \omega_t \notin S_u \text{ for all } t \in \mathbb{N}\right\}\right] \in \left[l_{\operatorname{inf}}, u_{\operatorname{inf}}\right].$$ 符号解释：

• $\mathbb{P}_{s_0}[\dots]$: 从 $s_0$ 开始的概率测度。
• $l_{\mathrm{inf}}$: 无限时间范围概率安全的下界。
• $u_{\mathrm{inf}}$: 无限时间范围概率安全的上界。 这是一种定量性质。如果 $l_{\mathrm{inf}} = u_{\mathrm{inf}} = 1$，则意味着几乎肯定安全。

定义 4 (Probabilistic Safety over Finite Time Horizons, 有限时间范围概率安全)： 系统 $M_\mu$ 在有限时间范围 $T \in [0, \infty)$ 上是概率安全 (probabilistically safe) 的，其概率范围为 $[l_{\mathrm{fin}}, u_{\mathrm{fin}}]$ (其中 $0 \leq l_{\mathrm{fin}} \leq u_{\mathrm{fin}} \leq 1$)，如果从任何初始状态 $s_0 \in S_0$ 开始，在 $T$ 时间内不进入 $S_u$ 的概率落入 $[l_{\mathrm{fin}}, u_{\mathrm{fin}}]$ 范围内。形式化表示为： $$\forall s_0 \in S_0. \mathbb{P}_{s_0}\left[\left\{\omega \in \Omega_{s_0} \mid \omega_t \notin S_u \text{ for all } t \leq T\right\}\right] \in \left[l_{\mathrm{fin}}, u_{\mathrm{fin}}\right].$$ 符号解释：

• $T$: 有限时间范围。
• $l_{\mathrm{fin}}$: 有限时间范围概率安全的下界。
• $u_{\mathrm{fin}}$: 有限时间范围概率安全的上界。 当无限时间范围的下界 $l_{\mathrm{inf}} = 0$ 时，有限时间范围的概率安全变得尤为重要。

4.2.2. 框架概览

本文提出的统一验证框架流程如图 1 所示。

该图像是示意图，展示了统一的DNN控制系统安全性验证框架。框架分为定性和定量验证两个主要部分，定性验证首先尝试通过合成神经障碍证书（NBC）来获得几乎安全的保证；如果失败，则进入定量验证阶段，进一步通过合成NBC来计算无穷和有限时间的安全性上下界。图中还包含针对 $k$-归纳NBC和指数界限的说明，展示了不同条件下的验证流程。 图 1. 统一验证框架的流程图。

框架包含三个主要步骤：

1. 步骤 1: 定性验证 (QV)：
   • 尝试合成一个满足 定理 1 条件的 NBC。
   • 如果成功，则根据定理 1 结论系统几乎肯定安全，验证结束。
   • 如果失败，可以尝试合成满足 定理 8 (其条件比定理 1 更弱) 的 $k$-归纳 NBC。
   • 如果合成再次失败，则进入定量验证阶段。
2. 步骤 2: 无限时间范围定量验证 (QVITH)：
   • 尝试合成满足 定理 2 和 定理 3 条件的两个 NBC，分别用于计算无限时间范围概率安全的下界 $l_{\mathrm{inf}}$ 和上界 $u_{\mathrm{inf}}$。
   • 如果合成失败，则报告超时并终止。
   • 如果成功，可以获得 $l_{\mathrm{inf}}$ 和 $u_{\mathrm{inf}}$。
   • 同样，可以尝试合成满足 定理 9 和 定理 10 的 $k$-归纳 NBC 变体。
   • 如果 $l_{\mathrm{inf}}$ 不小于预设安全阈值 $\delta \in (0, 1)$，则终止验证。否则（当 $l_{\mathrm{inf}}$ 太低，例如接近 0 时），继续进行有限时间范围定量验证。
3. 步骤 3: 有限时间范围定量验证 (QVFTH)：
   • 尝试合成满足 定理 4 和 定理 6 条件的两个 NBC，用于计算有限时间范围概率安全的线性下界和上界。
   • 如果合成失败，则报告超时并终止。
   • 如果成功，则获得线性界限。
   • 或者，可以尝试合成满足 定理 5 和 定理 7 条件的两个 NBC，以获得可能更紧密的指数界限。

4.2.3. 定性与定量安全验证理论

4.2.3.1. 定性安全验证

定理 1 (Almost-Sure Safety, 几乎肯定安全)： 给定一个 $M_\mu$ 系统，其初始集为 $S_0$，不安全集为 $S_u$。如果存在一个障碍证书 $B: S \to \mathbb{R}$，使得对于某个常数 $\lambda \in (0, 1]$，以下条件成立：

1. $B(s) \leq 0 \quad \text{for all } s \in S_0$
2. $B(s) > 0 \quad \text{for all } s \in S_u$
3. $B(f(s, \pi(s+\delta))) - B(s) + \lambda \cdot B(s) \leq 0 \quad \text{for all } (s, \delta) \in S \times W$ 那么系统 $M_\mu$ 是几乎肯定安全的，即 $\forall s_0 \in S_0. \omega \in \Omega_{s_0} \implies \omega_t \notin S_u \forall t \in \mathbb{N}.$

符号解释：

• B(s): 障碍证书函数，将状态 $s$ 映射到实数。

• $\lambda$: 一个正的常数，用于定义 BC 的衰减率。

• $s$: 系统状态。

• $S_0$: 初始状态集。

• $S_u$: 不安全状态集。

• $f(s, \pi(s+\delta))$: 从状态 $s$ 经过被扰动策略 $\pi(s+\delta)$ 作用后的下一状态。

• $\delta$: 噪声，来源于噪声分布 $\mu$ 的支持集 $W$。

• $\forall (s, \delta) \in S \times W$: 对于所有状态 $s$ 和所有可能的噪声 $\delta$。

  直观解释 (Intuition)： 定理 1 中的 BC 与定义 1 中的 BC 类似，但条件 (3) 考虑了系统所有的随机行为，即在计算下一状态的 $B$ 值时，考虑了状态 $s$ 受到噪声 $\delta$ 扰动后的策略 $\pi(s+\delta)$ 所采取的动作。这确保了即使在存在随机扰动的情况下，如果初始状态的 $B$ 值非正，且不安全状态的 $B$ 值严格为正，那么在任何一步，系统都不会从安全区域（$B \le 0$）进入不安全区域（$B > 0$）。

4.2.3.2. 无限时间范围定量安全验证

定理 2 (Lower Bounds on Infinite-time Safety, 无限时间安全下界)： 给定一个 $M_\mu$ 系统，其初始集为 $S_0$，不安全集为 $S_u$。如果存在一个障碍证书 $B: S \to \mathbb{R}$，使得对于某个常数 $\epsilon \in [0, 1]$，以下条件成立：

1. $B(s) \geq 0 \quad \text{for all } s \in S$
2. $B(s) \leq \epsilon \quad \text{for all } s \in S_0$
3. $B(s) \geq 1 \quad \text{for all } s \in S_u$
4. $\mathbb{E}_{\delta \sim \mu}[B(f(s, \pi(s+\delta))) \mid s] - B(s) \leq 0 \quad \text{for all } s \in S \setminus S_u$ 那么，从 $s_0 \in S_0$ 开始，无限时间范围内的安全概率被以下公式从下方限制： $$\forall s_0 \in S_0. \mathbb{P}_{s_0}\left[\left\{\omega \in \Omega_{s_0} \bigm\vert \omega_t \notin S_u \text{ for all } t \in \mathbb{N}\right\}\right] \geq 1 - B(s_0).$$ 符号解释：

• $\epsilon$: 一个常数，用于限制初始状态的 BC 值。

• $\mathbb{E}_{\delta \sim \mu}[\dots \mid s]$: 在给定当前状态 $s$ 的条件下，对噪声 $\delta$ 采样的期望值。

• $S \setminus S_u$: 除了不安全状态集 $S_u$ 之外的所有状态。

  直观解释 (Intuition)： 满足定理 2 条件的 BC 是一个非负实值函数，并且具有超鞅 (supermartingale) 性质：条件 (10) 表明，对于不在不安全区域内的任何状态 $s$，期望的 $B$ 值在下一个时间步不会增加（即 $\mathbb{E}[B(s_{t+1}) \mid s_t] \leq B(s_t)$）。条件 (7) 和 (9) 定义了 $B$ 的界限，使其在安全区外（即 $S_u$）至少为 1。结合 Ville's Inequality，可以推导出 $1 - B(s_0)$ 作为安全概率的下界。

定理 3 (Upper Bounds on Infinite-time Safety, 无限时间安全上界)： 给定一个 $M_\mu$ 系统，其初始集为 $S_0$，不安全集为 $S_u$。如果存在一个障碍证书 $B: S \to \mathbb{R}$，使得对于某些常数 $\gamma \in (0, 1)$, $0 \leq \epsilon' < \epsilon \leq 1$，以下条件成立：

1. $0 \leq B(s) \leq 1 \quad \text{for all } s \in S$
2. $B(s) \geq \epsilon \quad \text{for all } s \in S_0$
3. $B(s) \leq \epsilon' \quad \text{for all } s \in S_u$
4. $B(s) - \gamma \cdot \mathbb{E}_{\delta \sim \mu}[B(f(s, \pi(s+\delta))) \mid s] \leq 0 \quad \text{for all } s \in S \setminus S_u$ 那么，从 $s_0 \in S_0$ 开始，无限时间范围内的安全概率被以下公式从上方限制： $$\forall s_0 \in S_0. \mathbb{P}_{s_0}\left[\left\{\omega \in \Omega_{s_0} \mid \omega_t \notin S_u \text{ for all } t \in \mathbb{N}\right\}\right] \leq 1 - B(s_0).$$ 符号解释：

• $\gamma$: 一个位于 $(0,1)$ 区间的常数，用于缩放期望值。

• $\epsilon', \epsilon$: 常数，用于定义 $B$ 在 $S_0$ 和 $S_u$ 上的界限。

  直观解释 (Intuition)： 满足定理 3 条件的 BC 是一个有界非负函数，并且具有 $\gamma$-缩放的次鞅 (submartingale) 性质 [52]：条件 (15) 表明，对于不在不安全区域内的状态 $s$，期望的 $B$ 值在下一个时间步以 $\gamma$ 比例缩放后会增加（即 $\mathbb{E}[B(s_{t+1}) \mid s_t] \geq B(s_t)/\gamma$）。结合 Optional Stopping Theorem，可以推导出 $1 - B(s_0)$ 作为安全概率的上界。

4.2.3.3. 有限时间范围定量安全验证

当无限时间范围的安全概率下界趋近于零时，分析有限时间范围内的概率变化变得有意义。

定理 4 (Linear Lower Bounds on Finite-time Safety, 有限时间线性安全下界)： 给定一个 $M_\mu$ 系统，其初始集为 $S_0$，不安全集为 $S_u$。如果存在一个障碍证书 $B: S \to \mathbb{R}$，使得对于某些常数 $\lambda > \epsilon \geq 0$ 和 $c \geq 0$，以下条件成立：

1. $B(s) \geq 0 \quad \text{for all } s \in S$
2. $B(s) \leq \epsilon \quad \text{for all } s \in S_0$
3. $B(s) \geq \lambda \quad \text{for all } s \in S_u$
4. $\mathbb{E}_{\delta \sim \mu}[B(f(s, \pi(s+\delta))) \mid s] - B(s) \leq c \quad \text{for all } s \in S \setminus S_u$ 那么，从 $s_0 \in S_0$ 开始，有限时间范围 $T$ 内的安全概率被以下公式从下方限制： $$\forall s_0 \in S_0. \mathbb{P}_{s_0}\left[\left\{\omega \in \Omega_{s_0} \middle\vert \omega_t \notin S_u \text{ for all } t \leq T\right\}\right] \geq 1 - (B(s_0) + cT) / \lambda.$$ 符号解释：

• $\lambda, \epsilon$: 常数，定义 $B$ 在 $S_0$ 和 $S_u$ 上的界限。

• $c$: 非负常数，限制 $B$ 期望值的增长。

  直观解释 (Intuition)： 定理 4 中的 BC 满足 $c$-鞅 (c-martingale) 性质 [48]。条件 (20) 意味着 $B$ 的期望值在每个时间步可以最多增加 $c$。这比超鞅性质（$c=0$）更宽松，但代价是只能提供有限时间范围内的安全保证。推导基于 Ville's Inequality。

定理 5 (Exponential Lower Bounds on Finite-time Safety, 有限时间指数安全下界)： 给定一个 $M_\mu$ 系统。如果存在一个函数 $B: S \to \mathbb{R}$，使得对于某些常数 $\alpha > 0$, $\beta \in \mathbb{R}$ 和 $\gamma \in [0, 1)$，以下条件成立：

1. $B(s) \geq 0 \quad \text{for all } s \in S$
2. $B(s) \leq \gamma \quad \text{for all } s \in S_0$
3. $B(s) \geq 1 \quad \text{for all } s \in S_u$
4. $\alpha \mathbb{E}_{\delta \sim \mu}[B(f(s, \pi(s+\delta))) \mid s] - B(s) \leq \alpha\beta \quad \text{for all } s \in S \setminus S_u$ 那么，从 $s_0 \in S_0$ 开始，有限时间范围 $T$ 内的安全概率被以下公式从下方限制： $$\forall s_0 \in S_0. \mathbb{P}_{s_0}\left[\left\{\omega \in \Omega_{s_0} \mid \omega_t \notin S_u \text{ for all } t \leq T\right\}\right] \geq 1 - \frac{\alpha\beta}{\alpha - 1} + \left(\frac{\alpha\beta}{\alpha - 1} - B(s_0)\right) \cdot \alpha^{-T}.$$ 符号解释：

• $\alpha$: 正常数，用于缩放期望值。

• $\beta$: 实数常数，用于限制缩放后的期望值增长。

• $\gamma$: 位于 [0,1) 区间的常数，限制初始状态的 $B$ 值。

  直观解释 (Intuition)： 定理 5 中的 BC 满足条件 (24)，即其 $\alpha$-缩放的期望值在每个时间步最多可以增加 $\alpha\beta$。这一定理是基于离散版本 Gronwall's Inequality 推导的新结果，灵感来源于连续时间动力系统的工作 [59]。

定理 6 (Linear Upper Bounds on Finite-time Safety, 有限时间线性安全上界)： 给定一个 $M_\mu$ 系统，其初始集为 $S_0$，不安全集为 $S_u$。如果存在一个障碍函数 $B: S \to \mathbb{R}$，使得对于某些常数 $\beta \in (0, 1)$, $\beta < \alpha < 1+\beta$, $c \geq 0$，以下条件成立：

1. $B(s) \geq 0 \quad \text{for all } s \in S$
2. $B(s) \leq \beta \quad \text{for all } s \in S \setminus S_u$
3. $\alpha \leq B(s) \leq 1 + \beta \quad \text{for all } s \in S_u$
4. $\mathbb{E}_{\delta \sim \mu}[B(f(s, \pi(s+\delta))) \mid s] - B(s) \geq c \quad \text{for all } s \in S \setminus S_u$ 那么，从 $s_0 \in S_0$ 开始，有限时间范围 $T$ 内的安全概率被以下公式从上方限制： $$\forall s_0 \in S_0. \mathbb{P}_{s_0}\left[\left\{\omega \in \Omega_{s_0} \mid \omega_t \notin S_u \text{ for all } t \leq T\right\}\right] \leq 1 - B(s_0) - \frac{1}{2}c \cdot T + \beta.$$ 符号解释：

• $\beta, \alpha$: 位于 $(0,1)$ 和 $(\beta, 1+\beta)$ 区间的常数，用于定义 $B$ 的界限。

• $c$: 非负常数。

  直观解释 (Intuition)： 定理 6 中的 BC 是非负的，并且当状态在 $S_u$ 中时，其值有界。条件 (28) 是定理 4 中 $c$-鞅性质的逆，它要求 $B$ 的期望值在每个时间步至少增加 $c$。

定理 7 (Exponential Upper Bounds on Finite-Time Safety, 有限时间指数安全上界)： 给定一个 $M_\mu$ 系统，其初始集为 $S_0$，不安全集为 $S_u$。如果存在一个障碍函数 $B: S \to \mathbb{R}$，使得对于某些常数 $K' \le K < 0$, $\epsilon > 0$ 和一个非空区间 [a, b]，以下条件成立：

1. $B(s) \geq 0 \quad \text{for all } s \in S \setminus S_u$
2. $K' \leq B(s) \leq K \quad \text{for all } s \in S_u$
3. $\mathbb{E}_{\delta \sim \mu}[B(f(s, \pi(s+\delta))) \mid s] - B(s) \leq -\epsilon \quad \text{for all } s \in S \setminus S_u$
4. $a \leq B(f(s, \pi(s+\delta))) - B(s) \leq b \quad \text{for all } s \in S \setminus S_u \text{ and } \delta \in W$ 那么，从 $s_0 \in S_0$ 开始，有限时间范围 $T$ 内的安全概率被以下公式从上方限制： $$\forall s_0 \in S_0. \mathbb{P}_{s_0}\left[\left\{\omega \in \Omega_{s_0} \mid \omega_t \notin S_u \text{ for all } t \leq T\right\}\right] \leq \exp\left(-\frac{2(\epsilon \cdot T - B(s_0))^2}{T \cdot (b - a)^2}\right).$$ 符号解释：

• K', K: 常数，定义 $B$ 在 $S_u$ 上的界限。

• $\epsilon$: 正常数，表示 $B$ 期望值的最小下降量。

• [a, b]: 一个非空区间，定义 $B$ 更新的上下界。

  直观解释 (Intuition)： 定理 7 中的 BC 是一个差分有界排序超鞅 (difference-bounded ranking supermartingale) [15]。条件 (31) 是超鞅差分条件，要求 $B$ 的期望值在每个时间步至少减少 $\epsilon$。条件 (32) 则表明 $B$ 的更新量是受限的。该定理的证明使用了 Hoeffding's Inequality on Supermartingales [26]。

4.2.4. 宽松的 $k$-归纳障碍证书 (Relaxed $k$-Inductive Barrier Certificates)

为了放松 BCs 的严格条件并加速合成，本文引入了 $k$-归纳变体。 首先定义 $k$-归纳更新函数： 对于系统 $M_\mu = (S, S_0, A, \pi, f, R, \mu)$，定义其 $k$-归纳更新函数 $g_{\pi,f}^k$ 为： $$g_{\pi,f}^k(s_t, \Delta_t^k) = \left\{ \begin{array}{ll} g_{\pi,f}(g_{\pi,f}^{k-1}(s_t, \Delta_t^{k-1}), \delta_{t+k-1}) & \mathrm{~if~} k > 1 \\ f(s_t, \pi(s_t + \delta_t)) & \mathrm{~if~} k = 1 \\ s_t & \mathrm{~if~} k = 0 \end{array} \right.$$ 其中，$\Delta_t^k = [\delta_t, \delta_{t+1}, \dots, \delta_{t+k-1}]$ 是长度为 $k$ 的噪声向量，每个 $\delta_t \sim \mu$，且 $g_{\pi,f}(s_t, \delta_t) := f(s_t, \pi(s_t + \delta_t))$。 直观解释： $g_{\pi,f}^k$ 表示给定一个 $k$ 维噪声向量 $\Delta^k \in W^k$ ($W = \mathsf{supp}(\mu)$ 是 $\mu$ 的支持集)，系统在 $k$ 个时间步后的状态。

4.2.4.1. $k$-归纳定性安全障碍证书

定理 8 ($k$-inductive Variant of Almost-Sure Safety, 几乎肯定安全的 $k$-归纳变体)： 给定一个 $M_\mu$ 系统，其初始集为 $S_0$，不安全集为 $S_u$。如果存在一个 $k$-归纳障碍证书 $B: S \to \mathbb{R}$，使得以下条件成立：

1. $\bigwedge_{0 \leq i < k} B(g_{\pi,f}^i(s, \Delta^i)) \leq 0 \quad \forall (s, \Delta^i) \in S_0 \times W^i$
2. $B(s) > 0 \quad \forall s \in S_u$
3. $\bigwedge_{0 \leq i < k} (B(g_{\pi,f}^i(s, \Delta^i)) \leq 0) \implies B(g_{\pi,f}^k(s, \Delta^k)) \leq 0 \quad \forall (s, \Delta^i) \in S \times W^i$ 那么系统 $M_\mu$ 是几乎肯定安全的。

符号解释：

• $\bigwedge$: 逻辑“与”操作。

• $g_{\pi,f}^i(s, \Delta^i)$: 从状态 $s$ 经过 $i$ 步后的状态，其中 $\Delta^i$ 是 $i$ 步的噪声序列。

  直观解释 (Intuition)：

• 条件 (33) 意味着从安全初始集开始的状态序列，在接下来的 k-1 个时间步内都将保持在安全区域（即 $B \le 0$）。

• 条件 (35) 是 $k$-归纳步。它表示如果在任意连续 $k$ 个时间步内系统是安全的（即 $B$ 值都非正），那么在第 $k+1$ 个时间步系统仍然是安全的。

• 为了便于计算 $k$-归纳 BC，条件 (35) 通常被其充分条件替换： $$-B(g_{\pi,f}^k(s, \Delta^k)) - \sum_{0 \leq i < k} \tau_i \cdot (-B(g_{\pi,f}^i(s, \Delta^i))) \geq 0, \quad \forall (s, \Delta^i) \in S \times W^i.$$ 其中 $\tau_0, \dots, \tau_{k-1} \geq 0$ 是非负常数。如果存在这样的 $\tau_i$ 满足上式，则条件 (35) 成立。

4.2.4.2. $k$-归纳定量安全障碍证书

定理 9 ($k$-inductive Lower Bounds on Infinite-time Safety, 无限时间安全 $k$-归纳下界)： 给定一个 $M_\mu$ 系统。如果存在一个 $k$-归纳障碍证书 $B: S \to \mathbb{R}$，使得对于某些常数 $k \in \mathbb{N}_{\geq 1}$, $\epsilon \in [0, 1]$ 和 $c \geq 0$，以下条件成立：

1. $B(s) \geq 0 \quad \text{for all } s \in S$
2. $B(s) \leq \epsilon \quad \text{for all } s \in S_0$
3. $B(s) \geq 1 \quad \text{for all } s \in S_u$
4. $\mathbb{E}_{\delta \sim \mu}[B(f(s, \pi(s+\delta))) \mid s] - B(s) \leq c \quad \text{for all } s \in S \setminus S_u$
5. $\mathbb{E}_{\Delta^k \sim \mu^k}[B(g_{\pi,f}^k(s, \Delta^k)) \mid s] - B(s) \leq 0 \quad \text{for all } s \in S \setminus S_u$ 那么，从 $s_0 \in S_0$ 开始，无限时间范围内的安全概率被以下公式从下方限制： $$\forall s_0 \in S_0. \mathbb{P}_{s_0}\left[\left\{\omega_0 \in \Omega_{s_0} \mid \omega_t \notin S_u \text{ for all } t \in \mathbb{N}\right\}\right] \geq 1 - k B(s_0) - \frac{k(k-1)c}{2}.$$ 符号解释：

• $\mu^k$: 在 $W^k$ 上的乘积测度，用于计算 $k$ 步噪声的期望。

  直观解释 (Intuition)： 条件 (40) 要求障碍证书是一个 $c$-鞅 (c-martingale)，即每一步的期望值可以最多增加 $c$。条件 (41) 要求每隔 $k$ 步采样的障碍证书是一个超鞅 (supermartingale)，即其期望值不会增加。这两种性质结合起来，可以导出无限时间范围的概率安全下界。

定理 10 ($k$-inductive Upper Bounds on Infinite-time Safety, 无限时间安全 $k$-归纳上界)： 给定一个 $M_\mu$ 系统。如果存在一个障碍证书 $B: S \to \mathbb{R}$，使得对于某些常数 $\gamma \in (0, 1)$, $0 \leq \epsilon' < \epsilon \leq 1$, $c \leq 0$，以下条件成立：

1. $0 \leq B(s) \leq 1 \quad \text{for all } s \in S$
2. $B(s) \geq \epsilon \quad \text{for all } s \in S_0$
3. $B(s) \leq \epsilon' \quad \text{for all } s \in S_u$
4. $\mathbb{E}_{\delta \sim \mu}[B(f(s, \pi(s+\delta))) \mid s] - B(s) \geq c \quad \text{for all } s \in S$
5. $B(s) - \gamma^k \cdot \mathbb{E}_{\Delta^k \sim \mu^k}[B(g_{\pi,f}^k(s, \Delta^k)) \mid s] \leq 0 \quad \text{for all } s \in S \setminus S_u$ 那么，从 $s_0 \in S_0$ 开始，无限时间范围内的安全概率被以下公式从上方限制： $$\forall s_0 \in S_0. \mathbb{P}_{s_0}\left[\left\{\omega \in \Omega_{s_0} \mid \omega_t \notin S_u \text{ for all } t \in \mathbb{N}\right\}\right] \leq 1 - k B(s_0) - \frac{k(k-1)c}{2}.$$ 直观解释 (Intuition)： 这个 BC 是非负且有界的。条件 (45) 是 $c$-鞅性质的逆。条件 (46) 要求每隔 $k$ 步采样的障碍证书是一个 $\gamma^k$-缩放的次鞅。这一定理的证明基于 Optional Stopping Theorem。

备注 1 (Remark 1)：为了使定理 9 和定理 10 中的概率界限非平凡 (non-trivial)，$k$ 的值应满足以下范围： $$1 \leq k \leq \frac{(c - 2B(s_0)) + \sqrt{4B(s_0)^2 + c^2 - 4c(B(s_0) - 2)}}{2c}.$$

4.2.5. 神经障碍证书 (NBCs) 的合成

本文采用 反例引导归纳综合 (CEGIS) 方法 [2] 来训练和验证目标 NBCs，如图 2 所示。

该图像是一个示意图，展示了基于 CEGIS 的神经障碍证书（NBC）合成的流程。流程开始于离散化状态空间，随后进行 NBC 的训练、验证与完善，直到满足有效性或超时条件。若验证通过，流程结束；若不通过，则进入改进阶段，直到失败或有效性确认。 图 2. 基于 CEGIS 的 NBC 合成流程。

工作流程： 在每个迭代循环中，首先训练一个作为候选 BC 的神经网络，然后将其传递给验证器。如果验证结果为假，则计算一组反例用于未来的训练。这个迭代过程重复进行，直到训练出的候选网络通过验证或者达到预设的超时时间。

4.2.5.1. 训练候选 NBCs

训练阶段的两个关键因素是训练数据的生成和损失函数的构建。

训练数据离散化 (Training Data Discretization)： 由于状态空间 $S$ 可能是连续和无限的，需要选择一个有限的状态集进行训练。这通过将状态空间 $S$ 离散化为一个有限子集 $\tilde{S} \subseteq S$ 来实现，使得对于每个 $s \in S$，都存在一个 $\tilde{s} \in \tilde{S}$ 使得 $||s - \tilde{s}||_1 < \tau$，其中 $\tau > 0$ 是粒度 (granularity)。因为 $S$ 是紧致 (compact) 的，可以通过网格化来生成 $\tilde{S}$。在验证失败后，$\tilde{S}$ 会根据反例和更小的粒度进行重构。从 $\tilde{S}$ 中，构造出用于训练的有限集 $\tilde{S}_0 := \tilde{S} \cap S_0$ 和 $\tilde{S}_u := \tilde{S} \cap S_u$。

损失函数构建 (Loss Function Construction)： 候选 NBC 被初始化为一个神经网络 $h_\theta$，其网络参数为 $\theta$。$h_\theta$ 通过最小化以下损失函数来训练： $$\mathcal{L}(\boldsymbol{\theta}) := k_1 \cdot \mathcal{L}_1(\boldsymbol{\theta}) + k_2 \cdot \mathcal{L}_2(\boldsymbol{\theta}) + k_3 \cdot \mathcal{L}_3(\boldsymbol{\theta}) + k_4 \cdot \mathcal{L}_4(\boldsymbol{\theta}) + k_5 \cdot \mathcal{L}_5(\boldsymbol{\theta})$$ 符号解释：

• $k_i$: 算法参数，用于平衡各个损失项的权重。

  以定理 2 的 NBC 合成为例，各损失项的定义如下：

• 第一个损失项 (对应条件 (7) $B(s) \geq 0$)： $$\mathcal{L}_1(\theta) = \frac{1}{|\tilde{S}|} \sum_{s \in \tilde{S}} \left( \operatorname{max}\{0 - h_\theta(s), 0\} \right)$$ 直观解释： 如果 $h_\theta(s)$ 小于 0，则产生损失，促使 $h_\theta(s)$ 保持非负。

• 第二和第三个损失项 (对应条件 (8) $B(s) \leq \epsilon$ 和 (9) $B(s) \geq 1$)： $$\mathcal{L}_2(\theta) = \frac{1}{|\tilde{S}_0|} \sum_{s \in \tilde{S}_0} \left( \operatorname{max}\{h_\theta(s) - \epsilon, 0\} \right)$$ $$\mathcal{L}_3(\theta) = \frac{1}{|\tilde{S}_u|} \sum_{s \in \tilde{S}_u} \left( \operatorname{max}\{1 - h_\theta(s), 0\} \right)$$ 直观解释： $\mathcal{L}_2$ 促使初始状态 $s \in \tilde{S}_0$ 的 $h_\theta(s)$ 不超过 $\epsilon$。$\mathcal{L}_3$ 促使不安全状态 $s \in \tilde{S}_u$ 的 $h_\theta(s)$ 不小于 1。

• 第四个损失项 (对应条件 (10) $\mathbb{E}_{\delta \sim \mu}[B(f(s, \pi(s+\delta))) \mid s] - B(s) \leq 0$)： $$\mathcal{L}_4(\theta) = \frac{1}{|\tilde{S} \setminus \tilde{S}_u|} \sum_{s \in \tilde{S} \setminus \tilde{S}_u} \left( \operatorname{max}\left\{\sum_{s' \in \mathcal{D}_s} \frac{h_\theta(s')}{N} - h_\theta(s) + \zeta, 0\right\} \right)$$ 符号解释：

  • $\tilde{S} \setminus \tilde{S}_u$: 训练集中非不安全状态的集合。
  • $\mathcal{D}_s := \{s' \mid s' = f(s, \pi(s+\delta_i)), \delta_i \sim \mu, i \in [1, N]\}$: 从状态 $s$ 采样 $N$ 个噪声 $\delta_i$ 得到的后继状态集合。
  • $\sum_{s' \in \mathcal{D}_s} \frac{h_\theta(s')}{N}$: 使用 $N$ 个后继状态的 $h_\theta(\cdot)$ 平均值来近似期望值 $\mathbb{E}_{\delta \sim \mu}[B(f(s, \pi(s+\delta)))]$。
  • $\zeta > 0$: 一个正的紧致化参数，用于使条件更严格。

• 仿真引导损失项 (Simulation-guided Loss Term)： 为了保证训练出的 NBC 提供的界限尽可能紧密，引入了这一损失项。对于每个 $s_0 \in \tilde{S}_0$，通过模拟 $N'$ 条轨迹来估算无限时间范围内的安全频率 $\mathbb{f}_s$。 $$\mathcal{L}_5(\theta) = \frac{1}{|\tilde{S}_0|} \sum_{s \in \tilde{S}_0} \left( \operatorname{max}\{\mathbb{f}_s + h_\theta(s) - 1, 0\} \right)$$ 直观解释： 定理 2 给出下界为 $1 - B(s_0)$。为了使这个下界紧密，我们希望 $1 - B(s_0)$ 尽可能接近真实的或模拟的安全频率 $\mathbb{f}_s$。因此，$\mathcal{L}_5$ 促使 $\mathbb{f}_s + h_\theta(s) - 1$ 尽可能不大于 0，即 $h_\theta(s) \leq 1 - \mathbb{f}_s$。由于 $1 - B(s_0) \leq \mathbb{f}_s$ (下界属性)，结合 $h_\theta(s)$ 近似 $B(s_0)$，这个损失项鼓励 $h_\theta(s)$ 尽可能小，从而使 $1 - h_\theta(s)$ 尽可能大且接近 $\mathbb{f}_s$。 作者强调，这种仿真引导方法结合 NBC 验证是可靠的，因为最终会通过验证步骤确保 NBC 满足所有形式化条件。

4.2.5.2. NBC 验证 (NBC Validation)

一个候选 NBC $h_\theta$ 只有在满足其对应定理的所有条件时才被认为是有效的。

• 条件 (7) 到 (9) 的验证 (以定理 2 为例)： 这三个条件可以通过以下组合约束来检查： $$\operatorname{inf}_{s \in S} h_\theta(s) \geq 0 \quad \wedge \quad \operatorname{sup}_{s \in S_0} h_\theta(s) \leq \epsilon \quad \wedge \quad \operatorname{inf}_{s \in S_u} h_\theta(s) \geq 1$$ 这可以通过区间界传播 (interval bound propagation) 方法 [21, 58] 来计算。如果任何状态违反了上述方程，它将被视为一个反例，并添加到 $\tilde{S}$ 中用于后续的训练。

• 条件 (10) 的验证 (以定理 2 为例)： 该条件是关于期望值的，且需要对无限状态空间 $S \setminus S_u$ 进行验证。定理 11 将验证从无限状态简化为有限状态。 定理 11：给定一个 $M_\mu$ 系统和一个函数 $B: S \to \mathbb{R}$。如果以下公式对于任何状态 $\tilde{s} \in \tilde{S} \setminus \tilde{S}_u$ 成立： $$\mathbb{E}_{\delta \sim \mu}[B(f(\tilde{s}, \pi(\tilde{s}+\delta))) \mid \tilde{s}] \leq B(\tilde{s}) - \zeta$$ 其中 \zeta = \tau \cdot L_B \cdot (1 + L_f \cdot (1 + L_{\pi}))，且 $L_f, L_\pi, L_B$ 分别是 $f, \pi$ 和 $B$ 的 Lipschitz 常数，那么对于任何状态 $s \in S \setminus S_u$，都有 $\mathbb{E}_{\delta \sim \mu}[B(f(s, \pi(s+\delta))) \mid s] - B(s) \leq 0$。 符号解释：

  • $\zeta$: 一个与系统和 BC 的 Lipschitz 常数以及离散化粒度相关的正值。
  • $L_B, L_f, L_\pi$: 分别是 $B$, $f$, $\pi$ 函数的 Lipschitz 常数 (Lipschitz constants)。一个函数的 Lipschitz 常数衡量了该函数在输入变化时输出变化的最大速率，即其“平滑度”或“陡峭度”。
  • $\tau$: 状态空间离散化时的粒度。

  验证期望值： 由于 $h_\theta$ 是神经网络形式，直接计算其期望值 $\mathbb{E}_{\delta \sim \mu}[h_\theta(f(\tilde{s}, \pi(\tilde{s}+\delta))) \mid \tilde{s}]$ 的封闭形式很困难。因此，本文通过区间算术 (interval arithmetic) [21, 58] 来上界 (bound from above) 这个期望值。

  • 将噪声分布 $\mu$ 及其支持集 $W$ 划分为 $m \geq 1$ 个有限单元 (cells)，即 $\mathrm{cell}(W) = \{W_1, \dots, W_m\}$。
  • 用 $\operatorname{maxvol} = \operatorname{max}_{W_i \in \mathrm{cell}(W)} \mathrm{vol}(W_i)$ 表示分区中任何单元相对于 Lebesgue 测度的最大体积。
  • 期望值被上界估计为： $$\mathbb{E}_{\delta \sim \mu}[h_\theta(f(\tilde{s}, \pi(\tilde{s}+\delta))) \mid \tilde{s}] \leq \sum_{W_i \in \mathrm{cell}(W)} \operatorname{maxvol} \cdot \operatorname{sup}_\delta F(\delta)$$ 其中 $F(\delta) = h_\theta(f(\tilde{s}, \pi(\tilde{s}+\delta)))$。这个上界可以通过区间算术来计算。

定理 12 (Soundness, 可靠性)： 如果一个训练好的 NBC 是有效的，那么它能够为定性验证认证几乎肯定安全，或者为定量验证提供经过认证的概率安全下界/上界。 直观解释： 这个定理确保了整个框架的正确性。一旦 NBC 通过了严格的形式化验证步骤，那么它所给出的安全保证（无论是定性还是定量）都是可靠的。

5. 实验设置

本文通过在四个经典的 DNN 控制系统上应用所提出的框架，评估了其有效性。

5.1. 数据集

实验使用的“数据集”是四个经典的 DNN 控制任务，它们本身是模拟环境，而不是传统意义上的静态数据集：

1. Pendulum (PD)：来自 OpenAI Gym [11]，是一个经典的控制问题，目标是使倒立摆保持直立。

2. Cartpole (CP)：同样来自 OpenAI Gym [11]，目标是使小车上的杆子保持平衡。

3. B1：一个常用的基准任务，常见于最先进的安全验证工具 [28]。

4. Tora：另一个常用的基准任务，常见于最先进的安全验证工具 [28]。

   这些任务代表了不同复杂度的控制问题，涵盖了强化学习和控制系统验证领域的典型挑战。选择这些系统是为了验证方法在不同动态特性和状态空间下的泛化能力。

5.2. 评估指标

论文的评估指标分为几个方面，以验证框架的不同组成部分：

5.2.1. 定性验证评估

• 验证结果 (Verification Result)：
  • $\checkmark$ (Verified)：表示成功训练并验证了相应的 NBC，证明系统几乎肯定安全。
  • Unknown：表示在给定超时时间内未能训练并验证出有效的 NBC。
• 失败剧集数 (#Fail.)：通过仿真记录系统进入不安全区域的剧集数量。这作为真实世界行为的参考基线，用于与形式化验证结果进行对比。

5.2.2. 定量验证评估

• 认证下界和上界 (Certified Lower and Upper Bounds)：
  • $l_{\mathrm{inf}}, u_{\mathrm{inf}}$：无限时间范围的概率安全下界和上界。
  • $l_{\mathrm{fin}}, u_{\mathrm{fin}}$：有限时间范围的概率安全下界和上界（包括线性和指数形式）。
  • 这些界限是 NBCs 根据定理 2-7 计算得出的平均值。
• 仿真结果 (Simulation Results)：作为概率安全的基线，通过大量仿真（例如 10,000 个剧集）统计得到实际安全频率。认证界限的有效性通过它们是否能“包围”仿真结果来体现。
• 紧密度 (Tightness)：衡量认证界限与仿真结果之间的接近程度。越接近，则界限越紧密。

5.2.3. 效率与改进评估

• 合成时间 (Synthesis Time)：衡量训练和验证 NBC 所需的时间（秒）。用于评估 $k$-归纳变体在减少开销方面的效果。
• 性能提升百分比 (Improvement Percentage)：
  • $k$-归纳 NBCs 相较于普通 NBCs 在合成时间上的降低。
  • 带有仿真引导损失项的 NBCs 相较于没有该项的 NBCs 在界限紧密度上的提升。

5.3. 对比基线

• 对于定性验证： 主要通过与大量仿真结果的对比来验证，即形式化验证结果 ($\checkmark$ 或 Unknown) 是否与仿真中是否存在失败剧集 (#Fail.) 相符。
• 对于定量验证：
  • 仿真结果 (Simulation Outcomes)：作为“地面真实”的近似值，用于评估认证界限的有效性和紧密度。
  • 普通 NBCs (Ordinary NBCs)：在评估 $k$-归纳 NBCs 和仿真引导训练方法的有效性时，普通的（即非 $k$-归纳且无仿真引导的）NBCs 作为对比基线。
  • 线性界限 (Linear Bounds)：在评估指数界限的紧密度时，线性界限作为对比。

5.4. 实验环境

所有实验都在以下工作站上进行：

• 操作系统 (Operating System)：Ubuntu 18.04
• CPU (Processor)：32 核 AMD Ryzen Threadripper CPU
• RAM (Memory)：128GB
• GPU (Graphics Processing Unit)：单块 24564MiB GPU

5.5. 噪声设置

为了模拟现实世界中的不确定性，实验中对 DNN 控制系统引入了状态扰动 (state perturbations)。

• 噪声类型 (Noise Type)：均匀噪声 (uniform noises)。
• 噪声特性 (Noise Characteristics)：零均值 (zero means) 和不同的半径 $r$。
• 扰动方式 (Perturbation Method)：对于每个状态 $s = (s_1, \ldots, s_n)$，向每个维度添加噪声 $X_1, \ldots, X_n$，得到扰动后的状态 $(s_1 + X_1, \ldots, s_n + X_n)$。
• 噪声分布 (Noise Distribution)：$X_i \sim \mathbf{U}(-r, r)$，其中 $1 \leq i \leq n$ 且 $r \geq 0$。

5.6. 初始状态采样

• 定性评估： 随机选择 10,000 个初始状态，而不是单个初始状态。
• 定量评估：
  • 计算这 10,000 个初始状态下，NBCs 提供的下界/上界的平均值，作为系统层面的定量安全概率。
  • 从这 10,000 个初始状态中的每一个开始，在不同扰动下模拟 10,000 个剧集，并将这些统计结果作为基线。

6. 实验结果与分析

本文的实验结果旨在评估所提出框架中三个关键方面的有效性：定性与定量验证方法、$k$-归纳障碍证书以及仿真引导训练方法。

6.1. 核心结果分析

6.1.1. 定性安全验证的有效性

以下是原文 Table 1 的结果：

分析：

• 一致性验证： 对于所有被 NBC 成功验证为“几乎肯定安全” ($\checkmark$) 的系统（例如 CP 在 $r=0$ 时），仿真结果显示 #Fail. 均为 0，即没有失败的剧集。这表明形式化验证与实际系统行为高度一致，验证了本文方法在定性验证上的有效性。
• 无法验证与仿真失败： 对于那些仿真中检测到失败剧集（#Fail. > 0）的系统，例如 CP 在 $r=0.01$ 时有 207 个失败剧集，PD 在 $r=0.01$ 时有 675 个失败剧集，相应的 NBC 无法被合成（结果为 Unknown）。这再次展示了方法的一致性：如果系统不安全，验证器就无法找到一个证明其安全的证书。
• $k$-归纳 NBC 的作用： 对于 CP 在 $r=0.01$ 时和 Tora 在 $r=0.02$ 时，尽管普通的 1-归纳 NBC 无法合成（Unknown），但通过应用 定理 8 的 2-归纳 NBC 变体，系统被成功验证 ($\checkmark$)，且仿真显示 #Fail. 为 0。这有力地证明了 $k$-归纳 NBC 通过放松条件，能够更有效地合成有效的障碍证书，从而在标准 NBC 失败的情况下提供安全保证，减少了验证开销。
• 扰动半径的影响： 随着扰动半径 $r$ 的增加，确保几乎肯定安全变得更具挑战性。例如，PD 和 Tora 在 $r$ 较小时可以被验证，但在 $r$ 增加后，验证结果变为 Unknown，这与实际系统在更大不确定性下难以保持绝对安全的直觉相符。

6.1.2. 无限时间范围定量安全验证的有效性

图 3 (a-d) 展示了在无限时间范围内的认证上下界与仿真结果的比较。

该图像是图表，展示了在不同扰动半径和时间步长下，DNN控制系统的认证上下界与模拟结果的比较，具体包括(a)至(d)中的扰动半径对概率的影响，以及(e)至(h)中时间步长对概率的影响。 图 3. 无限时间 (a-d) 和有限时间 (e-h) 范围内的认证上下界，以及它们与仿真结果的比较。

分析 (关注图 3 a-d)：

• 界限的有效性： 图中红色线（定理 2 下界）和蓝色线（定理 3 上界）代表了由普通 NBCs 计算的平均概率安全下界和上界。紫色线（定理 9 2-归纳下界）和绿色线（定理 10 2-归纳上界）代表了由 2-归纳 NBCs 计算的界限。这些认证界限始终“包围”了黑线（由仿真统计得到的安全频率）。这表明训练的 NBCs 能够可靠地提供对系统概率安全的有效界限。

• $k$-归纳 NBC 的表现： 2-归纳 NBC 提供的界限（紫色和绿色）通常比普通 NBC 提供的界限（红色和蓝色）稍微宽松。这符合预期，因为 $k$-归纳变体旨在放松条件以加速合成，可能以牺牲一部分紧密度为代价。

• 合成时间： 以下是原文 Table 2 的结果：

  Task	Lower	2-Lower	Upper	2-Upper
  CP	2318.5	1876.0	2891.9	2275.3
  PD	1941.6	1524.0	2282.7	1491.5
  Tora	280.3	218.5	895.1	650.7
  B1	587.4	313.6	1127.3	840.1

分析：

• 效率提升： Table 2 显示，2-归纳 NBCs 的合成时间普遍低于普通 NBCs。平均而言，2-归纳 NBCs 的合成时间比普通 NBCs 快了 25%。这验证了 $k$-归纳 NBCs 在降低验证开销方面的有效性。

6.1.3. 有限时间范围定量安全验证的有效性

图 3 (e-h) 展示了在有限时间范围内的认证上下界与仿真结果的比较。

分析 (关注图 3 e-h)：

• 界限的有效性： 紫色线（定理 5 指数下界）和蓝色线（定理 7 指数上界）代表了由 NBCs 计算的指数界限。红色线（定理 4 线性下界）和绿色线（定理 6 线性上界）代表了由 NBCs 计算的线性界限。这些认证界限在整个有限时间范围内都成功地“包围”了仿真结果（黑线），再次证明了方法的有效性。
• 界限的紧密度：
  • 指数上界 (蓝色) 始终比线性上界 (绿色) 更紧密。
  • 指数下界 (紫色) 随着时间的增加，变得比线性下界 (红色) 更紧密。
• 这表明，在有限时间范围的定量验证中，指数形式的界限通常能提供更精确的估计。

6.1.4. 仿真引导损失项的有效性

图 4 比较了有无仿真引导损失项训练的 NBCs 所计算的界限。

该图像是一个图表，展示了不同扰动半径 $r$ 对各种系统（CP、PD、Tora 和 B1）的概率边界的影响。各图展示了带有和不带有仿真引导损失项的上限和下限，显示了在不同情况下系统的安全性变化。 图 4. 在无限时间范围内，有无仿真引导损失项的认证界限比较。

分析：

• 紧密度显著提升： 图中红色线和蓝色线代表了使用仿真引导损失项训练的 NBCs 所计算的界限。紫色线和绿色线代表了未使用该项训练的 NBCs 所计算的界限。
• 结果显示： 没有仿真引导损失项训练的 NBCs 得到的上下界明显比使用该项训练的 NBCs 得到的界限更宽松。
• 量化改进： 具体而言，加入仿真引导损失项后，下界的紧密度平均提升了 47.5%，上界的紧密度平均提升了 31.7%。
• 结论： 这证实了仿真引导损失项在进行定量安全验证时是至关重要的，它能显著提高认证界限的精确性。

6.2. 数据呈现

原文 Table 1. 定性验证结果。 （已在 6.1.1 节展示）

原文 Table 2. 不同 NBCs 的合成时间。 （已在 6.1.2 节展示）

6.3. 消融实验/参数分析

论文中没有明确地标注为“消融实验”的章节，但对 $k$-归纳 NBCs 和仿真引导损失项的评估，本质上属于一种消融分析：

• $k$-归纳 NBCs 的评估： 比较了 1-归纳（即普通）NBC 与 2-归纳 NBC 在验证成功率（Unknown 变为 $√$）和合成时间上的差异。这表明了 $k$-归纳项对加速合成和拓宽可验证范围的贡献。

• 仿真引导损失项的评估： 比较了包含和不包含 $\mathcal{L}_5(\theta)$ 损失项的训练方法，结果量化了该项对界限紧密度的提升。这验证了仿真引导作为框架组件的有效性。

  这些分析表明，框架中的各个组件（特别是 $k$-归纳和仿真引导）都对最终的验证效果和效率有积极影响。

7. 总结与思考

7.1. 结论总结

本文提出了一种新颖且全面的框架，成功地统一了 DNN 控制系统的定性与定量安全验证问题。其核心在于将各种验证任务转化为合成神经障碍证书 (NBCs) 的问题。通过引入一系列创新的障碍证书条件，该框架能够提供：

1. 定性安全保证： 建立几乎肯定安全 (almost-sure safety)。
2. 定量安全保证： 计算无限时间范围和有限时间范围内的概率安全下界和上界，并以线性或指数形式呈现。 此外，为了提高合成效率和界限的紧密度，论文引入了 $k$-归纳 NBC 变体以放松约束，并设计了仿真引导训练方法来优化损失函数。通过原型工具 UniQQ 在四个经典 DNN 控制系统上的实验，验证了该方法的有效性，证明了其在处理带有随机扰动的 DNN 控制系统安全性验证方面的强大能力。

7.2. 局限性与未来工作

论文作者指出了自身的局限性，并提出了未来研究方向：

• NBC 质量的重要性： 实验表明，定性与定量验证结果显著依赖于训练出的 NBC 的质量。这意味着 NBC 的表达能力和拟合精度直接影响验证的可靠性和紧密度。
• 未来工作： 探索更复杂的深度学习方法来训练有效的 NBC，以期获得更精确的验证结果。这可能包括改进神经网络架构、优化训练算法或引入更先进的损失函数设计等。
• 紧密度影响因素： 进一步研究影响认证界限紧密度的因素，从而能够系统地设计出更紧密的界限。

7.3. 个人启发与批判

7.3.1. 个人启发

1. 形式化方法与深度学习的融合潜力： 本文是形式化验证与深度学习结合的典范。它利用了深度学习强大的模式识别和函数拟合能力来解决形式化验证中复杂函数构造的难题（障碍证书），同时又通过形式化验证的严格性来为深度学习模型提供可信赖的安全性保证。这种融合对于安全关键领域的 AI 应用至关重要。
2. 统一框架的价值： 将定性与定量验证、无限与有限时间范围以及线性与指数界限统一在一个框架内，极大地提高了验证方法的普适性和实用性。这种全面性使得研究人员和工程师可以根据具体需求灵活选择合适的安全保证形式。
3. $k$-归纳原理的巧妙应用： 将 $k$-归纳原理引入到障碍证书的合成中，是解决验证复杂性和效率之间矛盾的一个优雅方案。它在保留形式化保证的同时，通过放宽一步归纳的严格性，显著降低了计算成本，这对于实际应用具有重要意义。
4. 仿真引导的实用性： 在形式化验证中引入仿真引导的理念，是结合经验数据和理论严谨性的一个有效策略。虽然形式化验证旨在提供普适性保证，但仿真数据可以为神经网络的训练提供有价值的“软约束”或“目标”，从而引导模型学习到更紧密的界限，这在纯粹的理论推导难以达到最佳紧密度时显得尤为重要。

7.3.2. 潜在问题与批判

1. 计算成本与可扩展性： 尽管 $k$-归纳降低了合成时间，但 NBC 的训练和验证，特别是涉及区间算术来估计期望值和检查 Lipschitz 常数，对于高维状态空间或极其复杂的 DNN 模型，计算成本可能仍然非常高昂。如何进一步提高其在高维、大规模系统上的可扩展性是一个持续的挑战。

2. Lipschitz 常数的估计： 定理 11 中 $\zeta$ 的计算依赖于函数 $f, \pi, B$ 的 Lipschitz 常数。精确计算或紧密估计神经网络的 Lipschitz 常数本身就是一个研究难题，过高的估计可能导致 $\zeta$ 过大，从而使验证条件过于严格而难以满足，或导致结果不紧密。

3. 噪声分布的假设： 论文假设噪声分布 $\mu$ 要么有界，要么是独立单变量分布的乘积。虽然这在许多情况下是合理的，但现实世界中的噪声可能更复杂，例如具有相关性或非均匀支持集。扩展框架以处理更通用或未知的噪声模型是一个挑战。

4. 界限的真正紧密度： 尽管仿真引导损失项显著提高了界限的紧密度，但仍然存在一个理论上的差距。这些界限是“认证的”，但并不一定是“最紧密的”或“精确的”概率值。对于某些应用场景，这种差距可能仍然不够理想。

5. DNN 模型的黑箱性质： 障碍证书是 DNN 的一个外部属性，而不是 DNN 本身。这意味着如果 DNN 控制策略发生微小变化，可能需要重新合成 NBC。未来工作可以探索如何设计“内在安全”的 DNNs，或者如何使 NBCs 对 DNN 策略的变化更具鲁棒性。

6. 反例引导归纳综合 (CEGIS) 的效率： CEGIS 循环依赖于有效的反例生成和再训练。如果反例难以生成或再训练过程收敛缓慢，整个合成过程可能依然非常耗时。

   总的来说，本文为 DNN 控制系统的安全验证提供了一个强大且富有前景的统一框架，展示了形式化方法与深度学习融合的巨大潜力。但正如所有前沿研究一样，其在可扩展性、精确性与计算效率之间仍有权衡，需要未来的研究进一步探索和优化。