Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial Program...
summary
Algorithm reduces template-based synthesis of polynomial imperative programs to Quadratic Programming by applying Farkas, Handelman, Putinar (SOS) and the Real Nullstellensatz, producing existential QP-style constraints over coefficient symbols; sound and sound and semi-complete (completeness as degree bound increases). Implementation reduces synthesis to QP via SOS/PSD matrix templates and hands off QP to SMT/QFN solvers; artifacts and code are available. Scales to benchmarks of roughly up to ~20-line programs in their DSL, fails on non-polynomial features (mod, ints, lists) and does not synthesize termination proofs unless ranking functions are added.
AI-written summary · about
chapters (11)
- 0:00Polynomial program synthesis intro
- 1:24Program templates and transitions
- 2:46Sketch to logical constraints
- 4:08Quantifier alternation elimination
- 6:13Nonlinear constraints via monoid
- 8:40Sum of squares and quadratics
- 11:34Algorithm implementation
- 12:59Experimental results
- 14:01Limitations and termination
- 15:25Scalability and SMT challenges
- 16:51Q&A on bilinear constraints
related talks
20mOptimal Program Synthesis via Abstract Interpretation
47mBig Ideas in Program Synthesis
38mProgram Synthesis: A Dream Realized?
25mRecursive Program Synthesis using Paramorphisms
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)
17mSynthesizing MILP Constraints for Efficient and Robust Optimization
23mGenerating Programs for Polynomial Multiplication with Correctness Assurance
15mGauss: Program Synthesis by Reasoning Over Graphs