Sketch-Based Synthesis

The program skeleton is the concrete, user-written code that forms the fixed structure of the sketch. It defines control flow (e.g., loops, conditionals), function signatures, and data types. This skeleton provides critical constraints that drastically reduce the search space for the synthesizer, guiding it towards a syntactically and semantically plausible solution. For example, a skeleton for a sorting function would explicitly define the function name, parameters, and a loop structure, leaving only the comparison and swap logic as holes.

Holes (denoted by ?? or _ in tools like Sketch) are placeholders within the skeleton where code fragments must be synthesized. Each hole has an associated type (e.g., integer, boolean, list) and sometimes a grammar defining the set of allowed expressions. The synthesizer's core task is to find expressions of the correct type to fill these holes such that the complete program satisfies the specification. Holes can represent:

• Single expressions (e.g., a boolean condition ?? in an if statement).
• Sequences of statements.
• Entire function bodies.

The specification is the formal or semi-formal description of the program's required behavior. It acts as the correctness criterion for the synthesized code filling the holes. In sketch-based synthesis, specifications are often provided as:

• Assertions and Pre/Post-conditions: Logical constraints within the skeleton (e.g., assert(sorted(arr))).
• Reference Implementrations (oracles): A simpler, possibly inefficient, version of the function that defines correct behavior.
• Input-Output Examples: A set of concrete test cases the completed program must pass.
• Temporal Logic Formulas: For reactive systems, properties expressed in logics like LTL.

This component explicitly defines the set of possible code fragments that can be used to fill each hole. It is often specified via a context-free grammar or a set of component functions. For example, a hole for an integer expression might be constrained to the grammar: Expr := Constant | Variable | Expr + Expr | Expr * Expr. This constraint is critical for tractability; without it, the search space would be infinite. The grammar encodes domain knowledge, ensuring the synthesizer only explores relevant, efficient, or safe constructs.

The synthesis engine is the algorithmic core that searches for valid hole completions. It typically reduces the problem to a constraint satisfaction problem. The engine:

1. Encodes the skeleton, hole grammars, and specification into a system of logical constraints.
2. Uses a Satisfiability Modulo Theories (SMT) solver like Z3 to find a satisfying assignment for the holes.
3. Translates the solver's model back into concrete source code. This process often occurs within a Counterexample-Guided Inductive Synthesis (CEGIS) loop, where counterexamples from failed verification refine the constraints iteratively.

Syntax-Guided Synthesis (SyGuS) is the standardized formal framework that underlies most modern sketch-based synthesis tools. It explicitly separates the three key components:

• A grammar defining the search space (the 'Syntax' guide).
• A logical specification (typically in first-order logic).
• The synthesis engine that solves the SyGuS problem. Sketch-based synthesis is a powerful instantiation of the SyGuS paradigm, where the user-provided skeleton and holes implicitly define a tailored grammar for the problem at hand. The SyGuS format enables competition and innovation among different solver backends.

A program synthesis paradigm where the user provides a set of concrete input-output pairs as the specification. The synthesizer's goal is to infer a general program that correctly produces the given outputs for all provided inputs. This is highly user-friendly but can be ambiguous.

• Key Feature: Specification is purely demonstrative.
• Example: Microsoft Excel's FlashFill feature, which learns string transformations from a few cell examples.
• Contrast with Sketching: PBE provides no structural hints, while a sketch provides a partial program template.

A powerful algorithmic loop that combines inductive generalization with formal verification. It iteratively:

1. Synthesizes a candidate program consistent with current examples.
2. Verifies the candidate against a formal specification using a solver.
3. If verification fails, a counterexample (an input where the output is wrong) is extracted.
4. The counterexample is added to the set of examples, and the loop repeats.

This technique is foundational for correct-by-construction synthesis and is often used to fill the holes in a program sketch.

A standardized formal framework for program synthesis that defines the problem using two constraints:

• A context-free grammar (the Syn in SyGuS) that defines the space of allowed programs.
• A logical specification (often in first-order logic) that defines correctness.

The synthesizer must find a program from the grammar that satisfies the logical spec. This provides a rigorous, solver-friendly formulation. Sketch-based synthesis can be seen as a SyGuS problem where the sketch defines a specialized grammar with holes.

A hybrid architecture that combines the strengths of neural networks and symbolic reasoning.

• Neural Component: Learns from ambiguous, high-level specifications (e.g., natural language, noisy examples) to propose likely program structures or priors.
• Symbolic Component: Uses logical constraints, formal verification (e.g., SMT solvers), and search to ensure the generated program is semantically correct.

This approach is particularly effective for sketch-based synthesis, where a neural model might suggest initial sketches or rank potential completions, while symbolic methods guarantee final correctness.

A synthesis methodology that leverages rich type systems—such as refinement types or dependent types—to constrain the search space. The types act as a lightweight formal specification.

• Mechanism: The synthesizer uses type inference and hole-filling to construct a program that inhabits a given target type.
• Example: Given a type signature (x: {Int | x > 0}) -> {Int | result > x}, the synthesizer searches for a function that takes a positive integer and returns a larger integer.
• Relation to Sketching: Types can be seen as a form of sketch, specifying the "shape" of the code without the implementation details.

A specialized form of program synthesis focused on automatically fixing bugs in existing code. Given a faulty program and a specification (e.g., failing test cases), the repair engine synthesizes a minimal patch.

• Common Approach: Treats the buggy code as a sketch, where the buggy region is a "hole" to be replaced with a correct fragment.
• Techniques: Often uses CEGIS or constraint-solving to generate and validate candidate patches.
• Contrast: While general synthesis builds from scratch, repair modifies an existing, mostly correct artifact, making the search space more targeted.