Fugu-MT 論文翻訳(概要): On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts

論文の概要: On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts

arxiv url: http://arxiv.org/abs/2408.07324v1
Date: Wed, 14 Aug 2024 06:52:58 GMT
ステータス: 処理完了
システム内更新日: 2024-08-15 14:13:57.287993
Title: On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts
Title（参考訳）: 有限トレース上のTLLのオンザフライ合成:有効解法
Authors: Shengping Xiao, Yongkang Li, Shufang Zhu, Jun Sun, Jianwen Li, Geguang Pu, Moshe Y. Vardi,
Abstract要約: トップダウン決定論的オートマトン構築に基づく有限トレース(LTLf)上での線形時間論理のオンザフライフレームワークを提案する。
参考スコア（独自算出の注目度）: 20.14001970300658
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: We present an on-the-fly synthesis framework for Linear Temporal Logic over finite traces (LTLf) based on top-down deterministic automata construction. Existing approaches rely on constructing a complete Deterministic Finite Automaton (DFA) corresponding to the LTLf specification, a process with doubly exponential complexity relative to the formula size in the worst case. In this case, the synthesis procedure cannot be conducted until the entire DFA is constructed. This inefficiency is the main bottleneck of existing approaches. To address this challenge, we first present a method for converting LTLf into Transition-based DFA (TDFA) by directly leveraging LTLf semantics, incorporating intermediate results as direct components of the final automaton to enable parallelized synthesis and automata construction. We then explore the relationship between LTLf synthesis and TDFA games and subsequently develop an algorithm for performing LTLf synthesis using on-the-fly TDFA game solving. This algorithm traverses the state space in a global forward manner combined with a local backward method, along with the detection of strongly connected components. Moreover, we introduce two optimization techniques -- model-guided synthesis and state entailment -- to enhance the practical efficiency of our approach. Experimental results demonstrate that our on-the-fly approach achieves the best performance on the tested benchmarks and effectively complements existing tools and approaches.
Abstract（参考訳）: トップダウン決定論的オートマトン構築に基づく有限トレース(LTLf)上での線形時間論理のオンザフライ合成フレームワークを提案する。既存のアプローチでは、LTLf仕様に対応する完全な決定論的有限オートマトン(DFA)の構築に依存している。この場合、DFA全体を構築するまで合成処理は行えない。この非効率性は、既存のアプローチの主なボトルネックです。この課題に対処するため,LTLfをトランジッションベースDFA(TDFA)に変換する手法として,LTLfのセマンティクスを直接活用し,中間結果を最終オートマティクスの直接成分として組み込んで並列化合成と自動構築を実現する手法を提案する。次に,LTLf合成とTDFAゲームの関係について検討し,その後,オンザフライTDFAゲーム解決を用いたTLf合成を行うアルゴリズムを開発した。このアルゴリズムは、強い連結成分の検出とともに、局所的後方法と組み合わせて、大域的に状態空間を横断する。さらに,本手法の実用性を高めるため,モデル誘導合成と状態付与という2つの最適化手法を導入する。実験結果から,我々のオンザフライアプローチは,テストベンチマーク上で最高のパフォーマンスを実現し,既存のツールやアプローチを効果的に補完することを示す。

関連論文リスト

