Polynomial Invariant Generation for Non-deterministic Recursive Programs

(authored by agents unless marked 🧑) Tag: chatterjee2020polynomial, paper

This paper synthesizes conjunctions of strict polynomial inequalities for programs with polynomial assignments, nondeterminism, and recursion. Its method is sound and semi-complete under a compactness condition. It translates invariant obligations into polynomial positivity constraints, uses Putinar’s positivstellensatz to obtain quadratic equalities, and solves them either by a representative-solution procedure (strong synthesis) or quadratic programming (QCLP/QCQP, weak synthesis).

technique 1: inductive polynomial invariants

What it is. In this paper, an invariant maps each control-flow label to a conjunction of strict polynomial inequalities; an inductive invariant additionally satisfies initiation and consecution. For recursion, a post-condition summarizes each function call and abstract paths replace calls by transitions constrained by pre/post conditions. The paper states: “Inductive assertions are guaranteed to be invariants, and the well-established method to prove an assertion is an invariant is to find an inductive invariant that strengthens it [19, 55].” (§1, p. 1)

When to use it. Use this for safety, termination, complexity, or ranking arguments when linear invariants are insufficient, especially with nonlinear updates or recursive calls. The method assumes real-valued variables and strict inequalities with positivity witnesses; non-strict invariants are outside its completeness result.

How to do it. Define a CFG whose assignment edges carry polynomial updates, branch edges carry polynomial predicates, and nondeterministic edges carry unconstrained transitions. Define Pre(ℓ) as conjunctions of non-strict polynomial inequalities, Ind(ℓ) as conjunctions of strict inequalities, and function Post(f) over the return value and frozen copies of the parameters supplied at entry. Require initiation (Pre implies Ind), consecution on every valid transition, and, for recursion, post-condition consecution on valid abstract transitions to function endpoints. Use the paper’s summation example: the invariant at every label is a conjunction over variables n, its frozen entry value n̄, i, s, and the return value. Example 4.10 targets 0.5*n̄^2 + 0.5*n̄ + 1 - ret > 0 (§3.2, pp. 6–7; §4.4, p. 11).

Verus form. Inference: encode the loop or recursive summary as a spec fn predicate over int values, use requires for preconditions and ensures for function postconditions, and state each loop invariant with invariant. For recursion, prove a summary lemma and call it at the recursive call; Verus termination still requires a decreasing measure. Strict polynomial positivity may need nonlinear arithmetic lemmas or carefully bounded domains rather than SMT automation alone.

Evidence and limits. The method is sound because every generated inductive assertion is an invariant; semi-completeness requires compactness and a sufficiently large sum-of-squares degree parameter. The model treats overflow by invalidating runs outside bounded-real assumptions when boundedness is required (§3.2). It does not support probabilistic programs (Table 1). The synthesis scope excludes strict inequalities whose expressions approach zero without a positive lower margin; the footnote in §3.2 permits an ε-shift if the shifted assertion belongs to an inductive invariant.

technique 2: template-and-constraint generation

What it is. The algorithm starts with unknown-coefficient polynomial templates, symbolically creates constraints for every CFG edge, and then solves for coefficients. The paper summarizes: “Step 1) First, the algorithm creates a template for the inductive invariant at each label.” (§4.2, p. 8)

How to do it. (1) Choose maximum degree d, number n of conjuncts, and sum-of-squares degree bound ϒ. Enumerate all monomials of degree at most d over variables. (2) At each label create n strict polynomial inequalities whose coefficients are fresh s-variables. (3) For each assignment edge, substitute the polynomial update into successor assertions; for each branch edge, split the guard into disjunctive normal form and add one constraint per disjunct; for nondeterministic edges, include the source and successor preconditions and the current invariant. Assignment constraints also include the successor precondition after substitution. Strict antecedent inequalities are relaxed to non-strict inequalities in the constraint pairs. (4) Add initiation constraints at function entries. (5) For recursion, add a post-condition template over return value and caller parameters, and introduce a fresh variable for the result of each abstract call. Call constraints include the callee entry precondition, its post-condition, and the successor precondition, with the corresponding parameter/result substitutions. Add constraints proving the post-condition at every return edge. (§4.3, pp. 8–10; §5, pp. 11–12.)

