Deep Reinforcement Learning (DRL) has gained prominence as an effective approach for control systems. However, its practical deployment is impeded by state perturbations that can severely impact system performance. Addressing this critical challenge requires robustness verification about system performance, which involves tackling two quantitative questions: (i) how to establish guaranteed bounds for expected cumulative rewards, and (ii) how to determine tail bounds for cumulative rewards. In this work, we present the first approach for robustness verification of DRL-based control systems by introducing reward martingales, which offer a rigorous mathematical foundation to characterize the impact of state perturbations on system performance in terms of cumulative rewards. Our verified results provide provably quantitative certificates for the two questions. We then show that reward martingales can be implemented and trained via neural networks, against different types of control policies. Experimental results demonstrate that our certified bounds tightly enclose simulation outcomes on various DRL-based control systems, indicating the effectiveness and generality of the proposed approach.

翻译：深度强化学习（DRL）已成为控制系统的一种有效方法。然而，其实际部署受到状态扰动的影响，这种扰动可能严重损害系统性能。应对这一关键挑战需要对系统性能进行鲁棒性验证，这涉及解决两个量化问题：（i）如何建立期望累积奖励的保证界，以及（ii）如何确定累积奖励的尾部界。本文通过引入奖励鞅，首次提出面向基于DRL控制系统的鲁棒性验证方法。奖励鞅提供了严格的数学基础，用以刻画状态扰动以累积奖励形式对系统性能的影响。我们的验证结果为上述两个问题提供了可证明的量化保证。随后，我们展示了奖励鞅可通过神经网络针对不同类型的控制策略进行实现与训练。实验结果表明，我们认证的界紧密包裹了多种基于DRL控制系统的仿真结果，验证了所提方法的有效性与通用性。