Component-based Synthesis of Table Consolidation and Transformation Tasks from Examples

Yu Feng; Ruben Martins; Jacob Van Geffen; Isil Dillig; Swarat Chaudhuri

Source-linked AI summary

Component-based Synthesis of Table Consolidation and Transformation Tasks from Examples

Yu Feng, Ruben Martins, Jacob Van Geffen, Isil Dillig, Swarat Chaudhuri

arXiv:1611.07502v1Nov 22, 2016cs.PL

TL;DR

Data preparation often requires substantial effort to convert raw data into usable tables, motivating automated table transformation from examples. The paper presents flexible component-based synthesis using SMT-based deduction and partial evaluation, and evaluates MORPHEUS on diverse real-world R tasks.

Problem
Data scientists spend over 80% of their time converting raw data into suitable forms, including consolidating, reshaping, and extending tables.
Method
The approach performs example-driven, component-based synthesis over extensible sets of first-order and higher-order combinators, using SMT-based deduction and partial evaluation to prune and guide search.
Results
MORPHEUS successfully synthesizes a diverse class of real-world data preparation programs from tasks drawn from online discussions among R users.
Takeaways & Limitations
The technique automates challenging table transformation tasks without relying on a fixed DSL or hard-coded component-specific reasoning.
Takeaways & Limitations
The formulation assumes table transformers take tables and first-order functions as arguments.

Abstract

from arXiv · show

This paper presents an example-driven synthesis technique for automating a large class of data preparation tasks that arise in data science. Given a set of input tables and an out- put table, our approach synthesizes a table transformation program that performs the desired task. Our approach is not restricted to a fixed set of DSL constructs and can synthesize programs from an arbitrary set of components, including higher-order combinators. At a high-level, our approach performs type-directed enumerative search over partial pro- grams but incorporates two key innovations that allow it to scale: First, our technique can utilize any first-order specification of the components and uses SMT-based deduction to reject partial programs. Second, our algorithm uses partial evaluation to increase the power of deduction and drive enumerative search. We have evaluated our synthesis algorithm on dozens of data preparation tasks obtained from on-line forums, and we show that our approach can automatically solve a large class of problems encountered by R users.

1. Introduction

The paper introduces a flexible, example-driven method for synthesizing table transformation programs from input-output tables using arbitrary components rather than a fixed DSL. SMT-based deduction and partial evaluation make type-directed search scalable, and MORPHEUS synthesizes diverse R data-preparation tasks.

Data preparation commonly requires consolidating, reshaping, or augmenting tables, yet data scientists spend over 80% of their time converting raw data into suitable forms.
The technique synthesizes table transformation programs from input tables and a desired output table, addressing limitations of narrowly defined DSL-based approaches.
Unlike fixed-DSL methods, the component-based approach supports extensible libraries and higher-order and first-order combinators for tidying, reshaping, consolidation, and computation.
SMT-based deduction rejects partial programs using arbitrary first-order component specifications without hard-coded component-specific reasoning.
Partial evaluation improves deduction by producing concrete subterm tables and drives search by finitizing constants such as selectable column names.
MORPHEUS separates sketch generation from completion, applies SMT-based deduction in both phases, and successfully synthesizes diverse R data-preparation programs.

2. Motivating Examples

The motivating examples show MORPHEUS synthesizing R programs for reshaping, consolidating, filtering, grouping, and computing over tables from user-provided examples. These tasks include both structural transformations and value-level computations.

The examples are drawn from Stackoverflow and illustrate the diversity of real-world data-preparation tasks addressed by MORPHEUS.
Example 1: Example 1 requires reshaping a data frame and appending cell contents to column names, which MORPHEUS can synthesize from the example.
Example 2: For each origin, Example 2 filters flights to Seattle, counts them, and computes their proportion among the filtered results.
The examples span table consolidation, reshaping, subset selection, grouping, and computation over selected data.
Example 3: MORPHEUS synthesizes a program that gathers and joins vehicle identifiers with speeds, filters absent vehicles, and orders the resulting records.

3. Problem Formulation

The paper formalizes synthesis as inferring a well-typed program that transforms input tables into a specified output using a component library. Its model distinguishes table transformers from first-order value transformers and represents tables with typed columns and cells.

A table is modeled by row and column counts, a column-to-type mapping, and a cell-value mapping.
Components contain a name, type signature, and first-order formula describing an overapproximation of their input-output behavior.
The formal problem specification pairs an input-output example with the available component set.
The component library combines higher-order table transformers with first-order value transformers.Table transformers change table shape and may accept first-order functions as arguments; value transformers operate as first-order operators.
The synthesis problem is to infer a well-typed expression over components whose execution on the input tables equals the output table.

4. Hypotheses as Refinement Trees