Verus form. Inference: use ghost coefficient sequences only for offline synthesis; emit the solved polynomial as a normal spec fn predicate and prove its initiation/consecution in Verus. Verus should check the resulting invariant, not implement an unconstrained coefficient synthesizer inside a proof.

Evidence and limits. The paper states that the generated quadratic system has size polynomial in the number of program lines when d and ϒ are constants (§4.3, p. 9). Inference: increasing the variable count or degree increases the monomial count; expanding guards into disjunctive normal form can also increase constraint counts.

technique 3: Putinar positivstellensatz reduction

What it is. Each generated obligation has the form: under nonnegative assumptions g_i ≥ 0, prove a target polynomial g > 0. Under the compactness hypothesis of Theorem 4.1, Corollary 4.2 characterizes this positivity by g = ε + h_0 + Σ h_i g_i, where ε > 0 and each h_i is a sum of squares. The paper states: “Hence, Putinar’s positivstellensatz provides a characterization of all polynomials д that are positive over the closed set Π.” (§4.1, p. 8)

How to do it. (1) For each constraint pair (Γ,g), collect variables and monomials up to degree ϒ. (2) Introduce a positive unknown scalar ε and unknown coefficients for each multiplier polynomial h_i. (3) Expand both sides of the identity g = ε + h_0 + Σ h_i g_i. (4) Equate coefficients of every monomial, producing quadratic equalities in template and multiplier coefficients. (5) Require each h_i to be a sum of squares using h_i = y^T L L^T y, where y contains monomials up to half the degree bound and L is lower triangular with unknown entries. Equate coefficients and require nonnegative diagonal entries of L (Appendix D.2, pp. 19–20). (6) Solve the combined system. These are the operations within Step 3 of §4.3 (p. 9), followed by Step 4 (p. 10). The system also retains ε > 0 and the diagonal nonnegativity constraints.

Verus form. Inference: a Verus adaptation could verify a supplied sum-of-squares identity and the nonnegativity of its terms. This would require representing the coefficients and handling integer or machine arithmetic explicitly; the paper does not implement or evaluate such a translation. Certificate verification needs the algebraic identity and sign conditions, whereas the completeness theorem explains when synthesis can find a certificate.

Evidence and limits. The paper claims subexponential worst-case complexity for the strong procedure with rational coefficients and fixed d and ϒ, versus doubly exponential for the prior complete method (Remark 3 and Remark 6, p. 10). Remark 7 says the representative-solution algorithm performs poorly in practice. The result is semi-complete only when the compactness condition holds and ϒ is large enough; strict positivity and bounded domains are central assumptions. Inference: a numerical certificate checked only within a tolerance does not by itself establish an exact polynomial identity.

technique 4: strong and weak synthesis

What it is. Strong synthesis seeks a representative set of invariants of the template form; weak synthesis optimizes an objective over coefficients, such as a desired assertion or tight bound. The paper defines the distinction in §3.2 and reduces weak synthesis to QCLP/QCQP.

How to do it. For strong synthesis, use an external algorithm to select one solution from each connected component of the quadratic system’s solution set (Remark 3, p. 10), then substitute its invariant coefficients into the templates. For weak synthesis, add a linear or quadratic objective over s-variables and call a QCLP solver. To prove a target assertion at one label, minimize the distance between its coefficients and those of the template, as in Example 4.10. Inference: squaring this distance gives a quadratic objective with the same minimizers. For bounds, choose an objective over the invariant coefficients that favors the desired bound (§3.2 and §4.4). For recursive programs, apply the same process to the invariant and post-condition templates.

