論文の概要: Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces

• arxiv url: http://arxiv.org/abs/2501.13712v1
• Date: Thu, 23 Jan 2025 14:43:12 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-01-24 19:17:07.303879
• Title: Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces
• Title（参考訳）: 有限トレース上のテンソルに基づく線形時間論理による形式検証されたニューロシンボリック軌道学習
• Authors: Mark Chevallier, Filip Smola, Richard Schmoetten, Jacques D. Fleuriot,
• Abstract要約: 有限トレース(LTLf)上の線形時間論理に対するテンソル意味論の新しい形式化を提案する。 我々は,この形式化を,制約に対する識別可能な損失関数の定義と検証によって,ニューロシンボリック学習プロセスに統合できることを実証した。 この損失を利用して、プロセスは事前に特定された論理的制約を満たすことを学ぶ。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present a novel formalisation of tensor semantics for linear temporal logic on finite traces (LTLf), with formal proofs of correctness carried out in the theorem prover Isabelle/HOL. We demonstrate that this formalisation can be integrated into a neurosymbolic learning process by defining and verifying a differentiable loss function for the LTLf constraints, and automatically generating an implementation that integrates with PyTorch. We show that, by using this loss, the process learns to satisfy pre-specified logical constraints. Our approach offers a fully rigorous framework for constrained training, eliminating many of the inherent risks of ad-hoc, manual implementations of logical aspects directly in an "unsafe" programming language such as Python, while retaining efficiency in implementation.
• Abstract（参考訳）: 定理証明器 Isabelle/HOL において,有限トレース(LTLf)上の線形時間論理に対するテンソル意味論の新たな形式化について述べる。 本稿では,LTLf制約に対する識別可能な損失関数を定義し検証し,PyTorchと統合した実装を自動的に生成することにより,この形式化をニューロシンボリック学習プロセスに統合できることを実証する。 この損失を利用して、プロセスは事前に特定された論理的制約を満たすことを学ぶ。 このアプローチは制約付きトレーニングのための厳格なフレームワークを提供し、Pythonのような"安全でない"プログラミング言語に直接論理的側面を手動で実装し、実装の効率を保ちながら、アドホックなリスクの多くを排除します。

関連論文リスト

• Distilling Formal Logic into Neural Spaces: A Kernel Alignment Approach for Signal Temporal Logic [6.419602857618508]
  形式仕様の連続的ニューラル表現を学習するためのフレームワークを導入する。 シンボリックロバストネスカーネルをトランスフォーマーエンコーダに蒸留する。 エンコーダは1つのフォワードパスに埋め込みを生成し、計算コストのごく一部でカーネルのロジックを効果的に模倣する。
  論文  参考訳（メタデータ） (2026-03-05T14:08:25Z)
• 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)
• Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification [49.506412445511934]
  大きな言語モデル(LLM)は目覚ましい能力を示すが、その次は論理的不整合と報奨ハックを生み出す。 本稿では,自然言語生成プロセスと形式的記号的検証を動的にインターリーブする形式論理検証誘導フレームワークを提案する。 我々はこのフレームワークを,形式論理検証誘導制御による微調整とポリシー最適化の相乗効果を生かした,新しい2段階のトレーニングパイプラインを通じて運用する。
  論文  参考訳（メタデータ） (2026-01-30T07:01:25Z)
• Neuro-Symbolic Predictive Process Monitoring [7.295472411867107]
  本稿では,データ駆動学習と時間論理に基づく事前知識を統合したニューロシンボリック予測プロセスモニタリング(PPM)手法を提案する。 本稿では,有限トレース(LTLf)上の線形時間論理を自己回帰列予測器のトレーニングプロセスに組み込む新しい手法を提案する。 実世界の3つのデータセットを実験的に評価したところ,本手法は接尾辞予測精度と時間的制約の遵守を改善した。
  論文  参考訳（メタデータ） (2025-08-31T13:07:17Z)
• T-ILR: a Neurosymbolic Integration for LTLf [47.316620315732024]
  本稿では,時間論理の仕様をシーケンスベースタスクのためのディープラーニングアーキテクチャに直接組み込むニューロシンボリックフレームワークを提案する。 提案手法をT-ILR (Temporal Iterative Local Refinement) と呼ぶ。
  論文  参考訳（メタデータ） (2025-08-21T20:24:20Z)
