微分可能シミュレーションによる線形時相論理（LTL）での加速学習

要旨: 強化学習（RL）コントローラが現実の環境において安全性と信頼性の制約を満たすことを保証するのは、依然として難しい課題です。状態回避や制約付きマルコフ決定過程は、しばしば軌道レベルの要求を十分に捉えられなかったり、過度に保守的な挙動を引き起こしたりします。線形時相論理（LTL）などの形式仕様言語は、正しさが構成に組み込まれた目的（correct-by-construction）を提供しますが、その報酬は通常疎であり、ヒューリスティックな整形（shaping）が正しさを損なう可能性があります。私たちは知る限り、LTLと微分可能シミュレータを統合する初のエンドツーエンドの枠組みを提案します。この枠組みにより、形式仕様から直接、効率的な勾配ベース学習を実現します。提案法は、状態のソフトラベリングによって離散オートマトン遷移を緩和し、微分可能な報酬と、LTLに本質的に内在する疎性問題を緩和しつつ目的の健全性（objective soundness）を維持する状態表現を得ます。さらに、B"uchi受理（acceptance）を離散および微分可能なLTLリターンの両方に結び付ける理論的保証を提示し、決定論的および確率論的設定における、それらの不一致に対する調整可能な上界を導出します。実験的には、複雑で非線形、かつ接触の多い連続制御タスクにおいて、提案法は学習を大幅に加速し、離散ベースラインに対して最大で2倍のリターンを達成します。加えて、報酬マシン（reward machines）との互換性も示し、修正なしでコセーフLTLおよびLTL_\text{f}をカバーします。オートマトンに基づく報酬を微分可能にすることで、本研究は形式手法と深層強化学習を橋渡しし、連続領域における安全で仕様主導の学習を可能にします。