一句话：用半定规划松弛与鲁棒优化合成多项式程序不变式，分别求解强、弱不变式合成问题并给出理论保证。
基于约束求解的不变式合成把参数化模板的归纳条件编码为约束，其中刻画所有合法参数赋值的问题是强不变式合成，寻找单个可行赋值的问题是弱不变式合成；难点在于约束通常非凸且缺乏高效求解器。本文提出两个基于半定规划（SDP）的算法：Cluster 面向强合成，用鲁棒优化求解一系列 SDP 松弛，得到合法参数集逐步精确的下近似，并证明可靠性、收敛性及特定鲁棒性假设下的弱完备性；Mask 处理该假设不成立时，识别出含参数化多项式等式与已知不等式的掩码模板，通过变量替换将约束化为可用 SDP 松弛求解的等价形式。两者均已实现，实验表明优于现有方法。
Constraint-solving-based program invariant synthesis takes a parametric invariant template and encodes the (inductive) invariant conditions into constraints. The problem of characterizing the set of all valid parameter assignments is referred to as the strong invariant synthesis problem , while the problem of finding a concrete valid parameter assignment is called the weak invariant synthesis problem . For both problems, the challenge lies in solving or reducing the encoded constraints, which are generally non-convex and lack efficient solvers. In this article, we propose two novel algorithms for synthesizing invariants of polynomial programs using semidefinite programming (SDP): (1) The Cluster algorithm targets the strong invariant synthesis problem for polynomial invariant templates. Leveraging robust optimization techniques, it solves a series of SDP relaxations and yields a sequence of increasingly precise under-approximations of the set of valid parameter assignments. We prove the algorithm’s soundness, convergence, and weak completeness under a specific robustness assumption on templates. Moreover, the outputs can simplify the weak invariant synthesis problem. (2) The Mask algorithm addresses the weak invariant synthesis problem in scenarios where the aforementioned robustness assumption does not hold, rendering the Cluster algorithm ineffective. It identifies a specific subclass of invariant templates, termed masked templates, involving parameterized polynomial equalities and known inequalities. By applying variable substitution, the algorithm transforms constraints into an equivalent form amenable to SDP relaxations. Both algorithms have been implemented and demonstrated superior performance compared to state-of-the-art methods in our empirical evaluation.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{WuWXZZY25,
title = {Synthesizing Invariants for Polynomial Programs by Semidefinite Programming},
author = {Hao Wu and Qiuye Wang and Bai Xue and Naijun Zhan and Lihong Zhi and Zhi-Hong Yang},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {47},
number = {1},
year = {2025},
doi = {10.1145/3708559}
}