Beyond Affine Loops: A Geometric Approach to Program Synthesis
summary
Claims it reduces loop synthesis to solving finite polynomial systems by computing a finite set of polynomial equations whose solutions enumerate all parameterized loops satisfying given polynomial invariants. Uses algebraic geometry (Gröbner/corner bases), implements construction in Macaulay2, and combines decomposition, homotopy continuation and SMT solving. Reports Z3 finds rational solutions on most benchmark instances when the constructed system is small; performance collapses when the number of monomials exceeds about six to seven. Results produce explicit parameter sets (s equals number of solutions).
AI-written summary · about
chapters (18)
- 0:00Program synthesis intro
- 1:04Synthesis in biology
- 2:08Polynomial invariants in loops
- 3:16Related work
- 4:21Our contribution
- 5:49Loop synthesis to invariants
- 7:16Finite basis for systems
- 8:21Invariant sets with Groebner
- 9:26Theorem: invariants and parameters
- 10:28Example: invariant set
- 11:38Challenges in rational solutions
- 11:59Symbolic methods
- 12:43Numerical methods
- 13:25SMT solvers
- 14:06Results and benchmarks
- 15:55Approach summary
- 16:36Future directions
- 17:25Q&A: Performance
related talks
21mExact Loop Bound Analysis
01h 05mVerifying Infinitely Many Programs at Once
22mProgram Synthesis for Artifacts beyond Programs
24mPolynomial-Time Program Equivalence for Machine Knitting
19mSynthesizing Specifications
52mThink Abstractly, Work Concretely
27mUnrealizability Logic
15mHieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical(…)