Template-based Program Synthesis using Stellensätze
基于模板的程序合成方法——使用 Stellensätze

1 INTRODUCTION  1 引言

@real: \(i, s, n\);
@pre: \(n \geq 1\);
\(i=0\);
\(s=0\);
@invariant: \([[\{\overline{i, s}\}, \overline{2}]] \geq 0 \wedge[[\{\overline{i, s}\}, \overline{2}]] \geq 0 \wedge[[\{\bar{i}, \bar{n}\}, \overline{1}]] \geq 0\)
while( \([\{\underline{i}, \underline{n}\}, 1]]\) )
\{
    \(i=i+1\);
    \(s=[[\{\underline{i}, \underline{s}\}, 1]] ;\)
\}
@post: \((n-1) \cdot n / 2 \leq s \leq n \cdot(n+1) / 2\);

@real: \(i, s, n\);
@pre: \(n \geq 1\);
\(i=0\);
\(s=0\);
@invariant: \(s \geq i \cdot(i+1) / 2 \wedge s \leq i \cdot(i+1) / 2 \wedge i \leq n\)
while \((i \leq n-1)\)
\{
    \(i=i+1\);
    \(s=s+i\);
\}
@post: \((n-1) \cdot n / 2 \leq s \leq n \cdot(n+1) / 2\);

• Complexity: We prove that the problem is decidable. This is achieved by a reduction to the first-order theory of the reals. We also provide a reduction showing that our problem is (strongly) NP-hard. Note that, as mentioned above, decision procedures for the first-order theory of the reals are notoriously slow and cannot handle even toy programs in practice.
  复杂性：我们证明了该问题是可判定的。这是通过归约到实数的一阶理论来实现的。我们还提供了一个归约，表明我们的问题是（强）NP-难的。需要注意的是，如上所述，实数一阶理论的判定程序众所周知非常缓慢，实际上甚至无法处理简单的程序。
• Practical Algorithm: We use classical theorems from polyhedral and real algebraic geometry, including Farkas’ Lemma, Handelman’s Theorem, Putinar’s Positivstellensatz ${}^1$${}^1$^(1){ }^{1}, and the Real Nullstellensatz ${}^2$${}^2$^(2){ }^{2} to obtain a polynomial-time reduction to Quadratic Programming (QP). Since modern solvers, both SMT solvers and numerical ones, are quite efficient in handling real-world QP instances, this leads to a much more scalable approach to program synthesis in comparison to decision procedures for the first-order theory of the reals.
  实用算法：我们利用多面体和实代数几何中的经典定理，包括法尔卡斯引理（Farkas’ Lemma）、汉德尔曼定理（Handelman’s Theorem）、普蒂纳正性定理（Putinar’s Positivstellensatz ${}^1$${}^1$^(1){ }^{1} ）以及实数零点定理（Real Nullstellensatz ${}^2$${}^2$^(2){ }^{2} ），将问题多项式时间归约到二次规划（QP）。由于现代求解器，无论是 SMT 求解器还是数值求解器，在处理实际的二次规划实例时都非常高效，这使得该方法相比实数一阶理论的判定程序，在程序综合方面具有更好的可扩展性。
• Completeness: Crucially, we prove that our approach is not only sound but also semi-complete, i.e. it is complete as long as polynomials of sufficiently high degree are used in the templates. So, our approach achieves both soundness and completeness, while not suffering from the unscalability of quantifier elimination and decision procedures for the first-order theory of the reals.
  完备性：关键是，我们证明了我们的方法不仅是正确的，而且是半完备的，即只要在模板中使用足够高次数的多项式，它就是完备的。因此，我们的方法既实现了正确性又实现了完备性，同时避免了实数一阶理论的量词消除和判定过程的不具扩展性问题。
• Experimental Results: We provide extensive experimental results, illustrating the efficiency of our approach and that it can successfully handle a variety of programs.
  实验结果：我们提供了大量实验结果，展示了我们方法的高效性以及其成功处理各种程序的能力。

