Probabilistic Model Checking of Stochastic Reinforcement Learning Policies

要約

確率的強化学習 (RL) ポリシーを検証する方法を紹介します。
このアプローチは、アルゴリズムとそれに対応する環境が集合的にマルコフ特性に準拠している限り、任意の RL アルゴリズムと互換性があります。
この設定では、環境の将来の状態は、以前の状態やアクションとは関係なく、現在の状態と実行されたアクションのみに依存する必要があります。
私たちの手法では、モデル チェックと呼ばれる検証手法を RL と統合し、マルコフ決定プロセス、トレーニングされた RL ポリシー、確率的計算ツリー ロジック (PCTL) 式を利用して、後でモデルを介して検証できる正式なモデルを構築します。
チェッカーの嵐。
決定論的安全性推定および単純なモノリシック モデル チェックと呼ばれるベースライン手法と比較して、複数のベンチマークにわたるこの手法の適用性を実証します。
私たちの結果は、私たちの方法が確率的 RL ポリシーを検証するのに適していることを示しています。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google