使用 Stellensätze 的基于模板的程序综合
Template-based Program Synthesis using Stellensätze
AI总结：
针对含实变量的多项式命令式程序模板综合，本文借助 Putinar Positivstellensatz 等实代数几何定理将含量词交替问题归约为 QP，提出可靠且半完备的高效综合算法。
摘要：
基于模板的综合（也称为 sketching）是一种局部化的程序综合方法，其中程序员不仅提供规约，还提供程序的高层“草图”。该草图本质上是一个部分程序，用于建模程序员的总体直觉，同时将低层细节留作未实现的“洞”。综合引擎的作用就是填补这些洞，使完成后的程序满足所需规约。在本文中，我们关注带实变量的多项式命令式程序的基于模板的综合，即所有出现在赋值、条件和守卫中的表达式都是程序变量上多项式的命令式程序。虽然该问题可以通过归约到实数一阶理论而以可靠且完备的方式求解，但所得公式包含量词交替，对于现代 SMT 求解器极其困难，即使考虑只有寥寥数行的玩具程序也是如此。此外，经典的量词消去算法众所周知不可扩展，完全不适用于此用例。相比之下，我们的主要贡献是一种基于多面体与实代数几何中若干著名定理的算法，即 Putinar 的 Positivstellensatz、Real Nullstellensatz、Handelman 定理和 Farkas 引理；该算法避开量词消去困难，并将问题直接归约为二次规划（QP）。或者，也可以将我们的算法视为对综合问题中出现的特定公式进行量词消去的一种高效方式。所得 QP 实例随后可由 SMT 求解器相当轻松地处理。值得注意的是，我们到 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...
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
