論文の概要: Enumerating Minimal Unsatisfiable Cores of LTLf formulas
- arxiv url: http://arxiv.org/abs/2409.09485v1
- Date: Sat, 14 Sep 2024 17:15:30 GMT
- ステータス: 処理完了
- システム内更新日: 2024-09-17 20:37:27.344070
- Title: Enumerating Minimal Unsatisfiable Cores of LTLf formulas
- Title（参考訳）: LTLf式における最小不飽和核の数え上げ
- Authors: Antonio Ielo, Giuseppe Mazzotta, Rafael Peñaloza, Francesco Ricca,
- Abstract要約: 有限トレース上の線形時間論理(textLTL_f$)は、AI、プロセスマイニング、モデルチェックなどの応用で広く使われている形式主義である。
本稿では,$textLTL_f$仕様の最小不満足コア(MUC)を列挙する新しい手法を提案する。
- 参考スコア（独自算出の注目度）: 8.650929640364593
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Linear Temporal Logic over finite traces ($\text{LTL}_f$) is a widely used formalism with applications in AI, process mining, model checking, and more. The primary reasoning task for $\text{LTL}_f$ is satisfiability checking; yet, the recent focus on explainable AI has increased interest in analyzing inconsistent formulas, making the enumeration of minimal explanations for infeasibility a relevant task also for $\text{LTL}_f$. This paper introduces a novel technique for enumerating minimal unsatisfiable cores (MUCs) of an $\text{LTL}_f$ specification. The main idea is to encode a $\text{LTL}_f$ formula into an Answer Set Programming (ASP) specification, such that the minimal unsatisfiable subsets (MUSes) of the ASP program directly correspond to the MUCs of the original $\text{LTL}_f$ specification. Leveraging recent advancements in ASP solving yields a MUC enumerator achieving good performance in experiments conducted on established benchmarks from the literature.
- Abstract（参考訳）: 有限トレース上の線形時間論理($\text{LTL}_f$)は、AI、プロセスマイニング、モデルチェックなどの応用で広く使われている形式主義である。
$\text{LTL}_f$の主な推論タスクは、満足度チェックである。しかしながら、最近の説明可能なAIへのフォーカスは、一貫性のない公式の分析への関心を高め、不実現性の最小限の説明の列挙も、$\text{LTL}_f$の関連するタスクである。
本稿では,$\text{LTL}_f$仕様の最小不満足コア(MUC)を列挙する新しい手法を提案する。
主なアイデアは、$\text{LTL}_f$式をAnswer Set Programming (ASP)仕様にエンコードすることであり、ASPプログラムの最小不満足なサブセット(MUS)は、オリジナルの$\text{LTL}_f$仕様のMUCと直接対応する。
ASP 解決における最近の進歩を活用すれば、文献から確立されたベンチマークで実施された実験で優れた性能を発揮する MUC 列挙子が得られる。
関連論文リスト
- FLARE: Faithful Logic-Aided Reasoning and Exploration [50.9814063216852]
タスク分解を用いて問題空間をトラバースする新しい手法を提案する。
我々はLarge Language Modelsを使ってソリューションを計画し、クエリを事実に軟式化し、論理プログラミングコードを使って述語する。
提案手法は,生成したコードに対する推論プロセスの忠実度を計算し,外部の解法に頼らずにマルチホップ探索のステップを解析する。
論文 参考訳（メタデータ） (2024-10-14T19:39:11Z) - Benchmarking Uncertainty Quantification Methods for Large Language Models with LM-Polygraph [83.90988015005934]
不確実性定量化(英: Uncertainty Quantification、UQ)は、機械学習(ML)アプリケーションにおいて重要なコンポーネントである。
最新のUQベースラインの集合を実装した新しいベンチマークを導入する。
我々は、9つのタスクにわたるUQと正規化技術に関する大規模な実証的研究を行い、最も有望なアプローチを特定した。
論文 参考訳（メタデータ） (2024-06-21T20:06:31Z) - Transfer Q Star: Principled Decoding for LLM Alignment [105.89114186982972]
Transfer $Q*$は、ベースラインモデルを通してターゲット報酬$r$の最適値関数を推定する。
提案手法は, 従来のSoTA法で観測された準最適差を著しく低減する。
論文 参考訳（メタデータ） (2024-05-30T21:36:12Z) - Evaluating and Improving Tool-Augmented Computation-Intensive Math
Reasoning [75.74103236299477]
CoT(Chain-of- Thought prompting)とツール拡張は、大きな言語モデルを改善するための効果的なプラクティスとして検証されている。
ツールインターフェース,すなわち textbfDELI を用いた推論ステップを考慮に入れた新しい手法を提案する。
CARPと他の6つのデータセットの実験結果から、提案されたDELIは、主に競合ベースラインを上回っていることが示された。
論文 参考訳（メタデータ） (2023-06-04T17:02:59Z) - SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。
我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。
我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
論文 参考訳（メタデータ） (2023-05-16T17:55:51Z) - A Few Expert Queries Suffices for Sample-Efficient RL with Resets and
Linear Value Approximation [16.29514743112387]
最適値関数のみを線形化可能な設定において、サンプル効率のよい強化学習(RL)について検討する。
専門的なクエリと探索をブレンドするための統計的・計算学的に効率的なアルゴリズム(Delphi)を提案する。
Delphi には $tildemathcalO(d)$ エキスパートクエリと $texttpoly(d,|mathcalA|,1/varepsilon)$ 探索サンプルの量が必要です。
論文 参考訳（メタデータ） (2022-07-18T01:39:13Z) - 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 to extrapolate using continued fractions: Predicting the
critical temperature of superconductor materials [5.905364646955811]
人工知能(AI)と機械学習(ML)の分野では、未知のターゲット関数 $y=f(mathbfx)$ の近似が共通の目的である。
トレーニングセットとして$S$を参照し、新しいインスタンス$mathbfx$に対して、このターゲット関数を効果的に近似できる低複雑さの数学的モデルを特定することを目的としている。
論文 参考訳（メタデータ） (2020-11-27T04:57:40Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。