論文の概要: Synthesis with Explicit Dependencies
- arxiv url: http://arxiv.org/abs/2301.10556v1
- Date: Wed, 25 Jan 2023 12:51:55 GMT
- ステータス: 処理完了
- システム内更新日: 2023-01-26 15:20:40.625338
- Title: Synthesis with Explicit Dependencies
- Title（参考訳）: 明示的依存による合成
- Authors: Priyanka Golia, Subhajit Roy, and Kuldeep S. Meel
- Abstract要約: 我々はManthan3と呼ばれるヘンキン合成のためのデータ駆動型アプローチを提案する。
Manthan3は最先端のツールと競合する。
- 参考スコア（独自算出の注目度）: 35.159590750027
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Quantified Boolean Formulas (QBF) extend propositional logic with
quantification $\forall, \exists$. In QBF, an existentially quantified variable
is allowed to depend on all universally quantified variables in its scope.
Dependency Quantified Boolean Formulas (DQBF) restrict the dependencies of
existentially quantified variables. In DQBF, existentially quantified variables
have explicit dependencies on a subset of universally quantified variables
called Henkin dependencies. Given a Boolean specification between the set of
inputs and outputs, the problem of Henkin synthesis is to synthesize each
output variable as a function of its Henkin dependencies such that the
specification is met. Henkin synthesis has wide-ranging applications, including
verification of partial circuits, controller synthesis, and circuit
realizability.
This work proposes a data-driven approach for Henkin synthesis called
Manthan3. On an extensive evaluation of over 563 instances arising from past
DQBF solving competitions, we demonstrate that Manthan3 is competitive with
state-of-the-art tools. Furthermore, Manthan3 could synthesize Henkin functions
for 26 benchmarks for which none of the state-of-the-art techniques could
synthesize.
- Abstract（参考訳）: quantified boolean formulas (qbf) は命題論理を量子化 $\forall, \exists$ で拡張する。
QBF では、存在量化変数はその範囲内のすべての普遍量化変数に依存することが許される。
依存量子化ブール式(DQBF)は、存在量化変数の依存関係を制限する。
DQBF では、存在量化変数はヘンキン依存と呼ばれる普遍量化変数のサブセットに明示的な依存関係を持つ。
入力と出力の集合の間のブール仕様が与えられると、ヘンキン合成の問題は、それぞれの出力変数をそのヘンキン依存性の関数として合成し、その仕様が満たされることである。
ヘンキン合成は、部分回路の検証、コントローラ合成、回路実現可能性など幅広い応用がある。
本研究は、マンタン3と呼ばれるヘンキン合成のためのデータ駆動アプローチを提案する。
過去のDQBF解決コンペから発生した553以上のインスタンスを広範囲に評価し、Manthan3が最先端のツールと競合することを示した。
さらに、Manthan3は26のベンチマークでヘンキン関数を合成することができた。
関連論文リスト
- Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
本稿では, パール構造因果モデルにおいて, 因果関係などの部分的特定可能なクエリのバウンダリングの問題について議論する。
最近提案された反復EMスキームは初期化パラメータをサンプリングしてそれらの境界を内部近似する。
シンボルパラメータを実際の値に置き換えた回路構造を,単一のシンボル知識コンパイルによって得られることを示す。
論文 参考訳（メタデータ） (2023-10-05T07:10:40Z) - RelationPrompt: Leveraging Prompts to Generate Synthetic Data for
Zero-Shot Relation Triplet Extraction [65.4337085607711]
ゼロショット関係トリプルト抽出(ZeroRTE)のタスク設定について紹介する。
入力文が与えられた後、抽出された各三重項は、トレーニング段階で関係ラベルが見えないヘッドエンティティ、リレーションラベル、テールエンティティから構成される。
本稿では、言語モデルに構造化テキストを生成するよう促すことで、関係例を合成する。
論文 参考訳（メタデータ） (2022-03-17T05:55:14Z) - Computational Graph Completion [0.8122270502556374]
計算知識の生成、編成、推論のためのフレームワークを導入する。
計算科学と工学のほとんどの問題は、計算グラフを完成させるものであると記述できるという観察から動機づけられている。
論文 参考訳（メタデータ） (2021-10-20T00:32:06Z) - Engineering an Efficient Boolean Functional Synthesis Engine [22.075107339383255]
入力と出力の集合間のブール仕様が与えられたとき、関数合成の問題は、各出力を仕様が満たされるような入力の関数として合成することである。
関数合成のためのデータ駆動型フレームワークに対して,4つのアルゴリズム改良を提案する。
Manthan2はManthanに比べて実行時のパフォーマンスが大幅に向上した。
論文 参考訳（メタデータ） (2021-08-12T13:01:49Z) - Realization of arbitrary doubly-controlled quantum phase gates [62.997667081978825]
本稿では,最適化問題における短期量子優位性の提案に着想を得た高忠実度ゲートセットを提案する。
3つのトランペット四重項のコヒーレントな多レベル制御を編成することにより、自然な3量子ビット計算ベースで作用する決定論的連続角量子位相ゲートの族を合成する。
論文 参考訳（メタデータ） (2021-08-03T17:49:09Z) - Statistically Meaningful Approximation: a Case Study on Approximating
Turing Machines with Transformers [50.85524803885483]
本研究は,統計的学習性を示すために近似ネットワークを必要とする統計有意(SM)近似の形式的定義を提案する。
回路とチューリングマシンの2つの機能クラスに対するSM近似について検討する。
論文 参考訳（メタデータ） (2021-07-28T04:28:55Z) - Program Synthesis as Dependency Quantified Formula Modulo Theory [21.817030743512568]
本稿では,文法を含まない合成技術の実現可能性について検討する。
我々は、依存量化フォーミュラモデュロ理論の証人を見つける問題に対して、$mathbbT$-制約付き合成をDQF($mathbbT$)に還元できることを示した。
論文 参考訳（メタデータ） (2021-05-19T16:05:20Z) - A Normal Form Characterization for Efficient Boolean Skolem Function
Synthesis [2.093287944284448]
本稿では,通常の合成をトラクタブルに特徴づけるSAUNFという表現形式を提案する。
AIの問題の文脈で使用されるBDDやDNNFのような確立された通常の形式よりも指数関数的に簡潔であり、SynNNFのような他のより最近提案された形式を厳密に推定する。
論文 参考訳（メタデータ） (2021-04-29T04:16:41Z) - Programming by Rewards [20.626369097817715]
我々は、性能、資源利用、あるいはベンチマーク上の正確性などの量的指標を最適化するための新しいアプローチである「報酬によるプログラミング」 (PBR) を定式化し、研究する。
PBR仕様は、(1)入力機能$x$と(2)報酬関数$r$で構成され、ブラックボックスコンポーネントとしてモデル化されている(実行しかできない)。
フレームワークは理論的に確立された -- 報酬が優れた特性を満たす場合において、合成されたコードは正確な意味で最適であることを示す。
論文 参考訳（メタデータ） (2020-07-14T05:49:14Z) - Conditional Self-Attention for Query-based Summarization [49.616774159367516]
条件依存モデリング用に設計されたニューラルネットワークモジュールであるテキスト条件自己アテンション(CSA)を提案する。
DebatepediaとHotpotQAベンチマークデータセットの実験は、CSAがバニラトランスフォーマーを一貫して上回っていることを示している。
論文 参考訳（メタデータ） (2020-02-18T02:22:31Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。