通过指数倾斜的扩散引导搜索（DiffTilt）：在安全关键系统反证中的应用

# 通过指数倾斜的扩散引导搜索（DiffTilt）：在安全关键系统反例生成中的应用  
**来源：** https://arxiv.org/html/2607.23134  
**Tanmay Khandait, Preetom Biswas, Hideki Okamoto, Bardh Hoxha, Georgios Fainekos, and Giulia Pedrielli**

T. Khandait, P. Biswas, and G. Pedrielli 隶属于亚利桑那州立大学计算与增强智能学院，地址：美国亚利桑那州坦佩（电子邮箱：[email protected], [email protected], [email protected]）。  
H. Okamoto, B. Hoxha, and G. Fainekos 隶属于丰田北美研发中心，地址：美国密歇根州安娜堡 48105（电子邮箱：[email protected], [email protected], [email protected]）。

###### 摘要  
在自主系统和信息物理系统中发现罕见的安全关键失效是验证与确认领域的基本挑战。现有的反例生成方法依赖于条件采样策略，这种策略将环境与系统执行轨迹的联合分布进行因子分解，因此会受到**乘性稀有效应**的影响：失效诱导输入和失效诱导轨迹的同时稀缺性使得穷举搜索成本过高。本文提出了**DiffTilt**，一个分布框架，通过**指数倾斜**扩散模型诱导的环境与执行轨迹联合分布来解决这一挑战。我们证明，这种扩散引导采样在联合空间中可以精确地解释为重要性采样，其中引导分数实现了概率质量向失效相关行为的KL最优重新分配。此外，我们证明倾斜可证明地放大了失效概率，并且严格优于受限于乘性稀有效应的条件采样策略。在该框架中，联合生成模型充当场景的可复用先验，无需忠实表示被测系统。相反，通过昂贵的仿真进行的真实系统评估仅限于学习一个评分函数，该函数负责表征所生成场景的质量，从而实现对昂贵仿真的选择性和自适应使用。此外，虽然我们专注于反例生成，但该框架具有通用性，适用于其他场景生成问题，如规划、综合。在这项工作中，我们研究了DiffTilt在ARCH-COMP基准测试上的性能，并提出了一个额外的牵引-拖车基准测试用于反例生成，以展示当场景生成由良好定义的规范（而非奖励）引导时，几种方法的行为。在所有案例中，与最先进的方法相比，所提出的方法实现了具有竞争力或更优的反例生成性能，当规范定义不限于STL公式时，性能提升更为显著。

