Inductive Synthesis of Structurally Recursive Functional Programs from Non-recur...
summary
Synthesizes structurally recursive ML-style functions from input-output examples by first enumerating all nonrecursive straight-line expressions per example and then top-down searching recursive programs while pruning any candidate inconsistent with those blocks. Uses block-based pruning and a compact version space graph to represent billions of blocks (claims >1e9 blocks in ~0.1s), plus library sampling to invert library calls. Implements Trio, proves completeness (won’t miss a solution eventually), and reports solving 98%+ of benchmarks (60 prior+new tasks) and outperforming prior tools.
AI-written summary · about
chapters (16)
- 0:00Intro
- 0:45Recursive Functional Synthesis
- 1:52Two Strategies
- 3:19Major Hurdle: Recursion
- 5:38Our Key Idea: Two Phased Synthesis
- 6:18Step 1: Synthesizing Blocks
- 7:20Step 2: Top-Down Search w/ Block-based Pruning (1/4)
- 9:55Challenges
- 11:06Key to Scalability 2: Version Spaces
- 13:05Bottom-Up Enumerator
- 13:32Library Sampling: Generation of Inverse Maps (1/2)
- 14:50Block Generator
- 17:19Candidate Generator
- 17:55Version Space Matching
- 19:48Evaluation
- 20:55In the Paper...
related talks
47mBig Ideas in Program Synthesis
38mProgram Synthesis: A Dream Realized?
40mType-Driven Program Synthesis
01h 10mNeurosymbolic Program Synthesis: Bridging Perception and Reasoning in Real-World(…)
46mCorecursion, Codata, and Just a Little Combinatorial Game Theory
16mJust-in-Time Learning for Bottom-Up Enumerative Synthesis
15mGauss: Program Synthesis by Reasoning Over Graphs
17mProgrammatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Progr...