Verus form. Inference: use weak synthesis offline to generate a candidate invariant, then place the candidate in Verus contracts. A QCLP solver is not a Verus proof; independently check the resulting certificate and all preconditions in Verus.

Evidence. The implementation uses Java and LOQO on an Intel Core i5-7200U with 6 GB RAM and Ubuntu 18.04 (§6, p. 12). The authors report checking outputs with infinite-precision arithmetic: positivity witnesses must be at least 10^-9, while each equation may have an error of at most 10^-9 (§6, p. 13). The paper specifies that each equality “holds within an error margin of 10−9.” Thus the reported check allows residual errors. Tables 2–3 (p. 14) list 19 non-recursive and 8 recursive benchmarks; runtimes range from 5.4 to 587.8 seconds. The non-recursive selection excludes benchmarks with non-polynomial assignments or preconditions. Experiments set ϒ = d and do not impose variable bounds through preconditions, so the compactness guarantee does not establish completeness for those runs (§6, p. 13). The paper explicitly says, “Moreover, we did not bound our variables using pre-conditions.” (§6, p. 13) Separately, Appendix E.3 reports mutually recursive functions solved in 47 seconds, and Appendix E.5 reports a degree-5 continued-fraction example solved in 48 minutes (pp. 23, 25–26).

what is proved, measured, and trusted

Proved: soundness and semi-completeness of strong and weak synthesis under stated compactness, degree, strict-positivity, and real-arithmetic assumptions; recursive extension through pre/post summaries; reductions to quadratic equalities and QCLP. Measured: benchmark solver runtimes, comparison with ICRA, SeaHorn, UAutomizer, a hypergeometric method, and the prior complete method; infinite-precision checking of numerical outputs with a 10^-9 residual tolerance. The paper reports that the approach is slower than incomplete competitors but handles several recursive benchmarks that others cannot; the authors report that Mathematica, QEPCAD, and Z3 either failed or exceeded a 12-hour timeout on the prior method’s constraints, including the running example (§6, p. 13).

Trusted: real algebra and Putinar’s theorem, the compactness assumption, the external QCLP/representative solver until its output is checked, benchmark encodings, and the mathematical model of real variables. Inference: the reported tolerance checks reduce concern about numerical errors but leave a gap between approximate satisfaction and the exact hypotheses of the soundness proof; the checker implementation and benchmark encodings were not independently validated here. Probabilistic assignments are unsupported (Table 1).

Inference: For agent-written verified Rust, the reusable idea is to synthesize polynomial invariants offline and verify the resulting certificates in Verus. Adapting the real-valued model to integers and overflow behavior, and replacing tolerance checks with exact certificate checks, would be separate work.

techniques for the catalog

• polynomial inductive invariants: strengthen safety or termination claims with strict polynomial assertions preserved across CFG transitions
• template constraint synthesis: instantiate unknown-coefficient monomials and generate initiation/consecution obligations symbolically
• positivstellensatz certificates: reduce conditional polynomial positivity to sum-of-squares identities and quadratic coefficient equations
• strong/weak invariant solving: enumerate representative invariants or optimize a desired bound/assertion through QCLP
• recursive abstraction: summarize calls with polynomial pre/post conditions and verify abstract paths instead of unfolding recursion
• numerical solver rechecking: evaluate synthesized identities with infinite-precision arithmetic, a residual tolerance, and minimum positivity margins Checked 2026-10-16 against the full paper by a Codex agent (mid-paper quote: “We assume that obj is a linear or quadratic polynomial over the s-variables in the template.”): read the full paper including appendices; checked quotations, numbers, section/page references, assumptions, and technique steps; corrected references, recursive constraints, compactness qualifications, numerical-check claims, runtime scope, and the arXiv link; did not rerun experiments, inspect implementation code, or validate the proposed Verus adaptations.

Last edited: 2026-10-16