Just-in-Time Learning for Bottom-Up Enumerative Synthesis
summary
Builds a solver called Probe that uses just-in-time learning to update PCFG production costs from cheapest partial solutions and then runs guided bottom-up search that prunes by observational equivalence. Probe reduces a hard string problem from exploring ~30 million programs to about 130K programs, finds the remove-angles solution in 5 seconds where a traditional enumerator times out at 20 minutes, solves 48/82 SyGuS benchmarks vs 23/82 for Euphony within 10 minutes, and produces much smaller, better-generalizing programs than CVC4.
AI-written summary · about
chapters (15)
- 0:00Intro
- 0:28Syntax-Guided Program Synthesis (SyGuS)
- 2:15Traditional Program Synthesis Search strategy: explore programs in order of size
- 3:34Guided Program Synthesis: Challenges
- 4:40PROBE Overview
- 5:23Talk Outline
- 5:49Our Solution: Just-in-Time Learning
- 7:25Partial Solution Selection
- 8:54Unguided Search Techniques
- 11:56Experimental Setup: Baseline
- 12:08Synthesis Time (Probe VS Euphony)
- 12:58Synthesis Time (Probe VS CVC4)
- 13:42Solution Quality: Generalization Accuracy
- 14:56Solution Quality: Size of Solutions (CVCA)
- 15:23Evaluation Conclusion
related talks
14mGeneralizable Synthesis Through Unification
47mBig Ideas in Program Synthesis
26mData-Driven Lemma Synthesis for Interactive Proofs
24mAnswer Set Programming for Egg Extraction and More
17mSynthesizing MILP Constraints for Efficient and Robust Optimization
25mInductive Synthesis of Structurally Recursive Functional Programs from Non-recur...
18mActive Learning for Neurosymbolic Program Synthesis
38mProgram Synthesis: A Dream Realized?