Generalizable Synthesis Through Unification
summary
Defines an Occam solver with PAC-style guarantees and proves Eusolver fails that criterion, then builds PolyGen, an Occam STUN solver that decomposes CLIA synthesis into disjunctive synthesis problems, decision lists, and per-term domain-solver calls with randomized example sampling. PolyGen synthesizes the three-way max example with 10 examples (Eusolver needs ~400, CVC4 times out at 500), is instantiated on 100 SyGuS CLIA tasks, and outperforms Eusolver and Euphony on both generalizability and runtime.
AI-written summary · about
chapters (15)
- 0:00Intro
- 0:22Programming by Example (PBE)
- 1:47Research Status on Generalizability
- 3:04Our Contribution
- 3:46Occam Learning on Program Synthesis
- 4:58Synthesis through Unification (STUN)
- 5:45Eusolver
- 8:58STUN and Occam Solver
- 9:49Term Solver in PolyGen
- 10:36Disjunctive Synthesis
- 11:03Unifier in PolyGen
- 12:13Evaluation Setup
- 13:00Results on the Generalizability
- 13:23Results on the Efficiency
- 13:35Summary
related talks
16mJust-in-Time Learning for Bottom-Up Enumerative Synthesis
47mBig Ideas in Program Synthesis
38mProgram Synthesis: A Dream Realized?
17mExplainable Program Synthesis by Localizing Specifications
17mModeling Black-Box Components with Probabilistic Synthesis
17mSynthesizing MILP Constraints for Efficient and Robust Optimization
20mFunction synthesis for maximizing model counting
29mSyntia: Synthesizing the Semantics of Obfuscated Code