Model Checking for Reinforcement Learning in Autonomous Driving: One Can Do More Than You Think!

要約

ほとんどの強化学習 (RL) プラットフォームは、Python を使用する OpenAI Gymnasium などの高レベル プログラミング言語を使用します。
これらのフレームワークは、自動運転 (AD) やロボット工学など、さまざまなドメインで RL アルゴリズムをテストするためのさまざまな API とベンチマークを提供します。
これらのプラットフォームは多くの場合、RL アルゴリズムの設計とトレーニングのパフォーマンスを重視しますが、RL の適用を成功させるために重要なモデルと報酬関数の正確性を無視します。
この論文では、形式的手法を使用して AD システムをモデル化することを提案し、AD の RL でモデル チェック (MC) をどのように使用できるかを示します。
MC と RL を組み合わせた研究のほとんどは、安全シールドなどの安全性に焦点を当てています。
ただし、この論文では、MC が RL を強化できるさまざまな側面を示しています。
まず、MC ベースのモデルの事前分析により、センサーの精度と学習ステップ サイズに関するバグが明らかになります。
このステップは RL の準備として機能し、バグが存在する場合に時間を節約し、ターゲット システムに対するユーザーの理解を深めます。
第 2 に、報酬オートマトンは報酬関数の設計に利益をもたらし、特に学習目標が複数ある場合に学習パフォーマンスを大幅に向上させることができます。
これらの発見はすべて実験によって裏付けられています。

要約(オリジナル)

Most reinforcement learning (RL) platforms use high-level programming languages, such as OpenAI Gymnasium using Python. These frameworks provide various API and benchmarks for testing RL algorithms in different domains, such as autonomous driving (AD) and robotics. These platforms often emphasise the design of RL algorithms and the training performance but neglect the correctness of models and reward functions, which can be crucial for the successful application of RL. This paper proposes using formal methods to model AD systems and demonstrates how model checking (MC) can be used in RL for AD. Most studies combining MC and RL focus on safety, such as safety shields. However, this paper shows different facets where MC can strengthen RL. First, an MC-based model pre-analysis can reveal bugs with respect to sensor accuracy and learning step size. This step serves as a preparation of RL, which saves time if bugs exist and deepens users’ understanding of the target system. Second, reward automata can benefit the design of reward functions and greatly improve learning performance especially when the learning objectives are multiple. All these findings are supported by experiments.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google