强化学习策略验证综述

# 强化学习策略验证综述
来源：https://arxiv.org/html/2607.16210
Luca Marzari¹, Ezio Bartocci¹ & Enrico Marchesini²
¹维也纳工业大学，奥地利维也纳
²麻省理工学院，美国马萨诸塞州剑桥
[email protected], [email protected], [email protected]

###### 摘要

强化学习（RL）正越来越多地应用于复杂、安全关键的领域，然而基于神经网络的策略缺乏严格的行为保障，这仍然是部署的主要障碍。近年来策略表达能力和规模的提升加剧了这一挑战，导致关于RL策略验证的研究工作迅速增长但概念上碎片化。本综述为RL验证方法提供了统一的视角。我们引入了一个分类法，沿三个轴明确现有方法之间的关系：验证范式（形式化与概率化）、时间范围（单步与多步）以及保证强度。除了分类法，我们还统一了基础理论，明确了隐含假设和局限性，并指出了新兴方向。

## 1 引言

在过去的十年中，强化学习（RL）已成为复杂高维环境中序列决策的强大框架（Mnih等人，2015（https://arxiv.org/html/2607.16210#bib.bib62））。近年来表达能力和可扩展训练方面的进步加速了在安全关键领域（如自动驾驶和能源系统）部署RL智能体的兴趣（Lichtlé等人，2024（https://arxiv.org/html/2607.16210#bib.bib174）；Marchesini等人，2025（https://arxiv.org/html/2607.16210#bib.bib76），2026（https://arxiv.org/html/2607.16210#bib.bib77））。尽管取得了这些进展，但在高风险环境中部署RL系统仍然受到缺乏严格的*行为*保证的限制。RL策略通常实现为深度神经网络（DNN），具有复杂的非线性决策边界，可能在罕见条件下、分布偏移或交互效应下表现出不安全行为（Szegedy等人，2013（https://arxiv.org/html/2607.16210#bib.bib147）；Aydeniz等人，2025（https://arxiv.org/html/2607.16210#bib.bib22））。由于仅凭经验验证无法排除此类失败（Marchesini等人，2023（https://arxiv.org/html/2607.16210#bib.bib20）；Marzari等人，2025a（https://arxiv.org/html/2607.16210#bib.bib118）），形式化和系统化的验证对于安全关键的RL应用变得至关重要。

这一需求催生了将*深度神经网络形式化验证*方法应用于RL，这些方法旨在训练后、部署前可证明地认证策略满足所需的行为属性（Liu等人，2021（https://arxiv.org/html/2607.16210#bib.bib161））。与监督学习不同，RL引发正确性属性从根本上依赖于交互、反馈以及策略执行下的分布偏移。RL策略并非在固定的输入分布上运行，而是通过闭环控制主动塑造其遇到的状态分布，导致误差累积、罕见事件失败以及可能仅在长时间跨度后才会出现的安全违规（例如，一个在每一步局部鲁棒的策略仍可能通过长时间跨度的复合误差违反安全）（Sutton和Barto，2018（https://arxiv.org/html/2607.16210#bib.bib175））。因此，RL中的验证目标不能简化为仅输入输出鲁棒性，还必须考虑时间依赖性、策略-环境耦合以及部署时的不确定性。这些特性从根本上塑造了可验证的内容以及有意义的抽象。具体来说，我们验证的属性包括安全保证（例如，碰撞避免）、鲁棒性保证（例如，对噪声或对抗性扰动的弹性）以及可达性保证（例如，任务完成）。随着RL策略在表达能力和规模上的增长，提供这些认证变得越来越具有挑战性。

