Program Synthesis as Dependency Quantified Formula Modulo Theory

• URL: http://arxiv.org/abs/2105.09221v1
• Date: Wed, 19 May 2021 16:05:20 GMT
• Title: Program Synthesis as Dependency Quantified Formula Modulo Theory
• Authors: Priyanka Golia, Subhajit Roy, and Kuldeep S. Meel
• Abstract summary: This paper investigates the feasibility of synthesis techniques without grammar. We show that $mathbbT$-constrained synthesis can be reduced to DQF($mathbbT$), i.e., to the problem of finding a witness of a Dependency Quantified Formula Modulo Theory.
• Score: 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.

Related papers

• Eliciting Fine-Tuned Transformer Capabilities via Inference-Time Techniques [1.14219428942199]
  Large language models have transformed natural language processing, yet supervised fine-tuning (SFT) remains computationally intensive.<n>This paper formally proves that capabilities acquired through SFT can be approximated by a base transformer model.<n>We extend these results to practical scenarios with finite context lengths and partial dataset access.
  arXiv  Detail & Related papers  (2025-06-09T08:37:19Z)
• Neural network learns low-dimensional polynomials with SGD near the information-theoretic limit [75.4661041626338]
  We study the problem of gradient descent learning of a single-index target function $f_*(boldsymbolx) = textstylesigma_*left(langleboldsymbolx,boldsymbolthetarangleright)$ under isotropic Gaussian data. We prove that a two-layer neural network optimized by an SGD-based algorithm learns $f_*$ of arbitrary link function with a sample and runtime complexity of $n asymp T asymp C(q) cdot d
  arXiv  Detail & Related papers  (2024-06-03T17:56:58Z)
• Matching the Statistical Query Lower Bound for $k$-Sparse Parity Problems with Sign Stochastic Gradient Descent [83.85536329832722]
  We solve the $k$-sparse parity problem with sign gradient descent (SGD) on two-layer fully-connected neural networks. We show that this approach can efficiently solve the $k$-sparse parity problem on a $d$-dimensional hypercube. We then demonstrate how a trained neural network with sign SGD can effectively approximate this good network, solving the $k$-parity problem with small statistical errors.
  arXiv  Detail & Related papers  (2024-04-18T17:57:53Z)
• Horizon-Free and Variance-Dependent Reinforcement Learning for Latent Markov Decision Processes [62.90204655228324]
  We study regret minimization for reinforcement learning (RL) in Latent Markov Decision Processes (LMDPs) with context in hindsight. We design a novel model-based algorithmic framework which can be instantiated with both a model-optimistic and a value-optimistic solver.
  arXiv  Detail & Related papers  (2022-10-20T21:32:01Z)
• SQ Lower Bounds for Learning Single Neurons with Massart Noise [40.1662767099183]
  PAC learning a single neuron in the presence of Massart noise. We prove that no efficient SQ algorithm can approximate the optimal error within any constant factor.
  arXiv  Detail & Related papers  (2022-10-18T15:58:00Z)
• Learning a Single Neuron with Adversarial Label Noise via Gradient Descent [50.659479930171585]
  We study a function of the form $mathbfxmapstosigma(mathbfwcdotmathbfx)$ for monotone activations. The goal of the learner is to output a hypothesis vector $mathbfw$ that $F(mathbbw)=C, epsilon$ with high probability.
  arXiv  Detail & Related papers  (2022-06-17T17:55:43Z)
• Permutation Compressors for Provably Faster Distributed Nonconvex Optimization [68.8204255655161]
  We show that the MARINA method of Gorbunov et al (2021) can be considered as a state-of-the-art method in terms of theoretical communication complexity. Theory of MARINA to support the theory of potentially em correlated compressors, extends to the method beyond the classical independent compressors setting.
  arXiv  Detail & Related papers  (2021-10-07T09:38:15Z)
• Tightening the Dependence on Horizon in the Sample Complexity of Q-Learning [59.71676469100807]
  This work sharpens the sample complexity of synchronous Q-learning to an order of $frac|mathcalS|| (1-gamma)4varepsilon2$ for any $0varepsilon 1$. Our finding unveils the effectiveness of vanilla Q-learning, which matches that of speedy Q-learning without requiring extra computation and storage.
  arXiv  Detail & Related papers  (2021-02-12T14:22:05Z)
• Learning elliptic partial differential equations with randomized linear algebra [2.538209532048867]
  We show that one can construct an approximant to $G$ that converges almost surely. The quantity $0Gamma_epsilonleq 1$ characterizes the quality of the training dataset.
  arXiv  Detail & Related papers  (2021-01-31T16:57:59Z)
• Hardness of Learning Halfspaces with Massart Noise [56.98280399449707]
  We study the complexity of PAC learning halfspaces in the presence of Massart (bounded) noise. We show that there an exponential gap between the information-theoretically optimal error and the best error that can be achieved by a SQ algorithm.
  arXiv  Detail & Related papers  (2020-12-17T16:43:11Z)
• Statistical Query Lower Bounds for Tensor PCA [10.701091387118023]
  In the PCA problem introduced by Richard and Montanari, one is given a dataset consisting of $n$ samples $mathbbEmathbfT_1:n$ of i.i.d. Perkins Gaussian tensors of order $k$ with the promise that $mathbbEmathbfT_1:n$ is a rank-1. The goal is to estimate $mathbbE mathbfT_1$, but no time estimator is known. We provide a sharp analysis of the optimal sample complexity
  arXiv  Detail & Related papers  (2020-08-10T13:14:34Z)
• Programming by Rewards [20.626369097817715]
  We formalize and study programming by rewards'' (PBR), a new approach for optimizing some quantitative metric such as performance, resource utilization, or correctness over a benchmark. A PBR specification consists of (1) input features $x$, and (2) a reward function $r$, modeled as a black-box component (which we can only run) We show that the framework is theoretically-founded ---in cases when the rewards satisfy nice properties, the synthesized code is optimal in a precise sense.
  arXiv  Detail & Related papers  (2020-07-14T05:49:14Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.