We introduce a method to verify stochastic reinforcement learning (RL)
policies. This approach is compatible with any RL algorithm as long as the
algorithm and its corresponding environment collectively adhere to the Markov
property. In this setting, the future state of the environment should depend
solely on its current state and the action executed, independent of any
previous states or actions. Our method integrates a verification technique,
referred to as model checking, with RL, leveraging a Markov decision process, a
trained RL policy, and a probabilistic computation tree logic (PCTL) formula to
build a formal model that can be subsequently verified via the model checker
Storm. We demonstrate our method's applicability across multiple benchmarks,
comparing it to baseline methods called deterministic safety estimates and
naive monolithic model checking. Our results show that our method is suited to
verify stochastic RL policies.

我们介绍了一种验证随机强化学习政策的方法，该方法与任何强化学习算法兼容，只要算法及其对应的环境共同遵守马尔科夫属性。我们的方法将模型检验技术与强化学习相结合，利用马尔科夫决策过程、训练好的强化学习策略和概率计算树逻辑（PCTL）公式构建一个正式模型，并通过模型检验器 Storm 进行验证。我们在多个基准测试中展示了我们的方法的适用性，并与称为确定性安全估计和简单的整体模型检验方法进行了比较。我们的结果表明，我们的方法适用于验证随机强化学习政策。