強化学習/時間論理2026/5/1arXiv:2605.01051

時間論理のための価値関数：最適方策と安全フィルタ

Value Functions for Temporal Logic: Optimal Policies and Safety Filters

時間論理仕様に対する価値関数の最適性と方策の最適性の微妙な関係を解明し、非マルコフ方策を用いて病理を回避する最適方策を構築するとともに、Q関数を複雑な時間論理仕様の安全フィルタとして利用する方法を示した論文。

詳しい要約

1. どんなもの？

- 時間論理（TL）仕様に対する価値関数と最適政策の関係を扱う研究。 - 基本的なreach, avoid, reach-avoid問題のBellman方程式はよく研究されているが、非割引無限ホライズン設定では価値最適性と政策最適性の関係が微妙になる。 - 特にreach-avoid問題（Until仕様）では、Q関数を貪欲に最大化すると、価値関数が最適でもタスク完了を無限に先延ばしする政策が生成される。 - 最近のTL価値関数を構成要素の価値関数のグラフに分解する結果に基づき、状態履歴に基づく非マルコフ政策を構築し、その最適性を証明。 - 入れ子になったUntil, Globally, Globally-Until仕様の定量的ロバスト性スコアに関して最適性を示す。 - Q関数を複雑なTL仕様の安全フィルタとして使用する方法も示す。

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

- 従来のreach, avoid, reach-avoid問題のBellman方程式研究を拡張し、より複雑なTL仕様（入れ子Until, Globally, Globally-Until）を扱う。 - 非割引無限ホライズン設定における価値最適性と政策最適性の微妙な関係を明らかにし、貪欲Q最大化の病理（タスク完了の無限先延ばし）を指摘。 - 最近のTL価値関数分解結果を基に、非マルコフ政策を構築し、その最適性を証明した点が新しい。 - 安全フィルタとしてのQ関数の利用を、単純なavoidやreach-avoidタスクから複雑なTL仕様に拡張。

3. 技術・手法の肝は？

- TL価値関数を構成要素の価値関数のグラフに分解する最近の結果を利用。 - 状態履歴に基づく非マルコフ政策を構築。 - 入れ子Until, Globally, Globally-Until仕様の定量的ロバスト性スコアに関して政策の最適性を証明。 - Q関数を安全フィルタとして使用し、複雑なTL仕様に拡張。

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

- 要旨からは不明（理論的証明が主と思われるが、実験的検証の記述はない）。

5. 議論はある？

- 非割引無限ホライズン設定における価値最適性と政策最適性の関係の微妙さを議論。 - 貪欲Q最大化がreach-avoid問題でタスク完了を無限に先延ばしする病理を指摘。 - 非マルコフ政策の最適性を証明し、安全フィルタとしてのQ関数の拡張を議論。

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

- 要旨で参照/比較されている研究：基本的なreach, avoid, reach-avoid問題のBellman方程式に関する研究、最近のTL価値関数分解結果。 - 関連手法：非マルコフ政策、安全フィルタ、Q関数。 - 同分野の定番：Markov Decision Processes (MDPs), Linear Temporal Logic (LTL), Reinforcement Learning。

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

著者: Oswin So, William Sharpless, Sylvia Herbert, Chuchu Fan

分類: cs.RO, cs.AI, cs.LG, cs.LO, math.OC

原文アブストラクト

While Bellman equations for basic reach, avoid, and reach-avoid problems are well studied, the relationship between value optimality and policy optimality becomes subtle in the undiscounted infinite-horizon setting, particularly for more complicated tasks. Greedily maximizing the Q-function can produce policies that indefinitely defer task completion for reach-avoid problems, or equivalently, Until specifications, even when the value function is optimal. Building upon recent results decomposing the value function for temporal logic (TL) into a graph of constituent value functions, we construct non-Markovian policies based on state history that avoid this pathology and prove their optimality with respect to the quantitative robustness score for nested Until, Globally, and Globally-Until specifications. We further show how the Q function can serve as a safety filter for complex TL specifications, extending prior results beyond simple avoid or reach-avoid tasks.

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

← 論文一覧