強化学習/形式仕様2025/6/1arXiv:2506.01167

微分可能シミュレーションを用いた線形時相論理による学習の加速

Accelerated Learning with Linear Temporal Logic using Differentiable Simulation

線形時相論理(LTL)と微分可能シミュレータを統合し、形式仕様から直接勾配ベースで学習できる初のエンドツーエンド枠組みを提案。接触の多い連続制御タスクで学習を大幅に加速し、離散ベースラインの最大2倍のリターンを達成した。

詳しい要約

1. どんなもの？

- 強化学習 (RL) コントローラに linear temporal logic (LTL) の形式仕様を課し、differentiable simulator 上で勾配ベース学習を可能にする初の end-to-end フレームワーク - 離散的な automaton 遷移を状態の soft labeling で緩和し、微分可能な報酬と状態表現を得る - 接触の多い非線形連続制御タスクで検証し、training の加速と最大2倍の return を報告 - reward machines との互換性を持ち、co-safe LTL と LTL_f も変更なしで扱えると主張

2. 先行研究と比べてどこがすごい？

- state-avoidance や constrained Markov decision processes は trajectory-level 要件を捉えにくく、過度に保守的になりうる - LTL は correct-by-construction な目的を与えるが報酬が sparse で、heuristic shaping は正しさを損ないうる - 本研究は LTL と differentiable simulator を統合し、sparsity を緩和しつつ objective soundness を保つ点が新しい - 離散ベースライン比で training を大幅加速し最大2倍の return を達成したと報告

3. 技術・手法の肝は？

- 離散 automaton 遷移を状態の soft labeling により緩和し、微分可能な報酬・状態表現を構成 - LTL の sparse 報酬問題を微分可能報酬で緩和しつつ、目的の健全性を保持 - Büchi acceptance と離散/微分可能 LTL return の関係を理論的に保証 - 決定論的・確率的設定で両者の乖離に対する調整可能な bound を導出 - reward machines と互換で co-safe LTL と LTL_f を変更なしに扱う

4. どうやって有効だと検証した？

- 複雑で非線形、接触の多い連続制御タスクで実験 - 提案手法が training を大幅に加速し、離散ベースラインの最大2倍の return を達成 - reward machines との互換性、co-safe LTL と LTL_f への適用可能性を実証 - 理論面では Büchi acceptance と離散/微分可能 LTL return の関係、乖離 bound を提示

5. 議論はある？

- 微分可能報酬と離散 LTL return の乖離について、決定論的・確率的設定で調整可能な bound を導出 - soft labeling による緩和が objective soundness を保つと主張するが、bound の実用上の tightness やタスク依存性は要旨からは不明 - 実世界設定での安全性・信頼性制約の充足度や、differentiable simulator 依存の限界は要旨からは不明

6. 次に読むべき論文は？

- reward machines に関する研究 - constrained Markov decision processes を用いた安全 RL - state-avoidance に基づく手法 - LTL と RL を組み合わせた既存の automaton-based reward shaping 研究 - differentiable simulator を用いたモデルベース RL

※ AIが要旨から生成した要約です。正確性は原文をご確認ください。

著者: Alper Kamil Bozkurt, Calin Belta, Ming C. Lin

分類: cs.LG, cs.RO

原文アブストラクト

Ensuring that reinforcement learning (RL) controllers satisfy safety and reliability constraints in real-world settings remains challenging: state-avoidance and constrained Markov decision processes often fail to capture trajectory-level requirements or induce overly conservative behavior. Formal specification languages such as linear temporal logic (LTL) offer correct-by-construction objectives, yet their rewards are typically sparse, and heuristic shaping can undermine correctness. We introduce, to our knowledge, the first end-to-end framework that integrates LTL with differentiable simulators, enabling efficient gradient-based learning directly from formal specifications. Our method relaxes discrete automaton transitions via soft labeling of states, yielding differentiable rewards and state representations that mitigate the sparsity issue intrinsic to LTL while preserving objective soundness. We provide theoretical guarantees connecting B\"uchi acceptance to both discrete and differentiable LTL returns and derive a tunable bound on their discrepancy in deterministic and stochastic settings. Empirically, across complex, nonlinear, contact-rich continuous-control tasks, our approach substantially accelerates training and achieves up to twice the returns of discrete baselines. We further demonstrate compatibility with reward machines, thereby covering co-safe LTL and LTL$_\text{f}$ without modification. By rendering automaton-based rewards differentiable, our work bridges formal methods and deep RL, enabling safe, specification-driven learning in continuous domains.

arXivで原文を読む →arXiv概要ページ

← 論文一覧