• Template-based Synthesis: The work [Srivastava et al. 2013] provides algorithms based on Farkas’ Lemma for template-based synthesis of linear/affine programs. Since our work can handle polynomial programs of arbitrary degree, [Srivastava et al. 2013]‘s results on linear/affine programs are subsumed by our approach. Moreover, while the use of Farkas’ Lemma is shared among the two approaches, we also use theorems from real algebraic geometry, e.g. Handelman and Putinar, as well as non-trivial combinations of them, which are not considered in [Srivastava et al. 2013]. So, we have a different methodology and handle a wider family of programs. To the best of our knowledge, our algebro-geometric approach is novel in program synthesis.
  基于模板的综合：文献[Srivastava et al. 2013]提出了基于 Farkas 引理的线性/仿射程序模板综合算法。由于我们的工作能够处理任意次数的多项式程序，[Srivastava et al. 2013]关于线性/仿射程序的结果被我们的方法所涵盖。此外，尽管两种方法都使用了 Farkas 引理，我们还使用了实代数几何中的定理，例如 Handelman 和 Putinar 定理，以及它们的非平凡组合，而这些在[Srivastava et al. 2013]中未被考虑。因此，我们采用了不同的方法论，并处理了更广泛的程序类别。据我们所知，我们的代数几何方法在程序综合领域是创新的。
• Invariant Generation: The work [Chatterjee et al. 2020b] provides template-based algorithms for automated generation of polynomial invariants over polynomial programs with real variables. Note that this is also a special case of our setting, in which the holes are limited to appear only in the invariants. Since we allow holes in both the program itself and the invariants, our setting is strictly more general. Moreover, while [Chatterjee et al. 2020b] also uses Positivstellensätze, it does not consider Nullstellensätze, and thus has a different mathematical basis. The work [Sankaranarayanan et al. 2004b] considers the same problem
  不变式生成：[Chatterjee et al. 2020b] 提供了基于模板的算法，用于自动生成带有实变量的多项式程序上的多项式不变式。注意，这也是我们设定的一个特例，其中空洞仅限于出现在不变式中。由于我们允许空洞同时出现在程序本身和不变式中，因此我们的设定更为通用。此外，虽然 [Chatterjee et al. 2020b] 也使用了 Positivstellensätze，但它没有考虑 Nullstellensätze，因此其数学基础不同。[Sankaranarayanan et al. 2004b] 的工作考虑了相同的问题。

• Termination analysis: Template-based algorithms that utilize Farkas’ Lemma or Positivstellensätze have also been considered in the context of termination and reachability analysis [Agrawal et al. 2017; Asadi et al. 2021; Chatterjee et al. 2016, 2020a; Neumann et al. 2020; Takisaka et al. 2018]. However, this is a very different and orthogonal problem and, while there are clear similarities in the approaches, it is not possible to directly or experimentally compare them. Conceptually, the works in termination analysis assume that strong-enough invariants are given as part of the input ${}^3$${}^3$^(3){ }^{3} and then reduce the problem of finding an affine/polynomial ranking function, or its probabilistic counterparts, to Linear Programming (LP). This is in contrast to our setting where the reduction is to Quadratic Programming (QP) and a reduction to LP is impossible due to the strong NP-hardness.
  终止性分析：基于模板的算法利用 Farkas 引理或 Positivstellensätze 也被应用于终止性和可达性分析的研究中[Agrawal 等，2017；Asadi 等，2021；Chatterjee 等，2016，2020a；Neumann 等，2020；Takisaka 等，2018]。然而，这是一类非常不同且正交的问题，尽管方法上存在明显的相似性，但无法直接或通过实验进行比较。从概念上讲，终止性分析中的工作假设足够强的不变式作为输入 ${}^3$${}^3$^(3){ }^{3} 的一部分，然后将寻找仿射/多项式排序函数或其概率对应物的问题归约为线性规划（LP）。这与我们的设置形成对比，我们的归约是到二次规划（QP），由于强 NP 难度，无法归约为 LP。

2 TEMPLATE-BASED SYNTHESIS OF POLYNOMIAL PROGRAMS
2 基于模板的多项式程序合成

