Fugu-MT 論文翻訳(概要): Multiple Query Satisfiability of Constrained Horn Clauses

論文の概要: Multiple Query Satisfiability of Constrained Horn Clauses

arxiv url: http://arxiv.org/abs/2211.15207v2
Date: Thu, 11 Jan 2024 21:55:46 GMT
ステータス: 処理完了
システム内更新日: 2024-01-16 00:29:20.095614
Title: Multiple Query Satisfiability of Constrained Horn Clauses
Title（参考訳）: 制約付きホーン節の多重クエリ充足性
Authors: Emanuele De Angelis (1), Fabio Fioravanti (2), Alberto Pettorossi (3), Maurizio Proietti (1) ((1) IASI-CNR, Rome, Italy, (2) DEc, University 'G. d'Annunzio', Chieti-Pescara, Italy, (3) DICII, University of Rome 'Tor Vergata', Italy)
Abstract要約: 本稿では,一組のクエリを含む一組のCHCを入力とし,一組のCHCを出力する手法を提案する。変換されたCHCは、各新しいクエリに適した情報を他のクエリから取得し、CHC満足度アルゴリズムが全てのクエリ間の関係を活用できるようにする。
参考スコア（独自算出の注目度）: 0.0
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: We address the problem of checking the satisfiability of a set of constrained Horn clauses (CHCs) possibly including more than one query. We propose a transformation technique that takes as input a set of CHCs, including a set of queries, and returns as output a new set of CHCs, such that the transformed CHCs are satisfiable if and only if so are the original ones, and the transformed CHCs incorporate in each new query suitable information coming from the other ones so that the CHC satisfiability algorithm is able to exploit the relationships among all queries. We show that our proposed technique is effective on a non trivial benchmark of sets of CHCs that encode many verification problems for programs manipulating algebraic data types such as lists and trees.
Abstract（参考訳）: 我々は複数のクエリを含む制約付きホーン節(chcs)のセットの充足可能性をチェックする問題に対処する。本稿では、一連のクエリを含む一連のCHCを入力として、変換されたCHCが元のクエリである場合にのみ満足できるように新しいCHCを出力する変換手法を提案し、変換されたCHCは、他のクエリから来る新しいクエリに適した情報に組み込んで、CHCが全てのクエリ間の関係を活用できるようにする。提案手法は,リストやツリーなどの代数データ型を操作するプログラムの検証問題の多くを符号化するchcの非自明なベンチマークに有効であることを示す。

関連論文リスト

Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification [0.09786690381850355]
制約付きホーンクロース(CHC)は、従来、形式的検証において低レベルな表現として用いられてきた。線形CHCに対する別のボトムアップ手法を提案し、オープンソースのモデルチェックフレームワーク THETA における2つの選択肢を評価する。
論文参考訳（メタデータ） (2024-04-23T16:46:27Z)
Matching Game for Optimized Association in Quantum Communication Networks [65.16483325184237]
本稿では,量子スイッチのためのスワップスタブルな要求-QSアソシエーションアルゴリズムを提案する。サービスされた要求の割合で、ほぼ最適(5%)のパフォーマンスを達成する。 QCNのサイズが大きくなると、スケーラビリティが向上し、ほぼ最適性能を維持することが示されている。
論文参考訳（メタデータ） (2023-05-22T03:39:18Z)
NQE: N-ary Query Embedding for Complex Query Answering over Hyper-Relational Knowledge Graphs [1.415350927301928]
複雑なクエリ応答は知識グラフの論理的推論に不可欠なタスクである。ハイパーリレーショナル知識グラフ(HKG)上のCQAのための新しいN-ary Query Embedding (NQE)モデルを提案する。 NQEは二元変換器エンコーダとファジィ論理理論を用いて全てのn-ary FOLクエリを満たす。我々は、WD50K上の多様なn-ary FOLクエリを含む、新しいCQAデータセットWD50K-NFOLを生成する。
論文参考訳（メタデータ） (2022-11-24T08:26:18Z)
Multi-Type Conversational Question-Answer Generation with Closed-ended and Unanswerable Questions [3.6825890616838066]
会話型質問応答(CQA)は、与えられたコンテキストの漸進的でインタラクティブな理解を促進する。オープンエンド,クローズドエンド,未解決の質問など,さまざまな質問タイプでCQA用のデータを合成する新しい手法を提案する。 4つの領域にまたがって、我々の合成データに基づいて訓練されたCQAシステムは、人間の注釈付きデータに基づいて訓練されたシステムに近い優れた性能を示す。
論文参考訳（メタデータ） (2022-10-24T07:01:51Z)
PACIFIC: Towards Proactive Conversational Question Answering over Tabular and Textual Data in Finance [96.06505049126345]
我々はPACIFICという新しいデータセットを提案する。既存のCQAデータセットと比較すると、PACIFICは(i)活動性、(ii)数値推論、(iii)表とテキストのハイブリッドコンテキストの3つの重要な特徴を示す。質問生成とCQAを組み合わせたPCQA(Proactive Conversational Question Answering)に基づいて,新しいタスクを定義する。 UniPCQAはPCQAのすべてのサブタスク上でマルチタスク学習を行い、Seeq2Seqの上位$kのサンプルをクロスバリデーションすることで、マルチタスク学習におけるエラー伝搬問題を緩和するための単純なアンサンブル戦略を取り入れている。
論文参考訳（メタデータ） (2022-10-17T08:06:56Z)
Bayes risk CTC: Controllable CTC alignment in Sequence-to-Sequence tasks [63.189632935619535]
予測アライメントの望ましい特性を強制するためにベイズリスクCTC(BRCTC)を提案する。 BRCTCを他の早期排出の選好と組み合わせることで、オンラインモデルの性能・遅延トレードオフが改善される。
論文参考訳（メタデータ） (2022-10-14T03:55:36Z)
Satisfiability and Containment of Recursive SHACL [4.8986598953553555]
シェープ制約言語(Shapes Constraint Language, SHACL)は、グラフ上の特定の形状を検証することでRDFデータを検証するための最近のW3C勧告言語である。これまでの研究は、バリデーション問題と、満足度と封じ込めの標準決定問題に主に焦点を合わせてきた。我々は、SHACLのセマンティクスを正確に把握するSCLと呼ばれる新しい一階言語への翻訳を提供することにより、SHACLの異なる特徴を包括的に研究する。また、SCLの2階拡張であるMSCLを提示し、単一の形式論理フレームワーク、メインで定義できるようにしました。
論文参考訳（メタデータ） (2021-08-30T08:51:03Z)
An Efficient Diagnosis Algorithm for Inconsistent Constraint Sets [68.8204255655161]
過制約問題における最小限の障害制約を識別する分割・分散型診断アルゴリズム(FastDiag)を提案する。ヒットセットの競合指向計算とfastdiagを比較し,詳細な性能解析を行う。
論文参考訳（メタデータ） (2021-02-17T19:55:42Z)
Generating Diverse and Consistent QA pairs from Contexts with Information-Maximizing Hierarchical Conditional VAEs [62.71505254770827]
非構造化テキストを文脈として与えられたQAペアを生成するための条件付き変分オートエンコーダ(HCVAE)を提案する。我々のモデルは、トレーニングにわずかなデータしか使わず、両方のタスクの全てのベースラインに対して印象的なパフォーマンス向上が得られる。
論文参考訳（メタデータ） (2020-05-28T08:26:06Z)
Query Resolution for Conversational Search with Limited Supervision [63.131221660019776]
本稿では,双方向トランスフォーマに基づくニューラルクエリ解決モデルQuReTeCを提案する。我々はQuReTeCが最先端モデルより優れており、また、QuReTeCのトレーニングに必要な人為的なデータ量を大幅に削減するために、我々の遠隔監視手法が有効であることを示す。
論文参考訳（メタデータ） (2020-05-24T11:37:22Z)
XCSP3: An Integrated Format for Benchmarking Combinatorial Constrained Problems [3.149883354098941]
新しいフォーマットはコンパクトで、可読性が高く、パースも比較的容易である。 XCSP3は、ほとんどすべての制約を包含している。ユーザは、非常に正確な基準からインスタンスを選択するための洗練されたクエリを作成できる。
論文参考訳（メタデータ） (2016-11-10T17:00:56Z)

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