論文の概要: Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version)

• arxiv url: http://arxiv.org/abs/2204.13693v1
• Date: Thu, 28 Apr 2022 17:57:33 GMT
• ステータス: 翻訳完了
• システム内更新日: 2022-04-29 14:56:22.431686
• Title: Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version)
• Title（参考訳）: 有限トレース上の線形時間論理モデュロ理論(拡張版)
• Authors: Luca Geatti, Alessandro Gianola and Nicola Gigante
• Abstract要約: 有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
• 参考スコア（独自算出の注目度）: 72.38188258853155
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: This paper studies Linear Temporal Logic over Finite Traces (LTLf) where proposition letters are replaced with first-order formulas interpreted over arbitrary theories, in the spirit of Satisfiability Modulo Theories. The resulting logic, called LTLf Modulo Theories (LTLfMT), is semi-decidable. Nevertheless, its high expressiveness comes useful in a number of use cases, such as model-checking of data-aware processes and data-aware planning. Despite the general undecidability of these problems, being able to solve satisfiable instances is a compromise worth studying. After motivating and describing such use cases, we provide a sound and complete semi-decision procedure for LTLfMT based on the SMT encoding of a one-pass tree-shaped tableau system. The algorithm is implemented in the BLACK satisfiability checking tool, and an experimental evaluation shows the feasibility of the approach on novel benchmarks.
• Abstract（参考訳）: 本稿では,任意の理論上で解釈された一階公式に命題文字が置き換えられる有限トレース(ltlf)上の線形時相論理について,満足性モジュラー理論の精神を用いて検討する。 結果として得られる論理は LTLf Modulo Theories (LTLfMT) と呼ばれ、半決定可能である。 それでも、その高い表現力は、データ認識プロセスのモデルチェックやデータ認識計画など、多くのユースケースで有用である。 これらの問題の一般的な不決定性にもかかわらず、満足できる事例を解くことは研究に値する妥協である。 このような事例のモチベーションと記述の後,一通り木型卓上システムのSMT符号化に基づくLTLfMTの完全半決定法を提案する。 このアルゴリズムはBLACK満足度チェックツールに実装され、新しいベンチマークにおけるアプローチの有効性を実験的に評価した。

関連論文リスト

• Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version) [49.462399222747024]
  本研究では,大規模状態空間を持つ決定過程(MDP)における非マルコフ報酬の論理的仕様に関する新しい枠組みを提案する。 我々のアプローチは有限トレース(LTLfMT)上での線形時間論理モデュロ理論を利用する 本稿では,報酬マシンとHER(Hindsight Experience Replay)をベースとした一階述語論理仕様の翻訳手法を提案する。
  論文  参考訳（メタデータ） (2026-02-05T22:11:28Z)
• LLM-Guided Quantified SMT Solving over Uninterpreted Functions [10.767268261124515]
  非線形実算術上の非解釈関数 (UF) の量子式は、Satifiability Modulo Theories (SMT) の解法に根本的な課題をもたらす。 本稿では,UFインスタンス化のセマンティックガイダンスを提供するために,大規模言語モデルを活用するフレームワークであるAquaForteを紹介する。 提案手法は,制約分離によって計算式を前処理し,構造化プロンプトを用いてLLMから数学的推論を抽出し,従来のSMTアルゴリズムと統合する。
  論文  参考訳（メタデータ） (2026-01-08T07:40:37Z)
• Satisfiability Modulo Theory Meets Inductive Logic Programming [2.3791444696448085]
  ILPはリレーショナルドメインで解釈可能なルール学習を提供するが、数値的な制約で推論と推論を行う能力には制限がある。 最近の研究は、ICPとSMT(Satisfiability Modulo Theories)との緊密な統合、あるいは特別な数値推論機構によって、これらの制限に対処し始めている。 本稿では,ILPシステムPyGolとSMTソルバZ3を結合するモジュラー代替法について検討し,PyGolが提案する候補節を,背景理論上の量化式として解釈する。 これは、記号述語としきい値、間隔を含む学習された数値制約を組み合わせたハイブリッドルールの誘導を支援する。
  論文  参考訳（メタデータ） (2025-12-15T02:08:32Z)
• DAG-Math: Graph-Guided Mathematical Reasoning in LLMs [54.231935013127206]
  大型言語モデル (LLM) は, CoT (Chain-of-Thought) による数学的問題に対して高い性能を示す 我々は、有向非巡回グラフ(DAG)上の一定の規則に基づくプロセスとしてCoTをモデル化することを提案する。 ここでは,モデルのCoT軌道がDAG構造にどの程度よく依存するかを定量化する計量である論理的近接性を導入する。
  論文  参考訳（メタデータ） (2025-10-19T21:05:17Z)
• Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
  シンボルレベルのプリコーディングにおいて,推論の複雑さの低いエンドツーエンドディープラーニング(DL)フレームワークを提案する。 提案手法は,従来の手法よりも約80倍の高速化を実現しつつ,SLPの大幅な性能向上を達成できることを示す。
  論文  参考訳（メタデータ） (2025-10-02T15:15:50Z)
• Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces [0.0]
  有限トレース(LTLf)上の線形時間論理に対するテンソル意味論の新しい形式化を提案する。 我々は,この形式化を,制約に対する識別可能な損失関数の定義と検証によって,ニューロシンボリック学習プロセスに統合できることを実証した。 この損失を利用して、プロセスは事前に特定された論理的制約を満たすことを学ぶ。
  論文  参考訳（メタデータ） (2025-01-23T14:43:12Z)
• Bisimulation Learning [55.859538562698496]
  我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。 提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
  論文  参考訳（メタデータ） (2024-05-24T17:11:27Z)
• TLINet: Differentiable Neural Network Temporal Logic Inference [10.36033062385604]
  本稿では,STL式を学習するニューラルネットワークシンボリックフレームワークであるTLINetを紹介する。 従来の手法とは対照的に,時間論理に基づく勾配法に特化して設計された最大演算子の近似法を導入する。 我々のフレームワークは、構造だけでなく、STL公式のパラメータも学習し、演算子と様々な論理構造の柔軟な組み合わせを可能にします。
  論文  参考訳（メタデータ） (2024-05-03T16:38:14Z)
• Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
  システム実行から形式仕様を自動合成する問題を考察する。 時間論理式を合成するための古典的なアプローチの多くは、公式のサイズを最小化することを目的としている。 我々は,この概念を定式化し,有界な外見を持つ簡潔な公式を合成する学習アルゴリズムを考案する。
  論文  参考訳（メタデータ） (2023-10-26T14:13:15Z)
• Instruction Tuning for Large Language Models: A Survey [52.86322823501338]
  我々は、教師付き微調整(SFT)の一般的な方法論を含む、文献の体系的なレビューを行う。 また、既存の戦略の欠陥を指摘しながら、SFTの潜在的な落とし穴についても、それに対する批判とともに検討する。
  論文  参考訳（メタデータ） (2023-08-21T15:35:16Z)
• Decidable Fragments of LTLf Modulo Theories (Extended Version) [66.25779635347122]
  一般に、fMTは、任意の決定可能な一階述語理論(例えば、線形算術)に対して、テーブルーベースの半決定手順で半決定可能であることが示されている。 有限メモリと呼ぶ抽象的意味条件を満たす任意のfMT式に対して、新しい規則で拡張されたテーブルーもまた終了することが保証されていることを示す。
  論文  参考訳（メタデータ） (2023-07-31T17:02:23Z)
• Computing unsatisfiable cores for LTLf specifications [3.251765107970636]
  有限トレース上の線形時間時間時間論理(LTLf)は、多くのアプリケーション領域で仕様を作成するためのデファクト標準になりつつある。 満足度チェックのための最先端手法を用いて、不満足なコアを抽出する4つのアルゴリズムを提案する。 結果は、異なるアルゴリズムやツールの実現可能性、有効性、相補性を示している。
  論文  参考訳（メタデータ） (2022-03-09T16:08:43Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。 まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。 次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
  論文  参考訳（メタデータ） (2021-03-18T20:22:50Z)
• Temporal Answer Set Programming [3.263632801414296]
  本稿では,その知識表現と宣言的問題解決への応用の観点から,時間論理プログラミングの概要を述べる。 本研究は,TEL(Temporal Equilibrium Logic)と呼ばれる非単調な形式論の最近の成果に焦点を当てる。 第2部では,ASP.NET に近い時間論理プログラムと呼ばれる構文的断片を定義し,この問題が解決器 TEINGO の構築においてどのように活用されたかを説明する。
  論文  参考訳（メタデータ） (2020-09-14T16:13:36Z)
• Learning Reasoning Strategies in End-to-End Differentiable Proving [50.9791149533921]
  条件付き定理プローバーは勾配に基づく最適化により最適規則選択戦略を学習する。 条件付き定理プローサは拡張性があり、CLUTRRデータセット上で最先端の結果が得られることを示す。
  論文  参考訳（メタデータ） (2020-07-13T16:22:14Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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