Program synthesis by sketching

By Rastislav Bodík, Armando Solar-Lezama. 2008

556 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Natural Language Processing

Citations in the corpus

Competition-level code generation with AlphaCode (2022, methodology): “Finally, sketch-based approaches (Solar-Lezama, 2008) that synthesize programs from a provided skeleton of the target program greatly reduce the search space.”
CodeGeeX: A Pre-Trained Model for Code Generation with Multilingual Benchmarking on HumanEval-X (2023, background): “From LISPbased pioneering deductive synthesis approaches [31, 37] tomodern program synthesis systems [23, 30], to end-to-end code generation via deep neural networks [19, 32, 33], tremendous efforts have been made to enable machines to automatically write correct programs as part of the quest to art”
DeepCoder: Learning to Write Programs (2016, methodology): “set. Note that this scheme has the deﬁciency of potentially re-exploring some parts of the search space several times, which could be avoided by a more sophisticated search procedure. Sketch. Sketch (Solar-Lezama, 2008) is a successful SMT-based program synthesis tool from the programming languages ”
A Compositional Object-Based Approach to Learning Physical Dynamics (2016, methodology): “This approach of starting with a general sketch of a program and ﬁlling in the speciﬁcs is inspired by ideas from the program synthesis community (Ellis et al., 2015; Gaunt et al., 2016; Solar-Lezama, 2008).”
Neuro-Symbolic Program Synthesis (2016, background): “ huge (potentially inﬁnite) and searching over it is a challenging problem. Several search techniques including enumerative (Udupa et al., 2013), stochastic (Schkufza et al., 2013), constraint-based (Solar-Lezama, 2008), and version-space algebra based algorithms (Gulwani et al., 2012) have been dev”
Learning to Represent Programs with Graphs (2017, methodology): “ code is complete and remains unmodiﬁed), as in Allamanis et al. (2014; 2015). 2 Published as a conference paper at ICLR 2018 Our work is remotely related to work on program synthesis using sketches (Solar-Lezama, 2008) and automated code transplantation (Barr et al., 2015). However, these approache”
TerpreT: A Probabilistic Programming Language for Program Induction (2016, methodology): “ are listed in Table 1: gradientdescent (thus any TerpreT model can be viewed as a diﬀerentiable interpreter), (integer) linear program (LP) relaxations, SMT, and the Sketch program synthesis system (Solar-Lezama, 2008). To allow all of these back-ends to be used regardless of the speciﬁed execution”
Coarse-to-Fine Decoding for Neural Semantic Parsing (2018, methodology): “The idea of using sketches as intermediate representations has also been explored in the field of program synthesis (Solar-Lezama, 2008; Zhang and Sun, 2013; Feng et al., 2017).”
Syntax-guided synthesis (2013, methodology): “Specifically, we have transcribed all the hacker’s delight and integer benchmarks into the input language of the Sketch synthesis system [24].”
CodeGeeX: A Pre-Trained Model for Code Generation with Multilingual Evaluations on HumanEval-X (2023, methodology): “From LISP-based pioneering deductive synthesis approaches (Waldinger and Lee, 1969; Summers, 1977) to modern program synthesis systems (Solar-Lezama, 2008; Polozov and Gulwani, 2015), to end-to-end code generation via deep neural networks (Mou et al.”
SQLizer: query synthesis from natural language (2017, methodology): “In particular, the use of the term sketch is inspired by the Sketch system [Solar Lezama 2008; Solar-Lezama et al. 2005, 2006] in which the user writes a program sketch containing holes (unknown expressions).”
Automated feedback generation for introductory programming assignments (2012, methodology): “.Veriﬁcation Phase 10: if (˙ i = null) .Veriﬁcation Succeeds 11: (minHole, minHoleValue) getMinHoleValue(˚) 12: ˚ p ˚ 13: i i [fencode(minHole <minHoleVal)g We extend the CEGIS algorithm in SKETCH [24] to get the CEGISMIN algorithm shown in Algorithm 1 for efﬁciently solving sketches that include”
FrAngel: component-based synthesis with control structures (2018, methodology): “A common synthesis technique, popularized by Sketch [Solar-Lezama 2008], is to provide the overall code context (a program sketch) while leaving łholesž to be filled by the synthesizer [Bodík et al. 2010; Feng et al. 2017a,b; Feser et al. 2015; Galenson et al. 2014; Raychev et al. 2014].”
In-IDE Code Generation from Natural Language: Promise and Challenges (2021, background): “Besides visual no-code or low-code programming interfaces, there has also been much progress on program synthesis [11, 28, 30, 105], which uses input-output examples, logic sketches, etc.”
Generative Code Modeling with Graphs (2018, methodology): “For example, program synthesis tools based on enumeration and deduction [8, 9, 18, 23] are successful at generating programs that satisfy some (usually incomplete) formal speciﬁcation but are often obviously wrong on manual inspection, as they cannot distinguish unlikely from likely, “natural”…”
Unsupervised Learning by Program Synthesis (2015, methodology): “We handle infinitely recursive grammars by bounding the depth of recursive calls to the Generate procedure, as in [7].”
FlashMeta: a framework for inductive program synthesis (2015, methodology): “In particular, the participants of the SyGuS-COMP 2014 competition employed: SMT-based search [13], enumerative search [37], sketching [35], and stochastic search [31].”
Efficient Synthesis with Probabilistic Constraints (2019, methodology): “Here we describe one constructive way of obtaining such sets of programs with finite VC dimension: we will consider sets of programs defined as program sketches [26] in the simple grammar from [1], where a program is written in a loop-free language, and “holes” defining the sketch replace some const”
Large Language Models Are Zero-Shot Fuzzers: Fuzzing Deep-Learning Libraries via Large Language Models (2022, background): “Traditional program synthesis techniques [50, 53, 63] typically restrict themselves to a small set of functionalities in the language and cannot deal with a large number of library APIs, each with their own specific input and output parameters and types.”