• A finite set $\mathbb{V}$$\mathbb{V}$V\mathbb{V} of program variables,
  一组有限的程序变量 $\mathbb{V}$$\mathbb{V}$V\mathbb{V} ，
• A finite set $\mathbb{L}$$\mathbb{L}$L\mathbb{L} of locations,
  一组有限的位置 $\mathbb{L}$$\mathbb{L}$L\mathbb{L} ，
• An initial location ${\ell }_0\in \mathbb{L}$${\ell }_0\in \mathbb{L}$ℓ_(0)inL\ell_{0} \in \mathbb{L},
  一个初始位置 ${\ell }_0\in \mathbb{L}$${\ell }_0\in \mathbb{L}$ℓ_(0)inL\ell_{0} \in \mathbb{L} ，
• An initial polynomial assertion ${\theta }_0$${\theta }_0$theta_(0)\theta_{0},
  一个初始多项式断言 ${\theta }_0$${\theta }_0$theta_(0)\theta_{0} ，
• A final location $l_f\in \mathbb{L}$$l_f\in \mathbb{L}$l_(f)inLl_{f} \in \mathbb{L},
  一个最终位置 $l_f\in \mathbb{L}$$l_f\in \mathbb{L}$l_(f)inLl_{f} \in \mathbb{L} ，
• A final polynomial assertion ${\theta }_f$${\theta }_f$theta_(f)\theta_{f},
  一个最终多项式断言 ${\theta }_f$${\theta }_f$theta_(f)\theta_{f} ，
• A finite set $\mathcal{T}$$\mathcal{T}$T\mathcal{T} of transitions. Each transition $\tau \in \mathcal{T}$$\tau \in \mathcal{T}$tau inT\tau \in \mathcal{T} is a tuple ( $\ell ,{\ell }^{\prime },{\rho }_{\tau }$$\ell ,{\ell }^{\prime },{\rho }_{\tau }$ℓ,ℓ^('),rho_(tau)\ell, \ell^{\prime}, \rho_{\tau} ), where $\ell ,{\ell }^{\prime }\in \mathbb{L}$$\ell ,{\ell }^{\prime }\in \mathbb{L}$ℓ,ℓ^(')inL\ell, \ell^{\prime} \in \mathbb{L} are the pre and post locations, and ${\rho }_{\tau }$${\rho }_{\tau }$rho_(tau)\rho_{\tau}, called the transition relation, is a polynomial assertion over $\mathbb{V}\cup {\mathbb{V}}^{\prime }$$\mathbb{V}\cup {\mathbb{V}}^{\prime }$VuuV^(')\mathbb{V} \cup \mathbb{V}^{\prime}, where $\mathbb{V}$$\mathbb{V}$V\mathbb{V} represents variables in the pre location and its primed version ${\mathbb{V}}^{\prime }$${\mathbb{V}}^{\prime }$V^(')\mathbb{V}^{\prime} represents the variables in the post location, i.e. after taking the transition. Specifically, we have ${\mathbb{V}}^{\prime }=\{v^{\prime }\mid v\in \mathbb{V}\}$${\mathbb{V}}^{\prime }=\left\{v^{\prime }\mid v\in \mathbb{V}\right\}$V^(')={v^(')∣v inV}\mathbb{V}^{\prime}=\left\{v^{\prime} \mid v \in \mathbb{V}\right\};
  一个有限集合 $\mathcal{T}$$\mathcal{T}$T\mathcal{T} 的转换。每个转换 $\tau \in \mathcal{T}$$\tau \in \mathcal{T}$tau inT\tau \in \mathcal{T} 是一个元组 ( $\ell ,{\ell }^{\prime },{\rho }_{\tau }$$\ell ,{\ell }^{\prime },{\rho }_{\tau }$ℓ,ℓ^('),rho_(tau)\ell, \ell^{\prime}, \rho_{\tau} )，其中 $\ell ,{\ell }^{\prime }\in \mathbb{L}$$\ell ,{\ell }^{\prime }\in \mathbb{L}$ℓ,ℓ^(')inL\ell, \ell^{\prime} \in \mathbb{L} 是前置和后置位置， ${\rho }_{\tau }$${\rho }_{\tau }$rho_(tau)\rho_{\tau} ，称为转换关系，是关于 $\mathbb{V}\cup {\mathbb{V}}^{\prime }$$\mathbb{V}\cup {\mathbb{V}}^{\prime }$VuuV^(')\mathbb{V} \cup \mathbb{V}^{\prime} 的多项式断言，其中 $\mathbb{V}$$\mathbb{V}$V\mathbb{V} 表示前置位置的变量，其带撇号的版本 ${\mathbb{V}}^{\prime }$${\mathbb{V}}^{\prime }$V^(')\mathbb{V}^{\prime} 表示后置位置的变量，即执行转换后的变量。具体来说，我们有 ${\mathbb{V}}^{\prime }=\{v^{\prime }\mid v\in \mathbb{V}\}$${\mathbb{V}}^{\prime }=\left\{v^{\prime }\mid v\in \mathbb{V}\right\}$V^(')={v^(')∣v inV}\mathbb{V}^{\prime}=\left\{v^{\prime} \mid v \in \mathbb{V}\right\} ；
