Deep reinforcement learning is an increasingly popular technique for
synthesising policies to control an agent's interaction with its environment.
There is also growing interest in formally verifying that such policies are
correct and execute safely. Progress has been made in this area by building on
existing work for verification of deep neural networks and of continuous-state
dynamical systems. In this paper, we tackle the problem of verifying
probabilistic policies for deep reinforcement learning, which are used to, for
example, tackle adversarial environments, break symmetries and manage
trade-offs. We propose an abstraction approach, based on interval Markov
decision processes, that yields probabilistic guarantees on a policy's
execution, and present techniques to build and solve these models using
abstract interpretation, mixed-integer linear programming, entropy-based
refinement and probabilistic model checking. We implement our approach and
illustrate its effectiveness on a selection of reinforcement learning
benchmarks.

本研究提出了一种基于 Markov 决策过程、混合整数线性规划、熵式细化和概率模型检验的抽象方法，用于验证深度强化学习中的概率策略，并在一些强化学习基准测试上验证了其有效性。