論文の概要: A Compositional Framework for On-the-Fly LTLf Synthesis
- arxiv url: http://arxiv.org/abs/2508.04116v1
- Date: Wed, 06 Aug 2025 06:31:49 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-08-07 20:09:22.566683
- Title: A Compositional Framework for On-the-Fly LTLf Synthesis
- Title(参考訳): オンザフライLTLf合成のための合成フレームワーク
- Authors: Yongkang Li, Shengping Xiao, Shufang Zhu, Jianwen Li, Geguang Pu,
- Abstract要約: 両手法の強みを統合した合成フレームワークについて述べる。
我々のフレームワークは、他の解決者が扱えない顕著な数のインスタンスを解決できます。
- 参考スコア(独自算出の注目度): 7.591009777813453
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Reactive synthesis from Linear Temporal Logic over finite traces (LTLf) can be reduced to a two-player game over a Deterministic Finite Automaton (DFA) of the LTLf specification. The primary challenge here is DFA construction, which is 2EXPTIME-complete in the worst case. Existing techniques either construct the DFA compositionally before solving the game, leveraging automata minimization to mitigate state-space explosion, or build the DFA incrementally during game solving to avoid full DFA construction. However, neither is dominant. In this paper, we introduce a compositional on-the-fly synthesis framework that integrates the strengths of both approaches, focusing on large conjunctions of smaller LTLf formulas common in practice. This framework applies composition during game solving instead of automata (game arena) construction. While composing all intermediate results may be necessary in the worst case, pruning these results simplifies subsequent compositions and enables early detection of unrealizability. Specifically, the framework allows two composition variants: pruning before composition to take full advantage of minimization or pruning during composition to guide on-the-fly synthesis. Compared to state-of-the-art synthesis solvers, our framework is able to solve a notable number of instances that other solvers cannot handle. A detailed analysis shows that both composition variants have unique merits.
- Abstract(参考訳): 有限トレース(LTLf)上の線形時間論理からの反応性合成は、LTLf仕様の決定論的有限オートマトン(DFA)上の2プレイヤーゲームに還元できる。
ここでの最大の課題はDFAの構築であり、最悪の場合は2EXPTIME完全である。
既存の技術は、ゲーム解決前に構成的にDFAを構築するか、状態空間の爆発を緩和するためにオートマタの最小化を利用するか、ゲーム解決中にDFAを段階的に構築して完全なDFA構築を避けるかのいずれかである。
しかし、どちらも支配的ではない。
本稿では,両手法の強みを統合した合成オンザフライ合成フレームワークを提案する。
このフレームワークは、オートマチック(ゲームアリーナ)構築の代わりに、ゲーム解決中に構成を適用する。
最悪の場合、すべての中間結果を構成する必要があるが、これらの結果のプルーニングは後続の合成を単純化し、非実現可能性の早期検出を可能にする。
具体的には、合成前のプルーニングと、合成中のプルーニングを最大限に活用し、オンザフライ合成をガイドする2つの構成変種を許容する。
最先端の合成解法と比較して、我々のフレームワークは、他の解法が扱えない顕著な数のインスタンスを解くことができる。
詳細な分析は、両方の構成変種が固有の利点を持っていることを示している。
関連論文リスト
- Syzygy of Thoughts: Improving LLM CoT with the Minimal Free Resolution [59.39066657300045]
CoT(Chain-of-Thought)は、問題を逐次ステップに分解することで、大きな言語モデル(LLM)の推論を促進する。
思考のシジー(Syzygy of Thoughts, SoT)は,CoTを補助的,相互関連的な推論経路を導入して拡張する新しいフレームワークである。
SoTはより深い論理的依存関係をキャプチャし、より堅牢で構造化された問題解決を可能にする。
論文 参考訳(メタデータ) (2025-04-13T13:35:41Z) - On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts [20.14001970300658]
トップダウン決定論的オートマトン構築に基づく有限トレース(LTLf)上での線形時間論理のオンザフライフレームワークを提案する。
論文 参考訳(メタデータ) (2024-08-14T06:52:58Z) - Compositional Generalization in Spoken Language Understanding [58.609624319953156]
本稿では, (a) 新規スロットの組み合わせと (b) 長さの一般化の2種類の構成性について検討する。
本研究では,我々の合成SLUモデルが最先端のBERT SLUモデルより大幅に優れていることを示す。
論文 参考訳(メタデータ) (2023-12-25T21:46:06Z) - ExeDec: Execution Decomposition for Compositional Generalization in Neural Program Synthesis [54.18659323181771]
プログラム合成において望ましいいくつかの異なる構成一般化形式を特徴付ける。
本稿では,ExeDecを提案する。ExeDecは,実行サブゴールを予測し,各ステップでプログラム実行によって段階的に通知される問題を解くための,新しい分解ベースの戦略である。
論文 参考訳(メタデータ) (2023-07-26T01:07:52Z) - LeftRefill: Filling Right Canvas based on Left Reference through
Generalized Text-to-Image Diffusion Model [55.20469538848806]
leftRefillは、参照誘導画像合成のための大規模なテキスト・ツー・イメージ(T2I)拡散モデルを利用する革新的なアプローチである。
本稿では、参照誘導画像合成に大規模なテキスト・ツー・イメージ拡散モデル(T2I)を効果的に活用するための革新的なアプローチであるLeftRefillを紹介する。
論文 参考訳(メタデータ) (2023-05-19T10:29:42Z) - A Divide-Align-Conquer Strategy for Program Synthesis [5.7426444823028335]
本稿では,大規模プログラムの探索を複数の小さなプログラム合成問題に分割する例によって,構成セグメント化がプログラミングに応用可能であることを示す。
入力と出力における構成部品の構造的アライメントは、プログラム探索を導くのに使用されるペアワイズ対応に繋がる。
論文 参考訳(メタデータ) (2023-01-08T19:10:55Z) - Synthesis from Satisficing and Temporal Goals [21.14507575500482]
既存のアプローチでは、割引合成からの合成技術とDS報酬の最適化を組み合わせているが、音響アルゴリズムは得られていない。
合成と満足なDS報酬(しきい値を達成するリワード)を組み合わせた別のアプローチは、整数割引係数に対して健全で完備であるが、実際には分数割引係数が望まれる。
この研究は、DS報酬を分数割引係数で提示することから合成するための第1音素アルゴリズムへの既存の充足アプローチを拡張した。
論文 参考訳(メタデータ) (2022-05-20T23:46:31Z) - StyleT2I: Toward Compositional and High-Fidelity Text-to-Image Synthesis [52.341186561026724]
構成性の欠如は、堅牢性と公正性に深刻な影響を及ぼす可能性がある。
テキスト対画像合成の合成性を改善するための新しいフレームワークであるStyleT2Iを導入する。
その結果,StyleT2Iは入力テキストと合成画像との整合性という点で従来の手法よりも優れていた。
論文 参考訳(メタデータ) (2022-03-29T17:59:50Z) - Towards Compositional Adversarial Robustness: Generalizing Adversarial
Training to Composite Semantic Perturbations [70.05004034081377]
まず,合成逆数例を生成する新しい手法を提案する。
本手法は, コンポーネントワイド射影勾配勾配を利用して最適攻撃組成を求める。
次に,モデルロバスト性を$ell_p$-ballから複合意味摂動へ拡張するための一般化逆トレーニング(GAT)を提案する。
論文 参考訳(メタデータ) (2022-02-09T02:41:56Z) - Inducing Transformer's Compositional Generalization Ability via
Auxiliary Sequence Prediction Tasks [86.10875837475783]
体系的な構成性は人間の言語において必須のメカニズムであり、既知の部品の組換えによって新しい表現を作り出すことができる。
既存のニューラルモデルには、記号構造を学習する基本的な能力がないことが示されている。
本稿では,関数の進行と引数のセマンティクスを追跡する2つの補助シーケンス予測タスクを提案する。
論文 参考訳(メタデータ) (2021-09-30T16:41:19Z) - Finding needles in a haystack: Sampling Structurally-diverse Training
Sets from Synthetic Data for Compositional Generalization [33.30539396439008]
意味解析における合成一般化を改善するための合成発話プログラムペアの自動生成について検討する。
構造的に異なる合成例のサブセットを選択し、それらを合成一般化を改善するために利用する。
我々は,スキーマ2QAデータセットの新たな分割に対するアプローチを評価し,それが構成一般化の劇的な改善と従来のi.i.dセットアップの適度な改善につながっていることを示す。
論文 参考訳(メタデータ) (2021-09-06T16:20:47Z) - Compositional federated learning: Applications in distributionally
robust averaging and meta learning [31.97853929292195]
本稿では,新しい構成フェデレートラーニング(FL)フレームワークを解くための,効率的かつ効率的な合成フェデレートラーニング(ComFedL)アルゴリズムを提案する。
我々はComFedLアルゴリズムが$O(frac1sqrtT)$の収束率を達成することを証明した。
論文 参考訳(メタデータ) (2021-06-21T17:08:09Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。