The synthesis search represents partial programs as hypotheses organized in refinement trees, then separates table-structure choices from first-order expression completion. Partial evaluation maps complete hypotheses to concrete tables and preserves holes in incomplete ones.

A hypothesis is a partial program containing typed unknown expressions that can be constructed using table-transformation components.
Refinement replaces a typed hole with a more specific component application, making the hypothesis more constrained.
Refinement trees encode both the hypothesis abstract syntax tree and the history of refinements during search.
Sketches: A sketch fixes the table transformers and qualifies every table-typed leaf with an input table, leaving first-order arguments unresolved.
Complete programs: A complete program assigns qualifiers to all leaves and therefore fully specifies the expressions represented by the hypothesis.
Partial evaluation: Partial evaluation produces a concrete table for a complete program, but retains question marks when the hypothesis remains incomplete.

5. Synthesis Algorithm

The synthesis algorithm searches a priority queue of hypotheses, using deduction to convert or reject them and refinement to expand survivors. Candidate sketches are completed with first-order expressions and checked against the input-output example before being returned.

When deduction refutes a hypothesis, the algorithm discards it and adds its one-level table-transformer refinements to the worklist.
The procedure returns a complete program satisfying the example or ⊥ when no such program exists.
SYNTHESIZE starts with a maximally general table-typed hypothesis and iteratively processes hypotheses from a priority queue.
The deduction procedure tests whether a hypothesis can be converted into a sketch by assigning table holes to input variables.
For a candidate sketch, FILLSKETCH generates complete programs, which are returned only after CHECK verifies the input-output example.

6. SMT-based Deduction

SMT-based deduction converts component specifications into constraints and rejects hypotheses that cannot satisfy the input-output example. This reasoning applies to components with first-order specifications and can use partial evaluation to expose additional contradictions.

Constraint-based deduction: Component specifications may overapproximate behavior and can describe relationships such as the number of rows and columns in input and output tables.The sample specifications for library methods need not fully capture component behavior.
Constraint generation: The overall hypothesis specification is recursively derived from sub-hypotheses, with complete programs abstracted into constraints over their concrete tables.Leaf holes without available information receive the specification true.
Constraint-based deduction: DEDUCE returns ⊥ when a hypothesis cannot become a program satisfying the input-output examples by replacing its holes with inputs.Unsatisfiability indicates that the hypothesis cannot be unified with the example.
Constraint-based deduction: The deduction procedure generates an SMT formula from a hypothesis, its component specifications, and the input-output example, then rejects the hypothesis when the formula is unsatisfiable.The constraints connect hypothesis leaves to input tables and the root to the output table.
Worked example: In the worked example, the constraint requires the output to have fewer columns than the input, conflicting with equal concrete column counts, so the hypothesis is rejected.The contradiction is y.col < x1.col together with x1.col = y.col.

7. Sketch Completion

Sketch completion fills table-transformer sketches by first synthesizing table arguments and then enumerating table-dependent first-order functions. Partial evaluation supplies concrete tables that constrain later synthesis and enable early rejection.

Sketch completion: The completion algorithm synthesizes table-typed arguments bottom-up before other arguments because later first-order-function vocabularies depend on the resulting table schemas.Concrete intermediate tables determine which columns and constants can be used.
Table-driven type inhabitation: Sketch completion enumerates well-typed inhabitants with respect to a concrete table, making the available constants and column names table-dependent.This process is called table-driven type inhabitation.
Type inhabitation rules: Type inhabitation uses variables, tuples, component applications, and lambdas to construct well-typed first-order terms, including predicates such as x ≥10.Lambda abstraction is required because table transformers may be higher-order.
Sketch completion: After each completion, deduction checks the partially filled sketch, allowing partial evaluation to produce concrete tables and reject inconsistent candidates before all holes are filled.This is the key interaction between sketch completion and deduction.
Worked example: In the example, the predicate age > 12 is rejected before the remaining projection hole is filled because partial evaluation makes the resulting constraint unsatisfiable.The evaluated intermediate table contributes the final row and column constraints.

8. Implementation

MORPHEUS implements synthesis in C++ using Z3 for SMT satisfiability, a statistical cost model for prioritizing hypotheses, and parallel search across program sizes.

System implementation: MORPHEUS is implemented in C++ and uses the Z3 SMT solver with Linear Integer Arithmetic to check generated constraints.Z3 provides the satisfiability checks used by the deduction engine.
Hypothesis prioritization: A 2-gram model trained from existing code snippets assigns scores to hypotheses, which are then ordered in the worklist.Components from ΛT are represented as words in code-sentence representations.
Parallel search: MORPHEUS uses multiple threads to search for solutions of different sizes and terminates when any thread finds a correct solution.This strategy addresses the cost of exploring many smaller programs before a large correct hypothesis.

