Oriented Metrics for Bottom-Up Enumerative Synthesis
summary
Introduces an oriented metric that is asymmetric except at zero, lifts it from strings/bitvectors to programs, and uses it to prune (ball radius 100 in examples) and factorize the bottom-up search: a toy grammar goes from ~4,000 candidates at size 7 to ~900 after pruning and to 81 after metric-induced equivalence. Implements a generic solver called Merlin and reports concrete speedups (about 25× faster on bitvectors, ~75× vs Blaze, 42× vs baseline) with reusable artifacts.
AI-written summary · about
chapters (14)
- 0:00Oriented metrics for synthesis
- 1:06Syntax guided synthesis overview
- 3:36Bottom-up enumeration in practice
- 6:45Factorizing the search space
- 9:20Pruning with metrics
- 10:23Unifying equivalence and metrics
- 12:10Asymmetry in oriented metrics
- 16:16Metrics for operators
- 18:21Pruning programs with metrics
- 19:26Pruning and factorization
- 20:07Bottom-up synthesis framework
- 20:51Benchmark evaluation results
- 21:52Conclusion and future work
- 22:19Q&A
related talks
19mEnhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipu...
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)
17mEfficient Bottom-Up Synthesis for Programs with Local Variables
29mTowards Bottom-Up Enumeration in miniKanren via Pruning and Memoization
14mOne Down, 699 to Go: or, synthesising compositional desugarings
14mDataflow-Based Pruning for Speeding up Superoptimization
20mEquivalence by Canonicalization for Synthesis-Backed Refactoring
20mOptimal Program Synthesis via Abstract Interpretation