Program Synthesis Using Example Propagation
summary
Scrybe is an example-based synthesizer for a statically typed functional language that combines top-down deductive search (λ2 style) with Smyth-style live bidirectional evaluation and type propagation and example propagation through sketches to prune the search. It treats any imported function given by a structural-recursive definition as usable during synthesis, uses normalization and weighted search to avoid bad branches, and on the combined λ2+Myth benchmarks synthesizes most tasks while showing about a 5x speedup versus the same synthesizer without example propagation.
AI-written summary · about
chapters (6)
- 0:00Introduction
- 4:03Same spec, different impls
- 7:40Constraint propagation
- 11:53Example propagation
- 13:36Scribe implementation
- 17:32Q&A
related talks
31mLetting users do the undecidable: lessons from program synthesis
32mHole Refinements for Polymorphic Type-and-Example Driven Synthesis
25mRecursive Program Synthesis using Paramorphisms
18mMobius: Synthesizing Relational Queries with Recursive and Invented Predicates
19mEnhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipu...
31mSynthesizing Evidence of Emergent Computation
21mSynthesizing Formal Semantics from Executable Interpreters
15mLanguage-Parametric Reference Synthesis