論文の概要: Program Synthesis as Dependency Quantified Formula Modulo Theory
- arxiv url: http://arxiv.org/abs/2105.09221v1
- Date: Wed, 19 May 2021 16:05:20 GMT
- ステータス: 処理完了
- システム内更新日: 2021-05-20 13:44:54.037497
- Title: Program Synthesis as Dependency Quantified Formula Modulo Theory
- Title（参考訳）: 依存量式モジュロ理論としてのプログラム合成
- Authors: Priyanka Golia, Subhajit Roy, and Kuldeep S. Meel
- Abstract要約: 本稿では,文法を含まない合成技術の実現可能性について検討する。
我々は、依存量化フォーミュラモデュロ理論の証人を見つける問題に対して、$mathbbT$-制約付き合成をDQF($mathbbT$)に還元できることを示した。
- 参考スコア（独自算出の注目度）: 21.817030743512568
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Given a specification $\varphi(X,Y)$ over inputs $X$ and output $Y$, defined
over a background theory $\mathbb{T}$, the problem of program synthesis is to
design a program $f$ such that $Y=f(X)$ satisfies the specification $\varphi$.
Over the past decade, syntax-guided synthesis (SyGuS) has emerged as a dominant
approach for program synthesis where in addition to the specification
$\varphi$, the end-user also specifies a grammar $L$ to aid the underlying
synthesis engine. This paper investigates the feasibility of synthesis
techniques without grammar, a sub-class defined as $\mathbb{T}$-constrained
synthesis.
We show that $\mathbb{T}$-constrained synthesis can be reduced to
DQF($\mathbb{T}$), i.e., to the problem of finding a witness of a Dependency
Quantified Formula Modulo Theory. When the underlying theory is the theory of
bitvectors, the corresponding DQF(BV) problem can be further reduced to
Dependency Quantified Boolean Formulas (DQBF). We rely on the progress in DQBF
solving to design DQBF-based synthesizers that outperform the domain-specific
program synthesis techniques, thereby positioning DQBF as a core representation
language for program synthesis. Our empirical analysis shows that
$\mathbb{T}$-constrained synthesis can achieve significantly better performance
than syntax-guided approaches. Furthermore, the general-purpose DQBF solvers
perform on par with domain-specific synthesis techniques.
- Abstract（参考訳）: x$ と出力 $y$ の入力に対して $\varphi(x,y)$ が与えられると、プログラム合成の問題は、$y=f(x)$ が$\varphi$ を満たすようなプログラム $f$ を設計することである。
過去10年間で、構文誘導合成(sygus)はプログラム合成の主要な手法として登場し、$\varphi$の仕様に加えて、エンドユーザーは基礎となる合成エンジンを支援するために$l$という文法も指定している。
本稿では,$\mathbb{t}$-constrained synthesisというサブクラスである文法を含まない合成手法の実現可能性について検討する。
DQF($\mathbb{T}$)、すなわち、依存量化フォーミュラ・モデュロ理論の証人を見つける問題に対して、$\mathbb{T}$-constrained synthesis は DQF($\mathbb{T}$) に還元できることを示す。
基本理論がビットベクトルの理論であるとき、対応するDQF(BV)問題は、さらに依存量化ブール式(DQBF)に還元することができる。
ドメイン固有のプログラム合成技術より優れたDQBFベースのシンセサイザーを設計し、DQBFをプログラム合成のコア表現言語として位置づけることに、DQBFの進歩を頼っている。
我々の経験的分析は、$\mathbb{T}$-constrained synthesisは構文誘導型アプローチよりもはるかに優れた性能が得られることを示している。
さらに、汎用DQBFソルバはドメイン固有の合成技術と同等に動作する。
関連論文リスト
- Neural network learns low-dimensional polynomials with SGD near the information-theoretic limit [75.4661041626338]
単一インデックス対象関数 $f_*(boldsymbolx) = textstylesigma_*left(langleboldsymbolx,boldsymbolthetarangleright)$ の等方的ガウスデータの下で勾配降下学習の問題を考察する。
SGDアルゴリズムで最適化された2層ニューラルネットワークは、サンプル付き任意のリンク関数の$f_*$を学習し、実行時の複雑さは$n asymp T asymp C(q) cdot dであることを示す。
論文 参考訳（メタデータ） (2024-06-03T17:56:58Z) - Horizon-Free and Variance-Dependent Reinforcement Learning for Latent
Markov Decision Processes [62.90204655228324]
我々は,後期マルコフ決定過程(LMDP)における強化学習(RL)の文脈を考慮した後悔の最小化について検討した。
我々は,モデル最適化と値最適化の両手法でインスタンス化できる,新しいモデルベースアルゴリズムフレームワークを設計する。
論文 参考訳（メタデータ） (2022-10-20T21:32:01Z) - SQ Lower Bounds for Learning Single Neurons with Massart Noise [40.1662767099183]
マスアートノイズの存在下で単一ニューロンを学習するPAC。
我々は、任意の定数係数内で最適な誤差を近似できる効率的なSQアルゴリズムが存在しないことを証明した。
論文 参考訳（メタデータ） (2022-10-18T15:58:00Z) - Learning a Single Neuron with Adversarial Label Noise via Gradient
Descent [50.659479930171585]
モノトン活性化に対する $mathbfxmapstosigma(mathbfwcdotmathbfx)$ の関数について検討する。
学習者の目標は仮説ベクトル $mathbfw$ that $F(mathbbw)=C, epsilon$ を高い確率で出力することである。
論文 参考訳（メタデータ） (2022-06-17T17:55:43Z) - Permutation Compressors for Provably Faster Distributed Nonconvex
Optimization [68.8204255655161]
本稿では,Gorbunov et al (2021) の MARINA 法が,理論的な通信複雑性の観点から最先端の手法とみなすことができることを示す。
MARINAの理論は、古典的な独立圧縮機設定を超えて、潜在的にエミュレートされた圧縮機の理論を支持するものである。
論文 参考訳（メタデータ） (2021-10-07T09:38:15Z) - Tightening the Dependence on Horizon in the Sample Complexity of
Q-Learning [59.71676469100807]
この研究は、同期Q-ラーニングのサンプルの複雑さを、任意の$0varepsilon 1$に対して$frac|mathcalS| (1-gamma)4varepsilon2$の順序に絞る。
計算やストレージを余分に必要とせずに、高速なq-learningにマッチするvanilla q-learningの有効性を明らかにした。
論文 参考訳（メタデータ） (2021-02-12T14:22:05Z) - Learning elliptic partial differential equations with randomized linear
algebra [2.538209532048867]
ほぼ確実に収束する$G$への近似を構築することができることを示す。
0Gamma_epsilonleq 1$はトレーニングデータセットの品質を特徴付ける。
論文 参考訳（メタデータ） (2021-01-31T16:57:59Z) - Hardness of Learning Halfspaces with Massart Noise [56.98280399449707]
我々は、マッサート(有界)ノイズの存在下でPAC学習のハーフスペースの複雑さを研究します。
情報理論上最適なエラーとSQアルゴリズムで達成できる最高のエラーとの間に指数関数的なギャップがあることを示した。
論文 参考訳（メタデータ） (2020-12-17T16:43:11Z) - Statistical Query Lower Bounds for Tensor PCA [10.701091387118023]
Richard と Montanari が導入した PCA 問題では、$n$サンプル $mathbbEmathbfT_1:n$ of i.d. Perkins Gaussian tensors of order $k$ からなるデータセットが与えられ、$mathbbEmathbfT_1:n$ はランク 1 である。
目標は$mathbbE mathbfT_1$を見積もることである。
最適なサンプルの複雑さを鋭く分析する。
論文 参考訳（メタデータ） (2020-08-10T13:14:34Z) - Programming by Rewards [20.626369097817715]
我々は、性能、資源利用、あるいはベンチマーク上の正確性などの量的指標を最適化するための新しいアプローチである「報酬によるプログラミング」 (PBR) を定式化し、研究する。
PBR仕様は、(1)入力機能$x$と(2)報酬関数$r$で構成され、ブラックボックスコンポーネントとしてモデル化されている(実行しかできない)。
フレームワークは理論的に確立された -- 報酬が優れた特性を満たす場合において、合成されたコードは正確な意味で最適であることを示す。
論文 参考訳（メタデータ） (2020-07-14T05:49:14Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。