論文の概要: Formal Explanations for Linear Temporal Logic over Finite Traces

• arxiv url: http://arxiv.org/abs/2610.35169v1
• Date: Mon, 26 Oct 2026 10:33:46 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-27 22:27:13.829404
• Title: Formal Explanations for Linear Temporal Logic over Finite Traces
• Title（参考訳）: 有限トレース上の線形時間論理の形式的説明
• Abstract要約: LTLf(Linear Temporal Logic over Finite Traces)は人工知能において望まれる時間的行動を特定するために広く使われている。 有限トレース上での帰納的(AXps)と対照的な(CXps)説明のネイティブな特徴を導入する。
• 参考スコア（独自算出の注目度）: 5.792385818430938
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Linear Temporal Logic over Finite Traces (LTLf) is widely used in Artificial Intelligence to specify desired temporal behavior and determine whether finite traces satisfy or violate it. Explaining these outcomes is essential for debugging and trust. However, existing approaches typically capture either sufficient reasons or counterfactual causes, without clarifying their relationship. We introduce a native characterization of abductive (AXps) and contrastive (CXps) explanations directly over finite traces, based on locking and unlocking time-indexed events. We prove its equivalence to the classifier-based formulation, and show that CXps coincide with a recently proposed temporal causality semantics for LTLf. This characterization enables an efficient implementation based on the enumeration of minimal unsatisfiable cores and minimal correction sets of ASP programs. Experiments on real-world event logs demonstrate the effectiveness of the approach.
• Abstract（参考訳）: LTLf(Linear Temporal Logic over Finite Traces)は人工知能において、望ましい時間的振る舞いを特定し、有限トレースがそれを満たすか違反するかを決定するために広く使われている。 これらの結果を説明することは、デバッグと信頼に不可欠です。 しかし、既存のアプローチは通常、それらの関係を明確にすることなく、十分な理由または反現実的な原因を捉えている。 本稿では, ロックとアンロックに基づく, 帰納的 (AXps) とコントラスト的 (CXps) の説明を, 有限トレース上で直接的に導入する。 分類器に基づく定式化と等価性を証明し、最近提案されたLTLfの時間因果意味論とCXpsが一致することを示す。 この特徴付けにより、最小の満足できないコアと最小のASPプログラムの修正セットの列挙に基づく効率的な実装が可能となる。 実世界のイベントログの実験では、このアプローチの有効性が示されている。

関連論文リスト

• On Synthesis of Metric Interval Temporal Logics [0.5505634045241289]
  本稿では,表現型時間論理の適応型学習に最初に取り組む枠組みを提案する。 我々のアプローチは、タイムドラーニングの問題を、拡張性のある未使用のものに正式に還元します。 いくつかのベンチマークで実装を評価し,提案手法の有効性を実証した。
  論文  参考訳（メタデータ） (2026-09-01T10:30:46Z)
• AdapTime: Enabling Adaptive Temporal Reasoning in Large Language Models [65.97075015662318]
  AdapTimeは適応的な時間的推論手法であり、入力コンテキストに基づいて推論ステップを動的に実行する。 最先端のLCMとシームレスに統合され、外部サポートに頼ることなく、時間的推論能力を大幅に向上する。
  論文  参考訳（メタデータ） (2026-04-27T08:34:40Z)
• Towards plausibility in time series counterfactual explanations [0.0]
  本稿では,時系列分類問題に対する妥当な反実的説明を生成するための新しい手法を提案する。 この手法は入力空間内で直接勾配に基づく最適化を行う。 妥当性を高めるために、ターゲットクラスの$k$-nearest 隣人とソフトDTWアライメントを統合する。
  論文  参考訳（メタデータ） (2026-03-09T13:13:52Z)
• On Multi-Step Theorem Prediction via Non-Parametric Structural Priors [50.16583672681106]
  本研究では,インコンテキスト学習(ICL)のレンズによる学習自由な定理予測について検討する。 本稿では,過去の解の時間的依存関係を有向グラフとしてエンコードし,推論中に探索空間を効果的に引き起こす明示的なトポロジ的制約を課すTheorem Precedence Graphsを提案する。 FormalGeo7kベンチマークの実験から,本手法は89.29%の精度を実現し,ICLベースラインを著しく上回り,最先端の教師付きモデルに適合することがわかった。
  論文  参考訳（メタデータ） (2026-03-05T06:08:50Z)
• Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
  現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。 本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-10-29T15:30:31Z)
• Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces [0.0]
  有限トレース(LTLf)上の線形時間論理に対するテンソル意味論の新しい形式化を提案する。 我々は,この形式化を,制約に対する識別可能な損失関数の定義と検証によって,ニューロシンボリック学習プロセスに統合できることを実証した。 この損失を利用して、プロセスは事前に特定された論理的制約を満たすことを学ぶ。
  論文  参考訳（メタデータ） (2025-01-23T14:43:12Z)
• Conformance Checking of Fuzzy Logs against Declarative Temporal Specifications [22.272099472568893]
  本稿では,ファジィ事象データが宣言的時間規則に適合するかどうかをDeclareパターンとして検討する。 これは、各瞬間に1つのアクティビティのみが実行されるという仮定を緩める必要がある。 PyTorch Pythonライブラリに基づいた概念実証,効率的な実装を提供する。
  論文  参考訳（メタデータ） (2024-06-17T20:38:57Z)
• On the Identification of Temporally Causal Representation with Instantaneous Dependence [50.14432597910128]
  時間的因果表現学習は時系列観測から潜在因果過程を特定することを目的としている。 ほとんどの方法は、潜在因果過程が即時関係を持たないという仮定を必要とする。 我々は,インスタントtextbfOus textbfLatent dynamics のための textbfIDentification フレームワークを提案する。
  論文  参考訳（メタデータ） (2024-05-24T08:08:05Z)
• TLINet: Differentiable Neural Network Temporal Logic Inference [10.36033062385604]
  本稿では,STL式を学習するニューラルネットワークシンボリックフレームワークであるTLINetを紹介する。 従来の手法とは対照的に,時間論理に基づく勾配法に特化して設計された最大演算子の近似法を導入する。 我々のフレームワークは、構造だけでなく、STL公式のパラメータも学習し、演算子と様々な論理構造の柔軟な組み合わせを可能にします。
  論文  参考訳（メタデータ） (2024-05-03T16:38:14Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)

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

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