論文の概要: Constrained LTL Specification Learning from Examples

• arxiv url: http://arxiv.org/abs/2412.02905v3
• Date: Mon, 30 Dec 2024 18:51:21 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-01-03 14:35:05.674173
• Title: Constrained LTL Specification Learning from Examples
• Title（参考訳）: 例から学ぶ制約付きLTL仕様
• Authors: Changjian Zhang, Parv Kapoor, Ian Dardik, Leyi Cui, Romulo Meira-Goes, David Garlan, Eunsuk Kang,
• Abstract要約: 制約学習と呼ばれる新しいタイプの学習問題を提案する。 肯定的な例と否定的な例に加えて、ユーザーは公式の特性に関する1つ以上の制約を指定できる。 実験により、ATLASは、最先端の学習ツールよりも優れた性能を保ちながら、新しいタイプの学習問題を解決することができることを示した。
• 参考スコア（独自算出の注目度）: 8.544277223210894
• License:
• Abstract: Temporal logic specifications play an important role in a wide range of software analysis tasks, such as model checking, automated synthesis, program comprehension, and runtime monitoring. Given a set of positive and negative examples, specified as traces, LTL learning is the problem of synthesizing a specification, in linear temporal logic (LTL), that evaluates to true over the positive traces and false over the negative ones. In this paper, we propose a new type of LTL learning problem called constrained LTL learning, where the user, in addition to positive and negative examples, is given an option to specify one or more constraints over the properties of the LTL formula to be learned. We demonstrate that the ability to specify these additional constraints significantly increases the range of applications for LTL learning, and also allows efficient generation of LTL formulas that satisfy certain desirable properties (such as minimality). We propose an approach for solving the constrained LTL learning problem through an encoding in first-order relational logic and reduction to an instance of the maximal satisfiability (MaxSAT) problem. An experimental evaluation demonstrates that ATLAS, an implementation of our proposed approach, is able to solve new types of learning problems while performing better than or competitively with the state-of-the-art tools in LTL learning.
• Abstract（参考訳）: 時間論理仕様は、モデルチェック、自動合成、プログラム理解、実行時監視など、幅広いソフトウェア分析タスクにおいて重要な役割を果たす。 トレースとして指定された正の例と負の例のセットが与えられた場合、LTL学習は、正のトレースに対して真であると評価し、負のトレースに対して偽を判定する線形時間論理(LTL)において、仕様を合成する問題である。 本稿では,制約付きLTL学習という新しいタイプのLTL学習問題を提案する。そこでは,ユーザが学習対象のLTL式の性質に対する1つ以上の制約を指定するオプションが与えられる。 これらの制約を指定できることは、LTL学習の応用範囲を大幅に増加させ、また、特定の望ましい性質(最小性など)を満たすLTL式を効率的に生成できることを実証する。 本稿では,一階関係論理のエンコーディングと最大満足度(MaxSAT)問題のインスタンス化による制約付きLTL学習問題の解法を提案する。 実験により,提案手法の実装であるATLASは,LTL学習における最先端ツールよりも優れた性能を保ちながら,新たなタイプの学習問題を解くことができることが示された。

関連論文リスト

• Regret-Free Reinforcement Learning for LTL Specifications [6.342676126028222]
  強化学習は、未知のダイナミクスを持つシステムの最適制御ポリシーを学習するための有望な方法である。 現在のRLベースの手法は保証のみを提供しており、学習フェーズにおける過渡的なパフォーマンスについての洞察を与えていない。 マルコフ決定プロセス上の仕様の一般的なクラスに対処するコントローラを学習するための,最初の後悔のないオンラインアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2024-11-18T20:01:45Z)
• CoT-TL: Low-Resource Temporal Knowledge Representation of Planning Instructions Using Chain-of-Thought Reasoning [0.0]
  CoT-TLは、自然言語仕様を表現に変換するためのデータ効率のよいインコンテキスト学習フレームワークである。 CoT-TLは、ローデータシナリオで3つの多様なデータセット間で最先端の精度を達成する。
  論文  参考訳（メタデータ） (2024-10-21T17:10:43Z)
• Attribute Controlled Fine-tuning for Large Language Models: A Case Study on Detoxification [76.14641982122696]
  本稿では,属性制御付き大規模言語モデル(LLM)の制約学習スキーマを提案する。 提案手法は, ベンチマーク上での競合性能と毒性検出タスクを達成しながら, 不適切な応答を少ないLCMに導出することを示す。
  論文  参考訳（メタデータ） (2024-10-07T23:38:58Z)
• DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications [59.01527054553122]
  リニア時間論理(LTL)は、強化学習(RL)における複雑で時間的に拡張されたタスクを特定する強力なフォーマリズムとして最近採用されている。 既存のアプローチはいくつかの欠点に悩まされており、それらは有限水平フラグメントにのみ適用でき、最適以下の解に制限され、安全制約を適切に扱えない。 本研究では,これらの問題に対処するための新しい学習手法を提案する。 提案手法は, 自動仕様のセマンティクスを明示的に表現したB"uchiaの構造を利用して, 所望の式を満たすための真理代入の順序を条件としたポリシーを学習する。
  論文  参考訳（メタデータ） (2024-10-06T21:30:38Z)
• Directed Exploration in Reinforcement Learning from Linear Temporal Logic [59.707408697394534]
  リニア時間論理(LTL)は強化学習におけるタスク仕様のための強力な言語である。 合成された報酬信号は基本的に疎結合であり,探索が困難であることを示す。 我々は、仕様をさらに活用し、それに対応するリミット決定性B"uchi Automaton(LDBA)をマルコフ報酬プロセスとしてキャストすることで、よりよい探索を実現することができることを示す。
  論文  参考訳（メタデータ） (2024-08-18T14:25:44Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。 我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。 我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
  論文  参考訳（メタデータ） (2023-05-16T17:55:51Z)
• Policy Optimization with Linear Temporal Logic Constraints [37.27882290236194]
  本稿では,線形時間論理制約を用いた政策最適化の問題点について考察する。 我々は,タスク満足度とコスト最適性の両方を保証するために,サンプル複雑性分析を楽しむモデルベースアプローチを開発した。
  論文  参考訳（メタデータ） (2022-06-20T02:58:02Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• Computing unsatisfiable cores for LTLf specifications [3.251765107970636]
  有限トレース上の線形時間時間時間論理(LTLf)は、多くのアプリケーション領域で仕様を作成するためのデファクト標準になりつつある。 満足度チェックのための最先端手法を用いて、不満足なコアを抽出する4つのアルゴリズムを提案する。 結果は、異なるアルゴリズムやツールの実現可能性、有効性、相補性を示している。
  論文  参考訳（メタデータ） (2022-03-09T16:08:43Z)
• Learning Interpretable Models in the Property Specification Language [6.875312133832079]
  IEEE標準時相論理PSLにおける公式の学習アルゴリズムを開発した。 私たちの研究は、n番目の点ごとに起こる事象のような多くの自然の性質が、言葉で表現できないという事実に動機づけられている。
  論文  参考訳（メタデータ） (2020-02-10T11:42:50Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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