9. Evaluation

The evaluation tests MORPHEUS on 80 Stack Overflow data-preparation benchmarks, measuring automation success, scalability contributions, task complexity, and comparisons with existing synthesizers.

Evaluation setup: 80 Stack Overflow benchmarks evaluate MORPHEUS using input-output examples and components from the tidyr and dplyr R libraries.The experiments also use ten value-transformation components, including comparisons and aggregate functions.
Performance: 97.5% of benchmarks are synthesized within five minutes, with a 3.59-second median running time and 86.3% solved within 60 seconds.MORPHEUS solves 78 of 80 benchmarks and times out on two.
Impact of deduction: Deduction reduces the median running time from 95.53 seconds without deduction to 8.57 seconds with Spec 1, which solves 68 of 80 benchmarks.The no-deduction version times out on 32.5% of benchmarks, while even coarse specifications improve synthesis substantially.
Impact of partial evaluation: Partial evaluation lets MORPHEUS prune 72% of partial programs and improves both running time and the number of solved benchmarks.Without partial evaluation, Spec 1 solves 62 benchmarks and Spec 2 solves 64, with median times of 34.75 and 17.07 seconds respectively.
Benchmark complexity: In a user study, participants solved two of five representative tasks correctly on average, suggesting the benchmarks challenge proficient R programmers and expert data analysts.The average participant completed three tasks within one hour, but only two were correct.
Comparison with existing tools: MORPHEUS solves 96.4% of 28 SQL benchmarks in a one-second median, whereas SQLSYNTHESIZER solves 71.4% in 11 seconds.On the broader 80-benchmark set, SQLSYNTHESIZER solves only one benchmark, while λ2 solves none.

10. Related Work

The paper situates MORPHEUS among program-by-example, data-wrangling, deduction-based, component-based, and type-inhabitation approaches, distinguishing its general component-based synthesis and SMT-pruning strategy.

Programming by example: Earlier table-transformation synthesizers target narrower domains such as spreadsheet macros or SQL, whereas MORPHEUS addresses a broader class of table transformations.Related systems also include specialized extraction tools and synthesis methods for particular table languages.
Data wrangling: Wrangler and OpenRefine support broader data-wrangling tasks than MORPHEUS but do not automatically synthesize table transformations from examples.The comparison distinguishes interactive or framework-based transformation support from example-driven synthesis.
Deduction and search: Unlike prior deduction systems tied to fixed DSL constructs, MORPHEUS applies SMT-based deduction to components equipped with first-order specifications.Its search enumerates one satisfying program while using deduction to reject partial programs.
Component-based synthesis: MORPHEUS uses an SMT solver as a pruning tool in enumerative search rather than requiring precise component specifications for SMT-based synthesis.This contrasts with component-synthesis efforts that use SMT solving to search directly for component compositions.
Type inhabitation and sketching: MORPHEUS treats sketch completion as type inhabitation while using table contents to finitely restrict the inhabitants considered.Its sketches permit arbitrary expressions over first-order components, unlike sketches whose holes typically correspond to constants.

11. Conclusion

The paper concludes that MORPHEUS flexibly synthesizes many data-preparation transformations from arbitrary combinators and scales through SMT-based deduction and partial evaluation.

Conclusion: MORPHEUS automates challenging table-transformation tasks that commonly arise in data science and are difficult even for proficient R programmers.The conclusion attributes the tool’s demonstrated practicality to the experimental evaluation.
Conclusion: The synthesis algorithm accepts arbitrary combinators and corresponding specifications, providing flexibility beyond a fixed component set.Its scalability relies on SMT-based deduction and partial evaluation.

Appendix A: Specifications of high-order components

The appendix explains component specifications that constrain table-shape properties and shows how more precise constraints let MORPHEUS reject an incorrect hypothesis before completion.

Specifications: Spec 1 constrains only relationships between a table’s row and column counts, using T.row and T.col as table dimensions.These coarse constraints may leave incorrect hypotheses satisfiable.
Specifications: Spec 2 adds cardinality and group information, including new column names, new values, and the number of groups.T.newVals counts both new column names and cell values relative to the input table.
Example properties: For the example transformation, input and output column-name and value sets provide the quantities used to compute new-column and new-value cardinalities.The output’s group count is represented by a fresh variable k because zero or more group-by operators may precede it.
Deductive pruning: Spec 1 leaves an incorrect hypothesis satisfiable, so MORPHEUS continues exploring completions that cannot produce the desired solution.The example constraint ψ is satisfiable despite the hypothesis being incorrect.
Deductive pruning: Spec 2 makes the corresponding constraint unsatisfiable, allowing deduction to reject the incorrect hypothesis without completing it.The additional conjuncts involving new columns and new values cause the contradiction.