一句话：提出用代数几何定理将基于模板的多项式程序合成直接归约为二次规划，避免量词消去并保持半完备性。
本文研究含实变量、赋值/条件/卫式为多项式的命令式程序的基于模板合成（sketching）。该问题可归约到一阶实数理论并声全完备求解，但所得公式含量词交替，现代 SMT 求解器极难处理，经典量词消去也不可扩展。作者基于多面体与实代数几何中的 Putinar Positivstellensatz、Real Nullstellensatz、Handelman 定理和 Farkas 引理，提出绕过量词消去、直接将合成问题归约为二次规划（QP）的算法；也可视为对合成中特定公式的高效量词消去。该归约声且半完备，模板多项式次数足够高时完备。实验在文献中的多组示例上验证了方法的可扩展性。
Template-based synthesis, also known as sketching, is a localized approach to program synthesis in which the programmer provides not only a specification, but also a high-level "sketch" of the program. The sketch is basically a partial program that models the general intuition of the programmer, while leaving the low-level details as unimplemented "holes". The role of the synthesis engine is then to fill in these holes such that the completed program satisfies the desired specification. In this work, we focus on template-based synthesis of polynomial imperative programs with real variables, i.e. imperative programs in which all expressions appearing in assignments, conditions and guards are polynomials over program variables. While this problem can be solved in a sound and complete manner by a reduction to the first-order theory of the reals, the resulting formulas will contain a quantifier alternation and are extremely hard for modern SMT solvers, even when considering toy programs with a handful of lines. Moreover, the classical algorithms for quantifier elimination are notoriously unscalable and not at all applicable to this use-case.In contrast, our main contribution is an algorithm, based on several well-known theorems in polyhedral and real algebraic geometry, namely Putinar's Positivstellensatz, the Real Nullstellensatz, Handelman's Theorem and Farkas' Lemma, which sidesteps the quantifier elimination difficulty and reduces the problem directly to Quadratic Programming (QP). Alternatively, one can view our algorithm as an efficient way of eliminating quantifiers in the particular formulas that appear in the synthesis problem. The resulting QP instances can then be handled quite easily by SMT solvers. Notably, our reduction to QP is sound and semi-complete, i.e. it is complete if polynomials of a sufficiently high degree are used in the templates. Thus, we provide the first method for sketching-based synthesis of polynomial programs that does not sacrifice completeness, while being scalable enough to handle meaningful programs. Finally, we provide experimental results over a variety of examples from the literature.
@article{paperbot2020,
title = {Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial Programs},
author = {Amir Kafshdar Goharshady and S. Hitarth and Fatemeh Mohammadi and Harshit Jitendra Motwani},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA1},
year = {2023},
doi = {10.1145/3586052}
}