論文の概要: A Normal Form Characterization for Efficient Boolean Skolem Function Synthesis

• arxiv url: http://arxiv.org/abs/2104.14098v1
• Date: Thu, 29 Apr 2021 04:16:41 GMT
• ステータス: 処理完了
• システム内更新日: 2021-04-30 23:28:19.123987
• Title: A Normal Form Characterization for Efficient Boolean Skolem Function Synthesis
• Title（参考訳）: 効率的なブールスコレム関数合成のための正規形式解析
• Authors: Preey Shah, Aman Bansal, S. Akshay and Supratik Chakraborty
• Abstract要約: 本稿では,通常の合成をトラクタブルに特徴づけるSAUNFという表現形式を提案する。 AIの問題の文脈で使用されるBDDやDNNFのような確立された通常の形式よりも指数関数的に簡潔であり、SynNNFのような他のより最近提案された形式を厳密に推定する。
• 参考スコア（独自算出の注目度）: 2.093287944284448
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Boolean Skolem function synthesis concerns synthesizing outputs as Boolean functions of inputs such that a relational specification between inputs and outputs is satisfied. This problem, also known as Boolean functional synthesis, has several applications, including design of safe controllers for autonomous systems, certified QBF solving, cryptanalysis etc. Recently, complexity theoretic hardness results have been shown for the problem, although several algorithms proposed in the literature are known to work well in practice. This dichotomy between theoretical hardness and practical efficacy has motivated the research into normal forms or representations of input specifications that permit efficient synthesis, thus explaining perhaps the efficacy of these algorithms. In this paper we go one step beyond this and ask if there exists a normal form representation that can in fact precisely characterize "efficient" synthesis. We present a normal form called SAUNF that precisely characterizes tractable synthesis in the following sense: a specification is polynomial time synthesizable iff it can be compiled to SAUNF in polynomial time. Additionally, a specification admits a polynomial-sized functional solution iff there exists a semantically equivalent polynomial-sized SAUNF representation. SAUNF is exponentially more succinct than well-established normal forms like BDDs and DNNFs, used in the context of AI problems, and strictly subsumes other more recently proposed forms like SynNNF. It enjoys compositional properties that are similar to those of DNNF. Thus, SAUNF provides the right trade-off in knowledge representation for Boolean functional synthesis.
• Abstract（参考訳）: ブールスコーレム関数合成は、入力と出力の間の関係仕様を満たすような入力のブール関数として出力を合成する。 この問題はブール関数合成(Boolean functional synthesis)としても知られ、自律システムのための安全なコントローラの設計、認定QBF解決、暗号解析など、いくつかの応用がある。 近年,本論文で提案されているいくつかのアルゴリズムが実際にうまく機能することが知られているが,複雑性理論的な難易度がこの問題に対して示されてきた。 この理論的な硬さと実用性の間の二分法は、効率的な合成を可能にする入力仕様の正規形式や表現の研究を動機付け、おそらくこれらのアルゴリズムの有効性を説明する。 本稿では、この先一歩を踏み出し、「効率的な」合成を正確に特徴づける正規形式表現が存在するかどうかを問う。 我々は, 抽出可能な合成を正確に特徴付ける正規形式 SAUNF を提案する: 仕様は多項式時間合成可能なフであり, 多項式時間でSAUNF にコンパイルできる。 さらに、明細書は多項式サイズ汎関数解 iff を許容し、意味的に等価な多項式サイズソーンフ表現が存在する。 SAUNFは、BDDやDNNFのような確立された正常な形式よりも指数関数的に簡潔であり、AI問題の文脈で使用される。 DNNFと同様の組成特性を享受している。 したがって、SAUNFはブール関数合成の知識表現における正しいトレードオフを提供する。

関連論文リスト

• Efficient Reactive Synthesis Using Mode Decomposition [0.0]
  そこで本研究では,モードに基づく新しい分解アルゴリズムを提案する。 我々のアルゴリズムへの入力は、元の仕様とモードの記述である。 サブ仕様の自動生成方法を示し、全てのサブプロブレムが実現可能であれば、完全な仕様が実現可能であることを示す。
  論文  参考訳（メタデータ） (2023-12-14T08:01:35Z)
• Neural Combinatorial Logic Circuit Synthesis from Input-Output Examples [10.482805367361818]
  本稿では,入力出力の例から論理回路を合成するための,新しい完全説明可能なニューラルアプローチを提案する。 我々の方法は、ほぼ任意の原子の選択に利用できる。
  論文  参考訳（メタデータ） (2022-10-29T14:06:42Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• Adaptive n-ary Activation Functions for Probabilistic Boolean Logic [2.294014185517203]
  マッチングやアリティ向上の活性化関数を用いて,任意の論理を単一層で学習できることが示される。 我々は,非ゼロパラメータの数を信念関数の有効アリティに直接関連付ける基礎を用いて,信念表を表現する。 これにより、パラメータの間隔を誘導することで論理的複雑性を低減する最適化アプローチが開かれる。
  論文  参考訳（メタデータ） (2022-03-16T22:47:53Z)
• Statistically Meaningful Approximation: a Case Study on Approximating Turing Machines with Transformers [50.85524803885483]
  本研究は,統計的学習性を示すために近似ネットワークを必要とする統計有意(SM)近似の形式的定義を提案する。 回路とチューリングマシンの2つの機能クラスに対するSM近似について検討する。
  論文  参考訳（メタデータ） (2021-07-28T04:28:55Z)
• On Function Approximation in Reinforcement Learning: Optimism in the Face of Large State Spaces [208.67848059021915]
  強化学習のコアにおける探索・探索トレードオフについて検討する。 特に、関数クラス $mathcalF$ の複雑さが関数の複雑さを特徴づけていることを証明する。 私たちの後悔の限界はエピソードの数とは無関係です。
  論文  参考訳（メタデータ） (2020-11-09T18:32:22Z)
• Sinkhorn Natural Gradient for Generative Models [125.89871274202439]
  本研究では,シンクホーンの発散による確率空間上の最も急降下法として機能するシンクホーン自然勾配(SiNG)アルゴリズムを提案する。 本稿では,SiNG の主要成分であるシンクホーン情報行列 (SIM) が明示的な表現を持ち,対数的スケールの複雑さを正確に評価できることを示す。 本実験では,SiNGと最先端のSGD型解法を定量的に比較し,その有効性と有効性を示す。
  論文  参考訳（メタデータ） (2020-11-09T02:51:17Z)
• Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers [70.70479436076238]
  線形、非線形(ポリノミカル)およびパラメトリックモデルに対するリャプノフ関数を合成する。 パラメトリックテンプレートからLyapunov関数を合成するための帰納的フレームワークを利用する。
  論文  参考訳（メタデータ） (2020-07-21T14:45:23Z)
• Formal Synthesis of Lyapunov Neural Networks [61.79595926825511]
  本稿では,リアプノフ関数の自動合成法を提案する。 我々は,数値学習者と記号検証器が相互作用して,確実に正しいリアプノフニューラルネットワークを構築する,反例誘導方式を採用する。 提案手法は,Lyapunov関数を他の手法よりも高速かつ広い空間領域で合成する。
  論文  参考訳（メタデータ） (2020-03-19T17:21:02Z)
• Towards Neural-Guided Program Synthesis for Linear Temporal Logic Specifications [26.547133495699093]
  ニューラルネットワークを用いてQ関数を学習し、探索を誘導し、その後正当性を検証したプログラムを構築する。 提案手法は,検索と深層学習を組み合わせることで,合成を実現するのにユニークな手法である。
  論文  参考訳（メタデータ） (2019-12-31T17:09:49Z)

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

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