• On Scaling Neurosymbolic Programming through Guided Logical Inference [1.124958340749622]
  そこで我々は,論理的証明の計算をバイパスするアルゴリズムNLを提案する。 このアプローチは, ApproxDPNL と呼ばれる $epsilon$ あるいは $(epsilon, delta)$ 保証を用いて近似推論に適応可能であることを示す。
  論文  参考訳（メタデータ） (2025-01-30T08:49:25Z)
• Directed Exploration in Reinforcement Learning from Linear Temporal Logic [59.707408697394534]
  リニア時間論理(LTL)は強化学習におけるタスク仕様のための強力な言語である。 合成された報酬信号は基本的に疎結合であり,探索が困難であることを示す。 我々は、仕様をさらに活用し、それに対応するリミット決定性B"uchi Automaton(LDBA)をマルコフ報酬プロセスとしてキャストすることで、よりよい探索を実現することができることを示す。
  論文  参考訳（メタデータ） (2024-08-18T14:25:44Z)
• stl2vec: Semantic and Interpretable Vector Representation of Temporal Logic [0.5956301166481089]
  論理式を意味的に基底としたベクトル表現(機能埋め込み)を提案する。 我々はいくつかの望ましい性質を持つ公式の連続的な埋め込みを計算する。 本稿では,学習モデル検査とニューロシンボリック・フレームワークの2つの課題において,アプローチの有効性を実証する。
  論文  参考訳（メタデータ） (2024-05-23T10:04:56Z)
• Semantic Objective Functions: A distribution-aware method for adding logical constraints in deep learning [4.854297874710511]
  制約付き学習と知識蒸留技術は有望な結果を示した。 本稿では,機械学習モデルに知識を付加した論理的制約を組み込むロスベース手法を提案する。 本手法は,論理的制約のある分類タスクを含む,様々な学習課題において評価する。
  論文  参考訳（メタデータ） (2024-05-03T19:21:47Z)
• TLINet: Differentiable Neural Network Temporal Logic Inference [10.36033062385604]
  本稿では,STL式を学習するニューラルネットワークシンボリックフレームワークであるTLINetを紹介する。 従来の手法とは対照的に,時間論理に基づく勾配法に特化して設計された最大演算子の近似法を導入する。 我々のフレームワークは、構造だけでなく、STL公式のパラメータも学習し、演算子と様々な論理構造の柔軟な組み合わせを可能にします。
  論文  参考訳（メタデータ） (2024-05-03T16:38:14Z)
• Constrained Training of Neural Networks via Theorem Proving [0.2578242050187029]
  有限トレース上の線形時間論理の深い埋め込み(LTL$_f$)を定式化する。 次に、損失関数 $mathcalL$ を形式化し、その関数 $dmathcalL$ に微分可能であることを正式に証明する。 本研究では,動的運動のための既存のディープラーニングフレームワークのトレーニングに使用する場合,共通の運動仕様パターンに対する予測結果が得られたことを示す。
  論文  参考訳（メタデータ） (2022-07-08T13:13:51Z)
• Semantic Probabilistic Layers for Neuro-Symbolic Learning [83.25785999205932]
  我々は構造化出力予測(SOP)のための予測層を設計する。 予測が事前に定義されたシンボリック制約のセットと一致していることを保証するため、任意のニューラルネットワークにプラグインすることができる。 我々のセマンティック確率層(SPL)は、構造化された出力空間上で複雑な相関や制約をモデル化することができる。
  論文  参考訳（メタデータ） (2022-06-01T12:02:38Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• Leveraging Unlabeled Data for Entity-Relation Extraction through Probabilistic Constraint Satisfaction [54.06292969184476]
  シンボリックドメイン知識の存在下でのエンティティ関係抽出の問題を研究する。 本手法では,論理文の正確な意味を捉える意味的損失を用いる。 低データ体制に焦点をあてて、セマンティックな損失がベースラインをはるかに上回ることを示す。
  論文  参考訳（メタデータ） (2021-03-20T00:16:29Z)
• Reinforcement Learning with External Knowledge by using Logical Neural Networks [67.46162586940905]
  論理ニューラルネットワーク(LNN)と呼ばれる最近のニューラルシンボリックフレームワークは、ニューラルネットワークとシンボリックロジックの両方のキープロパティを同時に提供することができる。 外部知識ソースからのモデルフリー強化学習を可能にする統合手法を提案する。
  論文  参考訳（メタデータ） (2021-03-03T12:34:59Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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