Formally-Sharp DAgger for MCTS: Lower-Latency Monte Carlo Tree Search using Data Aggregation with Formal Methods

要約

私たちは、大規模なマルコフ決定プロセス (MDP) で高品質の後退期間ポリシーを生成するために、形式的手法、モンテカルロ木探索 (MCTS)、および深層学習を効率的に組み合わせる方法を研究しています。
特に、MDP の代表的な状態セットに関する高品質の決定のオフライン サンプルを生成するために、モデル チェック技術を使用して MCTS アルゴリズムをガイドします。
これらのサンプルは、サンプルの生成に使用されたポリシーを模倣するニューラル ネットワークをトレーニングするために使用できます。
このニューラル ネットワークは、低遅延の MCTS オンライン検索のガイドとして使用することも、最小限の遅延が必要な場合の本格的なポリシーとして使用することもできます。
統計モデル チェックを使用して、追加サンプルが必要な時期を検出し、学習されたニューラル ネットワーク ポリシーが (計算コストのかかる) オフライン ポリシーと異なる構成にそれらの追加サンプルを集中させます。
強化学習アルゴリズムを評価するための 2 つの一般的なベンチマークである、Frozen Lake とパックマン環境をモデル化する MDP でのメソッドの使用を示します。

要約(オリジナル)

We study how to efficiently combine formal methods, Monte Carlo Tree Search (MCTS), and deep learning in order to produce high-quality receding horizon policies in large Markov Decision processes (MDPs). In particular, we use model-checking techniques to guide the MCTS algorithm in order to generate offline samples of high-quality decisions on a representative set of states of the MDP. Those samples can then be used to train a neural network that imitates the policy used to generate them. This neural network can either be used as a guide on a lower-latency MCTS online search, or alternatively be used as a full-fledged policy when minimal latency is required. We use statistical model checking to detect when additional samples are needed and to focus those additional samples on configurations where the learnt neural network policy differs from the (computationally-expensive) offline policy. We illustrate the use of our method on MDPs that model the Frozen Lake and Pac-Man environments — two popular benchmarks to evaluate reinforcement-learning algorithms.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google