• An invariant $\mathbb{I}$$\mathbb{I}$I\mathbb{I} that maps some of the locations $\ell \in \mathbb{L}$$\ell \in \mathbb{L}$ℓinL\ell \in \mathbb{L} to a polynomial assertion $\mathbb{I}(\ell )$$\mathbb{I}(\ell )$I(ℓ)\mathbb{I}(\ell). Moreover, we have $\mathbb{I}\left({\ell }_0\right)={\theta }_0$$\mathbb{I}\left({\ell }_0\right)={\theta }_0$I(ℓ_(0))=theta_(0)\mathbb{I}\left(\ell_{0}\right)=\theta_{0} and $\mathbb{I}\left({\ell }_f\right)={\theta }_f$$\mathbb{I}\left({\ell }_f\right)={\theta }_f$I(ℓ_(f))=theta_(f)\mathbb{I}\left(\ell_{f}\right)=\theta_{f}. The set of locations for which an invariant is provided must be a cutset (see further below for a formal definition).
  一个不变式 $\mathbb{I}$$\mathbb{I}$I\mathbb{I} ，它将部分位置 $\ell \in \mathbb{L}$$\ell \in \mathbb{L}$ℓinL\ell \in \mathbb{L} 映射到多项式断言 $\mathbb{I}(\ell )$$\mathbb{I}(\ell )$I(ℓ)\mathbb{I}(\ell) 。此外，我们有 $\mathbb{I}\left({\ell }_0\right)={\theta }_0$$\mathbb{I}\left({\ell }_0\right)={\theta }_0$I(ℓ_(0))=theta_(0)\mathbb{I}\left(\ell_{0}\right)=\theta_{0} 和 $\mathbb{I}\left({\ell }_f\right)={\theta }_f$$\mathbb{I}\left({\ell }_f\right)={\theta }_f$I(ℓ_(f))=theta_(f)\mathbb{I}\left(\ell_{f}\right)=\theta_{f} 。提供不变式的位置集合必须是一个割集（正式定义见下文）。
  The translation from programs to transition systems is intuitive and straightforward. We can have one location $\ell \in \mathbb{L}$$\ell \in \mathbb{L}$ℓinL\ell \in \mathbb{L} for each line of the program, and let ${\ell }_0$${\ell }_0$ℓ_(0)\ell_{0} correspond to the initial line and ${\ell }_f$${\ell }_f$ℓ_(f)\ell_{f} to the end of the program. Similarly, ${\theta }_0$${\theta }_0$theta_(0)\theta_{0} serves as the pre-condition and ${\theta }_f$${\theta }_f$theta_(f)\theta_{f} as the post-condition. Programs are more human-friendly and hence a nicer way to specify the input to the synthesis problem. In contrast, it is easier to define the algorithms using the more formal notion of PTS. As such, we will define our semantics based on a PTS instead of a program. Below, we fix a PTS $(\mathbb{V},\mathbb{L},{\ell }_0,{\theta }_0,{\ell }_f,{\theta }_f,\mathcal{T},\mathbb{I})$$\left(\mathbb{V},\mathbb{L},{\ell }_0,{\theta }_0,{\ell }_f,{\theta }_f,\mathcal{T},\mathbb{I}\right)$(V,L,ℓ_(0),theta_(0),ℓ_(f),theta_(f),T,I)\left(\mathbb{V}, \mathbb{L}, \ell_{0}, \theta_{0}, \ell_{f}, \theta_{f}, \mathcal{T}, \mathbb{I}\right).
  从程序到转换系统的翻译直观且简单。我们可以为程序的每一行设一个位置 $\ell \in \mathbb{L}$$\ell \in \mathbb{L}$ℓinL\ell \in \mathbb{L} ，并让 ${\ell }_0$${\ell }_0$ℓ_(0)\ell_{0} 对应程序的起始行， ${\ell }_f$${\ell }_f$ℓ_(f)\ell_{f} 对应程序的结束行。同样， ${\theta }_0$${\theta }_0$theta_(0)\theta_{0} 作为前置条件， ${\theta }_f$${\theta }_f$theta_(f)\theta_{f} 作为后置条件。程序更符合人类习惯，因此是指定合成问题输入的更好方式。相比之下，使用更形式化的 PTS 概念定义算法更为简便。因此，我们将基于 PTS 而非程序来定义语义。下面，我们固定一个 PTS $(\mathbb{V},\mathbb{L},{\ell }_0,{\theta }_0,{\ell }_f,{\theta }_f,\mathcal{T},\mathbb{I})$$\left(\mathbb{V},\mathbb{L},{\ell }_0,{\theta }_0,{\ell }_f,{\theta }_f,\mathcal{T},\mathbb{I}\right)$(V,L,ℓ_(0),theta_(0),ℓ_(f),theta_(f),T,I)\left(\mathbb{V}, \mathbb{L}, \ell_{0}, \theta_{0}, \ell_{f}, \theta_{f}, \mathcal{T}, \mathbb{I}\right) 。

