Efficient Bottom-Up Synthesis for Programs with Local Variables
summary
Introduces lifted interpretation, an algorithm that evaluates all grammar programs simultaneously to enumerate binding contexts and collapse equivalent subprograms with local variables. Implements the idea in the web-automation tool Arborist, using trace semantics to build context→output equivalence classes for loops and lambdas. On 131 real-world benchmarks Arborist solves 93.9% and outperforms WebRobot and Helena, handling a broader set of tasks and running up to six times faster on the harder benchmarks.
AI-written summary · about
chapters (7)
- 0:00Program synthesis intro
- 1:05Bottom-up synthesis challenges
- 3:16Lifted interpretation
- 6:50Web automation via lifted
- 11:11Evaluation on benchmarks
- 12:42Key takeaways
- 13:23Q&A
related talks
25mBottom-Up Synthesis of Recursive Functional Programs using Angelic Execution
21mSynthesizing Formal Semantics from Executable Interpreters
19mAn Incremental Algorithm for Algebraic Program Analysis
29mGrammar Inference for Ad Hoc Parsers
28mOriented Metrics for Bottom-Up Enumerative Synthesis
20mPartial Evaluation, Whole-Program Compilation
51mSynthesis and Verification for All
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)