## I. 引言与相关工作  
在复杂的信息物理系统和自主系统中发现罕见但安全关键的失效仍然是基本挑战，其原因在于高维度、结构化约束以及环境与系统执行轨迹之间的强依赖性。现有的场景测试和反例生成方法通常依赖于条件采样策略或对输入的启发式搜索，这些方法隐式地将环境与轨迹的联合分布进行因子分解，因此受到乘性稀有效应的影响\[8 (https://arxiv.org/html/2607.23134#bib.bib9),15 (https://arxiv.org/html/2607.23134#bib.bib10),9 (https://arxiv.org/html/2607.23134#bib.bib11)\]。从概率角度来看，这些方法是在稀有事件的密度处采样，而非主动重塑该密度，导致即使条件生成模型准确，样本复杂度也高得惊人。重要性采样通过将概率质量重新加权至关键区域，为罕见事件估计提供了一个原则性框架，其中指数倾斜作为KL最优机制，用于强制执行矩约束和方差缩减\[4 (https://arxiv.org/html/2607.23134#bib.bib13),3 (https://arxiv.org/html/2607.23134#bib.bib14),2 (https://arxiv.org/html/2607.23134#bib.bib12)\]。这些思想与大偏差理论和吉布斯测度紧密相关，其中指数重加权将质量集中在极端事件上\[7 (https://arxiv.org/html/2607.23134#bib.bib15),5 (https://arxiv.org/html/2607.23134#bib.bib3)\]。然而，经典的重要性采样需要访问理想的参考分布或显式的似然模型，这些假设在现实的自主系统测试流程中很少满足。  
基于分数的生成建模和扩散过程的最新进展使得学习高维、结构化数据上的表达性联合分布成为可能，这为从分布角度重新审视罕见事件发现提供了新的机会\[13 (https://arxiv.org/html/2607.23134#bib.bib16),10 (https://arxiv.org/html/2607.23134#bib.bib7),14 (https://arxiv.org/html/2607.23134#bib.bib17)\]。与此同时，分类器引导和分数引导的扩散方法已经证明，可以通过学习的引导信号将生成过程导向数据空间中有语义意义的区域\[6 (https://arxiv.org/html/2607.23134#bib.bib18)\]。在这项工作中，我们将这些发展统一起来，将扩散引导的反例生成解释为对学习到的环境与执行轨迹联合分布的指数倾斜。我们证明，扩散引导在联合空间上诱导出一个精确的重要性采样方案，其中代理鲁棒性分数充当似然比倾斜，在温和的排序假设下可证明地放大失效概率。最后，我们证明，对于确定性动力系统，联合扩散引导倾斜简化为沿着动力学流形对输入的最优重要性采样，为分布引导的罕见事件发现提供了一个统一的理论框架。  
虽然分析动机来自反例生成和反例发现，但所提出的框架是通用的。对联合场景分布进行指数倾斜提供了一种机制，可以将采样导向安全违规之外感兴趣的行为，包括综合、证书估计。从验证角度来看，扩散引导的倾斜使得分布感知的复杂场景空间探索成为可能，而不仅限于反例生成。  
我们方法的另一个方面是**生成模型**与**被测系统（SUT）** 的分离。生成模型定义了环境和执行轨迹的先验，仅作为基础密度。因此，它不需要忠实地表示“真实”的系统动力学。我们的理论结果依赖于分数和倾斜机制的性质，而非学习模型的准确性。实际上，与SUT的交互是通过评分函数（例如鲁棒性监视器或运行时预言）进行的，因此仿真被选择性地调用，而大多数采样在生成模型内部进行。这种解耦实现了高效探索，保持了与黑箱验证流程的兼容性，并允许DiffTilt使用定义在轨迹上的任何分数，包括鲁棒性、奖励或专家定义的成本。

#### 贡献  
本文为扩散引导的反例生成作为原则性的反例生成机制提供了形式化基础。贡献如下：  
1. 1. 我们引入了反例生成的联合分布形式化，将失效发现解释为概率质量重新分配，并证明指数倾斜产生KL最优的偏置分布。  
2. 2. 我们建立了指数倾斜可证明地放大失效概率的充分必要条件，通过一阶随机占优（FOSD）表明，当分数在分布上将失效行为排在非失效行为之前时，倾斜恰好有效。  
3. 3. 我们刻画了条件采样的一个基本限制，表明即使条件分布完美，失效概率仍然受限于乘性稀有性，而联合倾斜通过重新分配联合空间中的质量克服了这一障碍。  
4. 4. 对于确定性动力系统，我们证明联合倾斜简化为沿着动力学流形对输入的最优重要性采样，将该框架与黑箱模拟器和现有的基于仿真的验证工作流程连接起来。  
5. 5. 我们提出了从\[12 (https://arxiv.org/html/2607.23134#bib.bib22)\]改编的TT2D牵引-拖车基准测试，作为可控的反例生成基准，提供了一个表达性设置，其中反例生成难度可以系统性地调整。  
这些结果使所提出的扩散引导反例生成DiffTilt成为基于重要性采样理论和随机序分析、可靠且具分布感知能力的反例生成增强方法，直接适用于复杂CPS的验证与确认。

## II. 扩散引导搜索作为重要性采样（IS）  
我们首先对本文考虑的场景采样器类别进行形式化。我们不限定于特定的算法或实现，而是采用抽象视角：生成模型定义了环境和执行轨迹的基础分布，通过评分函数引入引导，使采样偏向感兴趣的行为。这种抽象允许我们独立于底层生成模型的获取方式推理引导采样，并隔离驱动失效发现的概率机制。特别地，我们考虑在环境参数和系统执行轨迹的联合空间上运行的采样器，并且可以使用基于似然的重加权进行引导。扩散模型提供了该类采样器的一个便捷且富有表达力的实例，但本节中的形式化更广泛地适用于任何支持从联合密度采样和评估似然比的生成机制。本节的其余部分介绍了将在全文中使用的符号、假设和采样原语，为第III节 (https://arxiv.org/html/2607.23134#S3) 中的形式化分析奠定基础。

#### 预备知识  
令 $z_0 = (x, y) \in \mathbb{R}^d$ 为输入和对应输出的向量化表示。扩散模型通过定义两个耦合的马尔可夫链来学习从 $p(z_0)$ 生成样本：一个固定的**前向过程**，逐步将 $z_0$ 破坏为高斯噪声；以及一个学习的**反向过程**，对噪声样本进行去噪并将其转换回数据分布中的样本\[10 (https://arxiv.org/html/2607.23134#bib.bib7),14 (https://arxiv.org/html/2607.23134#bib.bib17)\]。

**前向过程。** 扩散模型通过一个固定的马尔可夫链将数据样本 $z_0$ 破坏为高斯噪声\[10 (https://arxiv.org/html/2607.23134#bib.bib7)\]：
$$ q(z_t \mid z_{t-1}) = \mathcal{N}\!\left(\sqrt{\alpha_t}\, z_{t-1},\, (1-\alpha_t)I\right), \tag{1} $$
边缘分布为 $q(z_t \mid z_0) = \mathcal{N}(\sqrt{\bar{\alpha}_t}\, z_0,\, (1-\bar{\alpha}_t)I)$，其中 $\bar{\alpha}_t = \prod_{s=1}^t \alpha_s$。

**反向过程和采样器。** 反向过程是一个学习的马尔可夫链 $p_\theta(z_{t-1} \mid z_t) = \mathcal{N}(\mu_\theta(z_t, t),\, \sigma_t^2 I)$。一个神经网络 $\varepsilon_\theta(z_t, t)$ 被训练来预测在时间步 $t$ 注入的噪声 $\varepsilon$\[10 (https://arxiv.org/html/2607.23134#bib.bib7)\]，从而恢复后验均值：
$$ \mu_\theta(z_t, t) = \frac{1}{\sqrt{\alpha_t}}\!\left(z_t - \frac{1-\alpha_t}{\sqrt{1-\bar{\alpha}_t}}\, \varepsilon_\theta(z_t, t)\right). \tag{2} $$
采样过程为：
$$ z_T \sim \mathcal{N}(0,I), \quad z_{t-1} = \mu_\theta(z_t, t) + \sigma_t \eta, \quad \eta \sim \mathcal{N}(0,I). \tag{3} $$

**分数解释与VP-SDE联系。** Song等人\[14 (https://arxiv.org/html/2607.23134#bib.bib17)\]证明，上述离散前向链是**方差保持SDE（VP-SDE）** 的离散化：
$$ dz = -\tfrac{1}{2} \beta(t)\, z\, dt + \sqrt{\beta(t)}\, dW_t. \tag{4} $$
在这种连续视角下，任何此类扩散的反向过程由Stein分数 $\nabla_{z_t} \log p_t(z_t)$ 通过反向时间SDE控制\[14 (https://arxiv.org/html/2607.23134#bib.bib17)\]：
$$ dz = \bigl[ f(z,t) - g(t)^2\, \nabla_z \log p_t(z) \bigr]\, dt + g(t)\, d\bar{W}_t. \tag{5} $$
噪声预测 $\varepsilon_\theta$ 与分数的关系为：
$$ \nabla_{z_t} \log p_t(z_t) \approx -\frac{\varepsilon_\theta(z_t, t)}{\sqrt{1-\bar{\alpha}_t}}, \tag{6} $$
DDPM中使用的反向扩散过程可以视为在此识别下对公式（5）的离散近似\[14 (https://arxiv.org/html/2607.23134#bib.bib17)\]。这种解释使得**引导**变得自然，因为修改分数会将样本导向 $p_t$ 的期望区域。

#### 目标采样密度  
上述采样器从基础联合分布 $p_\theta(x, y)$ 中采样，不对任何区域有偏好。然而在许多应用中，人们希望获得在标量目标函数 $R: \mathcal{Z} \to \mathbb{R}$ 下得分高的样本，无论 $R$ 编码的是任务奖励、约束违反还是对抗代价。问题在于如何在 $p_\theta$ 编码的先验不丢失的情况下将采样器偏向高得分区域。不失一般性，我们考虑最小化目标函数。令 $R(x, y)$ 为目标函数，$S_k(x, y)$ 为其代理函数，则倾斜后的采样分布为：
$$ p\left(x,y\right) := \frac{p_\theta\left(x,y\right) \exp\left(\beta S\left(x,y\right)\right)}{Z}, \quad Z = \mathbb{E}_{(X,Y)\sim p_\theta}\left[ \exp\left(\beta S\left(X,Y\right)\right) \right]. \tag{7} $$

## III. 分析  
本节对扩散引导的反例生成进行分布分析。我们将生成环境建模为环境和执行轨迹的联合分布，并研究指数倾斜对失效概率的影响。我们的目标是刻画倾斜何时放大失效、这如何依赖于评分函数，以及为什么它能克服条件采样的乘性稀有性障碍。该分析隔离了引导采样背后的概率机制，并建立了独立于特定扩散实现的保证。这些结果将扩散引导的反例生成形式化为原则性的重要性采样（IS），并阐明其相对于条件方法的优势。

#### 结果总结  
我们将罕见失效的高效发现视为重要性采样。失效需要同时存在一个稀有输入（概率 $\delta \ll 1$）和一个相应的