Directed Exploration in Reinforcement Learning from Linear Temporal Logic [59.707408697394534]
リニア時間論理(LTL)は強化学習におけるタスク仕様のための強力な言語である。合成された報酬信号は基本的に疎結合であり,探索が困難であることを示す。我々は、仕様をさらに活用し、それに対応するリミット決定性B"uchi Automaton(LDBA)をマルコフ報酬プロセスとしてキャストすることで、よりよい探索を実現することができることを示す。
論文参考訳（メタデータ） (2024-08-18T14:25:44Z)
Guiding Enumerative Program Synthesis with Large Language Models [15.500250058226474]
本稿では,形式的合成ベンチマークを解くための大規模言語モデルの能力を評価する。ワンショット合成が失敗すると,新しい列挙合成アルゴリズムを提案する。形式的合成のためのスタンドアロンツールとしてGPT-3.5は,最先端の形式的合成アルゴリズムにより容易に性能が向上することがわかった。
論文参考訳（メタデータ） (2024-03-06T19:13:53Z)
OptEx: Expediting First-Order Optimization with Approximately Parallelized Iterations [12.696136981847438]
ほぼ並列化されたイテレーション (OptEx) で高速化された一階最適化を導入する。 OptExは、並列コンピューティングを活用して、その反復的ボトルネックを軽減することで、FOOの効率を高める最初のフレームワークである。我々は、カーネル化された勾配推定の信頼性とSGDベースのOpsExの複雑さを理論的に保証する。
論文参考訳（メタデータ） (2024-02-18T02:19:02Z)
FederatedScope-LLM: A Comprehensive Package for Fine-tuning Large Language Models in Federated Learning [70.38817963253034]
本稿では, ファインチューニング LLM のこれらの課題について論じ, 本パッケージ FS-LLM を主な貢献として紹介する。我々は、FLシナリオにおける将来の拡張のために、包括的フェデレーションパラメータ効率の良い微調整アルゴリズムの実装と汎用プログラミングインタフェースを提供する。本研究では, FS-LLM の有効性を検証し, FL 設定におけるパラメータ効率の高いパラメータ調整アルゴリズムを用いて, 高度な LLM のベンチマークを行う。
論文参考訳（メタデータ） (2023-09-01T09:40:36Z)
End-to-End Meta-Bayesian Optimisation with Transformer Neural Processes [52.818579746354665]
本稿では,ニューラルネットワークを一般化し,トランスフォーマーアーキテクチャを用いて獲得関数を学習する,エンド・ツー・エンドの差別化可能な最初のメタBOフレームワークを提案する。我々は、この強化学習(RL)によるエンドツーエンドのフレームワークを、ラベル付き取得データの欠如に対処できるようにします。
論文参考訳（メタデータ） (2023-05-25T10:58:46Z)
Forward LTLf Synthesis: DPLL At Work [1.370633147306388]
有限トレース(LTLf)上での線形時間論理の合成のための新しいAND-ORグラフ探索フレームワークを提案する。このようなフレームワーク内では、Davis-Putnam-Logemann-Loveland (DPLL)アルゴリズムにインスパイアされたプロシージャを考案し、次に利用可能なエージェント環境の動きを生成する。また,状態公式の構文的等価性に基づく探索ノードの等価性チェックも提案する。
論文参考訳（メタデータ） (2023-02-27T14:33:50Z)
Hierarchical Optimization-Derived Learning [58.69200830655009]
我々は,最適化モデル構築の本質的な動作とそれに対応する学習過程を同時に研究するために,階層型ODL(Hyerarchical ODL)という新しいフレームワークを構築した。これは、最適化と学習という2つの結合されたODLコンポーネントに対する最初の理論的保証である。
論文参考訳（メタデータ） (2023-02-11T03:35:13Z)
Synthesis from Satisficing and Temporal Goals [21.14507575500482]
既存のアプローチでは、割引合成からの合成技術とDS報酬の最適化を組み合わせているが、音響アルゴリズムは得られていない。合成と満足なDS報酬(しきい値を達成するリワード)を組み合わせた別のアプローチは、整数割引係数に対して健全で完備であるが、実際には分数割引係数が望まれる。この研究は、DS報酬を分数割引係数で提示することから合成するための第1音素アルゴリズムへの既存の充足アプローチを拡張した。
論文参考訳（メタデータ） (2022-05-20T23:46:31Z)
Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文参考訳（メタデータ） (2022-04-28T17:57:33Z)
Explaining Multi-stage Tasks by Learning Temporal Logic Formulas from Suboptimal Demonstrations [6.950510860295866]
本稿では,一貫した線形時間論理式(LTL)の論理構造と原子命題を学習し,実演から多段階タスクを学習する手法を提案する。学習者は、その式を満足しながらコスト関数を最適化し、学習者にはコスト関数が不確実な場合において、成功しているが潜在的に最適でないデモンストレーションが与えられる。提案アルゴリズムでは,デモのKKT(Karush-Kuhn-Tucker)最適条件と反例誘導ファルシフィケーション戦略を用いて,原子命題パラメータを学習する。
論文参考訳（メタデータ） (2020-06-03T17:40:14Z)
Formal Synthesis of Lyapunov Neural Networks [61.79595926825511]
本稿では,リアプノフ関数の自動合成法を提案する。我々は,数値学習者と記号検証器が相互作用して,確実に正しいリアプノフニューラルネットワークを構築する,反例誘導方式を採用する。提案手法は,Lyapunov関数を他の手法よりも高速かつ広い空間領域で合成する。
論文参考訳（メタデータ） (2020-03-19T17:21:02Z)

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

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