論文の概要: Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version)

• arxiv url: http://arxiv.org/abs/2602.06227v1
• Date: Thu, 05 Feb 2026 22:11:28 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-09 22:18:26.129181
• Title: Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version)
• Title（参考訳）: HERのためのDo It:強化学習における第1次時間論理リワード仕様(拡張版)
• Authors: Pierriccardo Olivieri, Fausto Lasca, Alessandro Gianola, Matteo Papini,
• Abstract要約: 本研究では,大規模状態空間を持つ決定過程(MDP)における非マルコフ報酬の論理的仕様に関する新しい枠組みを提案する。 我々のアプローチは有限トレース(LTLfMT)上での線形時間論理モデュロ理論を利用する 本稿では,報酬マシンとHER(Hindsight Experience Replay)をベースとした一階述語論理仕様の翻訳手法を提案する。
• 参考スコア（独自算出の注目度）: 49.462399222747024
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In this work, we propose a novel framework for the logical specification of non-Markovian rewards in Markov Decision Processes (MDPs) with large state spaces. Our approach leverages Linear Temporal Logic Modulo Theories over finite traces (LTLfMT), a more expressive extension of classical temporal logic in which predicates are first-order formulas of arbitrary first-order theories rather than simple Boolean variables. This enhanced expressiveness enables the specification of complex tasks over unstructured and heterogeneous data domains, promoting a unified and reusable framework that eliminates the need for manual predicate encoding. However, the increased expressive power of LTLfMT introduces additional theoretical and computational challenges compared to standard LTLf specifications. We address these challenges from a theoretical standpoint, identifying a fragment of LTLfMT that is tractable but sufficiently expressive for reward specification in an infinite-state-space context. From a practical perspective, we introduce a method based on reward machines and Hindsight Experience Replay (HER) to translate first-order logic specifications and address reward sparsity. We evaluate this approach to a continuous-control setting using Non-Linear Arithmetic Theory, showing that it enables natural specification of complex tasks. Experimental results show how a tailored implementation of HER is fundamental in solving tasks with complex goals.
• Abstract（参考訳）: 本研究では,大規模状態空間を持つマルコフ決定過程(MDP)において,非マルコフ報酬の論理的記述のための新しい枠組みを提案する。 我々のアプローチは、有限トレース(LTLfMT)よりも線形時相論理モデュロ理論(LTLfMT)を活用し、述語は単純なブール変数ではなく任意の一階理論の1次公式である古典時相論理のより表現的な拡張である。 この拡張された表現力により、非構造化および異種データドメイン上の複雑なタスクの仕様化が可能になり、手動述語エンコーディングの必要性をなくす統一的で再利用可能なフレームワークが推進される。 しかし、LTLfMTの表現力の増大は、標準LTLf仕様と比較して理論的および計算的課題を生じさせる。 理論的観点からこれらの課題に対処し、無限状態空間における報酬仕様に十分表現可能なLTLfMTの断片を同定する。 本稿では,報奨機とHER(Hindsight Experience Replay)を用いた一階述語論理仕様の翻訳手法を提案する。 このアプローチを非線形算術理論を用いて連続的な制御設定に評価し,複雑なタスクの自然な仕様化を可能にすることを示す。 実験結果から,HERの調整された実装が,複雑な目標を持つタスクの解決にいかに重要であるかが示唆された。

関連論文リスト

• LSRIF: Logic-Structured Reinforcement Learning for Instruction Following [56.517329105764475]
  命令論理を明示的にモデル化するロジック構造化学習フレームワーク LSRIF を提案する。 実験の結果、LSRIFは命令追従と一般的な推論に大きな改善をもたらすことが示された。
  論文  参考訳（メタデータ） (2026-01-10T05:11:38Z)
• Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
  シンボルレベルのプリコーディングにおいて,推論の複雑さの低いエンドツーエンドディープラーニング(DL)フレームワークを提案する。 提案手法は,従来の手法よりも約80倍の高速化を実現しつつ,SLPの大幅な性能向上を達成できることを示す。
  論文  参考訳（メタデータ） (2025-10-02T15:15:50Z)
• Proof of Thought : Neurosymbolic Program Synthesis allows Robust and Interpretable Reasoning [1.3003982724617653]
  大規模言語モデル(LLM)は自然言語処理に革命をもたらしたが、一貫性のない推論に苦戦している。 本研究では,LLM出力の信頼性と透明性を高めるフレームワークであるProof of Thoughtを紹介する。 主な貢献は、論理的整合性を高めるためのソート管理を備えた堅牢な型システム、事実的知識と推論的知識を明確に区別するための規則の明示である。
  論文  参考訳（メタデータ） (2024-09-25T18:35:45Z)
• On the Diagram of Thought [20.805936414171892]
  大規模言語モデル(LLM)は多くのタスクで優れているが、構造化された多段階の推論を必要とする複雑な問題に悩まされることが多い。 思考のダイアグラム(Diagram of Thought, DoT)は、1つのLCMがその推論のメンタルマップを構築し、ナビゲートすることを可能にする新しいフレームワークである。
  論文  参考訳（メタデータ） (2024-09-16T07:01:41Z)
• Directed Exploration in Reinforcement Learning from Linear Temporal Logic [59.707408697394534]
  リニア時間論理(LTL)は強化学習におけるタスク仕様のための強力な言語である。 合成された報酬信号は基本的に疎結合であり,探索が困難であることを示す。 我々は、仕様をさらに活用し、それに対応するリミット決定性B"uchi Automaton(LDBA)をマルコフ報酬プロセスとしてキャストすることで、よりよい探索を実現することができることを示す。
  論文  参考訳（メタデータ） (2024-08-18T14:25:44Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。