| 范式 | 工具/论文 | 方法/求解器 | 时间范围 | 架构 | 鲁棒性 | 安全性 | 枚举 | 保证类型 | RL就绪 |
|------|-----------|-------------|----------|------|--------|--------|------|----------|--------|
| 形式化 | α,β-CROWN (Xu等人，2020 (https://arxiv.org/html/2607.16210#bib.bib70)) | 边界传播/线性化 | 单步 | MLP, CNN, RNN | ✓ | ✓ | × | 可靠且完备* | 是 |
|       | 单步Transformer |              | 单步 | Transformer | ✓ | × | × | 可靠 | 部分 |
|       | Nonnenum (Bak，2021 (https://arxiv.org/html/2607.16210#bib.bib30)), PyRAT (Lemesle等人，2024 (https://arxiv.org/html/2607.16210#bib.bib33)) | 抽象解释/可达性 | 单步 | MLP, CNN | ✓ | × | × | 可靠 | 是 |
|       | NNV 2.0 (Lopez等人，2023 (https://arxiv.org/html/2607.16210#bib.bib5)) |        | 单步 | MLP, Neural-ODE | ✓ | ✓ | × | 可靠 | 是 |
|       | ModelVerification.jl (Wei等人，2025 (https://arxiv.org/html/2607.16210#bib.bib14)) | 边界传播/线性化 | 单步 | MLP, CNN, Neural-ODE | ✓ | ✓ | × | 可靠且完备* | 是 |
|       | Marabou (Reluplex扩展) (Wu等人，2024 (https://arxiv.org/html/2607.16210#bib.bib31)) | SMT/MIP求解 | 单步 | MLP, CNN | ✓ | ✓ | × | 可靠且完备 | 是 |
|       | NeuralSAT (Duong等人，2024 (https://arxiv.org/html/2607.16210#bib.bib32)) |        | 单步 | MLP | ✓ | ✓ | × | 可靠且完备 | 是 |
|       | U/L-Dist (Kofnov等人，2025 (https://arxiv.org/html/2607.16210#bib.bib26)) | 边界传播/可达性 | 单步 | MLP, CNN | ✓ | × | × | 可靠且完备* | 部分 |
|       | 神经Lyapunov (Yang等人，2024 (https://arxiv.org/html/2607.16210#bib.bib155)) | 控制理论 | 多步 | 神经CBF | × | ✓ | × | 可靠且完备* | 是 |
|       | INVPROP (Kotha等人，2024 (https://arxiv.org/html/2607.16210#bib.bib141)) | 边界传播/线性化 | 单步 | MLP | × | ✓ | ✓ | 可靠 | 是 |
|       | 精确枚举 (Matoba和Fleuret，2020 (https://arxiv.org/html/2607.16210#bib.bib156)) | 原像枚举 | 单步 | MLP | × | ✓ | ✓ | 可靠且完备 | 是 |
| 概率化 | PT-LiRPA (Marzari等人，2025b (https://arxiv.org/html/2607.16210#bib.bib149)) | 概率线性松弛 | 单步 | MLP, CNN | ✓ | ✓ | × | 概率化 | 是 |
|       | 在线CBF (Marzari等人，2025c (https://arxiv.org/html/2607.16210#bib.bib115)) | 运行时监控 | 多步 | MLP + CBF | × | ✓ | ✓ | 概率化 | 是 |
|       | PL-MDP (Hasanbeig等人，2019 (https://arxiv.org/html/2607.16210#bib.bib153)) | 时序逻辑 | 多步 | MLP (抽象化) | × | ✓ | × | 概率化 | 部分 |
|       | FSC-based (Carr等人，2021 (https://arxiv.org/html/2607.16210#bib.bib40)) | 综合 | 单步 | MLP, RNN | × | ✓ | × | 概率化 | 部分 |
|       | PREMAP (Zhang等人，2025 (https://arxiv.org/html/2607.16210#bib.bib142)) | 边界传播/线性化 | 单步 | MLP | × | ✓ | ✓ | 可靠/概率化 | 部分 |
|       | 概率枚举 (Marzari等人， (https://arxiv.org/html/2607.16210#bib.bib18)) | 抽象解释/可达性+采样 | 单步 | MLP | × | ✓ | ✓ | 概率化 | 是 |

- *并非对所有方法，完备性仅在与穷举分支或线性规划求解器结合时成立。

表1：深度RL验证方法的统一分类，突出显示了单步、多步、概率化和基于枚举的公式化在保证强度和表达性之间的权衡。

图1：RL策略训练后验证流水线，突出用于建立安全保证的基于求解器的方法。

图1（https://arxiv.org/html/2607.16210#S1.F1）总结了训练后RL验证流水线，其中安全属性和训练好的策略由验证求解器分析，以产生反例、建立基于可达性的保证或枚举状态空间中的不安全区域。借助形式化方法、控制理论和统计分析，存在多种方法可以在训练后认证策略行为。这些包括通过可满足性（SAT）（Barrett和Tinelli，2018（https://arxiv.org/html/2607.16210#bib.bib146））和可达性分析（Lomuscio和Maganti，2017（https://arxiv.org/html/2607.16210#bib.bib107））提供可靠保证的确定性技术、量化随机环境中风险的概率方法（Valiant，1984（https://arxiv.org/html/2607.16210#bib.bib60）），以及结合学习策略与控制理论的混合神经符号方法（Zhao等人，2020（https://arxiv.org/html/2607.16210#bib.bib108））。尽管结果数量不断增加，但文献在概念上仍然碎片化。方法通常基于不同的假设，针对不同的正确性概念，并在不同的时间范围内运作，这使得很难比较方法或理解其基本关系。

**贡献**。我们通过引入一个统一的分类法来解决这种碎片化问题，该分类法针对基于神经网络的策略的训练后验证方法。我们沿三个核心轴组织现有方法：验证范式、属性的时间范围以及不同求解器的保证强度。除了分类法，我们使用统一的符号形式化主要RL验证问题，并提供清晰的说明性示例以阐明基本思想。我们还分析了现有方法的局限性以及表达性和可靠性之间的关键权衡。最后，我们讨论了验证现代策略架构、多智能体系统中的开放挑战，并概述了将验证技术扩展到这些设置的方向。

## 2 预备知识

强化学习通常被形式化为马尔可夫决策过程（MDP）⟨S,A,P,R,γ⟩，其中S和A分别表示有限状态空间和动作空间，P: S×A×S→[0,1]指定状态转移动态，R: S×A→ℝ是奖励函数，γ∈[0,1)是折扣因子。智能体的行为由将状态映射到动作的策略决定，在本综述的上下文中，策略由DNN参数化。部署时，策略会诱导状态-动作轨迹上的分布。

这里研究的大多数验证方法都在该策略-环境循环的抽象上推理，不同之处在于它们显式建模反馈、不确定性和时间依赖性的程度。因此，理解RL执行的哪些方面被保留或抽象掉对于解释保证至关重要。