• ${\ell }_i={\ell }_{i-1}^{\prime }$${\ell }_i={\ell }_{i-1}^{\prime }$ℓ_(i)=ℓ_(i-1)^(')\ell_{i}=\ell_{i-1}^{\prime} for all $i>1$$i>1$i > 1i>1.
  对于所有 $i>1$$i>1$i > 1i>1 ， ${\ell }_i={\ell }_{i-1}^{\prime }$${\ell }_i={\ell }_{i-1}^{\prime }$ℓ_(i)=ℓ_(i-1)^(')\ell_{i}=\ell_{i-1}^{\prime} 。
• ${\ell }_1$${\ell }_1$ℓ_(1)\ell_{1} and ${\ell }_m^{\prime }$${\ell }_m^{\prime }$ℓ_(m)^(')\ell_{m}^{\prime} are cutpoints, but no internal location ${\ell }_i$${\ell }_i$ℓ_(i)\ell_{i} with $1<i\le m$$1<i\le m$1 < i <= m1<i \leq m is a cutpoint.
  ${\ell }_1$${\ell }_1$ℓ_(1)\ell_{1} 和 ${\ell }_m^{\prime }$${\ell }_m^{\prime }$ℓ_(m)^(')\ell_{m}^{\prime} 是割点，但没有内部位置 ${\ell }_i$${\ell }_i$ℓ_(i)\ell_{i} ，其中 $1<i\le m$$1<i\le m$1 < i <= m1<i \leq m 是割点。

• $va{l}_0\models {\theta }_0$$va{l}_0\models {\theta }_0$val_(0)|==theta_(0)v a l_{0} \models \theta_{0}, i.e. the run starts with the initial location ${\ell }_0$${\ell }_0$ℓ_(0)\ell_{0} and an initial valuation that satisfies the precondition ${\theta }_0$${\theta }_0$theta_(0)\theta_{0};
  $va{l}_0\models {\theta }_0$$va{l}_0\models {\theta }_0$val_(0)|==theta_(0)v a l_{0} \models \theta_{0} ，即运行从初始位置 ${\ell }_0$${\ell }_0$ℓ_(0)\ell_{0} 开始，且初始赋值满足前置条件 ${\theta }_0$${\theta }_0$theta_(0)\theta_{0} ；
• For every $i<m$$i<m$i < mi<m, there exists a transition ${\tau }_i\in \mathcal{T}$${\tau }_i\in \mathcal{T}$tau_(i)inT\tau_{i} \in \mathcal{T} that allows us to go from ${\sigma }_i$${\sigma }_i$sigma_(i)\sigma_{i} to ${\sigma }_{i+1}$${\sigma }_{i+1}$sigma_(i+1)\sigma_{i+1}. More formally:
  对于每个 $i<m$$i<m$i < mi<m ，存在一个转换 ${\tau }_i\in \mathcal{T}$${\tau }_i\in \mathcal{T}$tau_(i)inT\tau_{i} \in \mathcal{T} ，允许我们从 ${\sigma }_i$${\sigma }_i$sigma_(i)\sigma_{i} 到达 ${\sigma }_{i+1}$${\sigma }_{i+1}$sigma_(i+1)\sigma_{i+1} 。更正式地说：
• ${\tau }_i=({\ell }_i,{\ell }_{i+1},{\rho }_{{\tau }_i})$${\tau }_i=\left({\ell }_i,{\ell }_{i+1},{\rho }_{{\tau }_i}\right)$tau_(i)=(ℓ_(i),ℓ_(i+1),rho_(tau_(i)))\tau_{i}=\left(\ell_{i}, \ell_{i+1}, \rho_{\tau_{i}}\right); and   ${\tau }_i=({\ell }_i,{\ell }_{i+1},{\rho }_{{\tau }_i})$${\tau }_i=\left({\ell }_i,{\ell }_{i+1},{\rho }_{{\tau }_i}\right)$tau_(i)=(ℓ_(i),ℓ_(i+1),rho_(tau_(i)))\tau_{i}=\left(\ell_{i}, \ell_{i+1}, \rho_{\tau_{i}}\right) ；并且
• $(va{l}_i,va{l}_{i+1}^{\prime })\models {\rho }_{{\tau }_i}$$\left(va{l}_i,va{l}_{i+1}^{\prime }\right)\models {\rho }_{{\tau }_i}$(val_(i),val_(i+1)^('))|==rho_(tau_(i))\left(v a l_{i}, v a l_{i+1}^{\prime}\right) \models \rho_{\tau_{i}}, i.e. if we consider $va{l}_i$$va{l}_i$val_(i)v a l_{i} as a valuation on $\mathbb{V}$$\mathbb{V}$V\mathbb{V} and $va{l}_{i+1}$$va{l}_{i+1}$val_(i+1)v a l_{i+1} as a valuation on ${\mathbb{V}}^{\prime }$${\mathbb{V}}^{\prime }$V^(')\mathbb{V}^{\prime}, then they jointly satisfy the transition condition ${\rho }_{{\tau }_i}$${\rho }_{{\tau }_i}$rho_(tau_(i))\rho_{\tau_{i}}.
  $(va{l}_i,va{l}_{i+1}^{\prime })\models {\rho }_{{\tau }_i}$$\left(va{l}_i,va{l}_{i+1}^{\prime }\right)\models {\rho }_{{\tau }_i}$(val_(i),val_(i+1)^('))|==rho_(tau_(i))\left(v a l_{i}, v a l_{i+1}^{\prime}\right) \models \rho_{\tau_{i}} ，即如果我们将 $va{l}_i$$va{l}_i$val_(i)v a l_{i} 视为 $\mathbb{V}$$\mathbb{V}$V\mathbb{V} 上的一个赋值，将 $va{l}_{i+1}$$va{l}_{i+1}$val_(i+1)v a l_{i+1} 视为 ${\mathbb{V}}^{\prime }$${\mathbb{V}}^{\prime }$V^(')\mathbb{V}^{\prime} 上的一个赋值，那么它们共同满足转换条件 ${\rho }_{{\tau }_i}$${\rho }_{{\tau }_i}$rho_(tau_(i))\rho_{\tau_{i}} 。