{"id":"38c827ed-8cf9-45fe-8ef2-ccda32b4c41f","arxiv_id":"2506.18171","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":5.0,"correctness_risk":"low","formal_verification":"none","parameter_count":2,"one_line_summary":"Sign-definite polynomials' parity constraints are used as symbolic reduction rules to speed up SMT synthesis of global Lyapunov functions.","lead":"This paper shows how to automatically simplify the search for global Lyapunov functions, certificates that a dynamical system converges to a fixed point. The authors derive simple algebraic rules that prune impossible terms from a candidate function before applying SMT solvers, and demonstrate the approach on systems up to ten dimensions.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"LaSalle synthesis loop's r values and iteration bound are unspecified, so the reported 'complete' LaSalle synthesis is under-auditable.","rationale":"The reader's weakest assumption identifies the same principal risk: the LaSalle synthesis loop is not fully specified and the r values for E8-E10 are missing. This is a genuine reproducibility and completeness concern rather than a mathematical counterexample. Proposition 1 appears correct, and the symbolic reduction rules derived from it are necessary conditions, so they should not discard valid strict or weak Lyapunov functions. The reported Lyapunov functions in the appendix are concrete certificates that can be verified independently. However, the central claim that the LaSalle-type conditions 'allow us to efficiently solve many cases' depends on the iterative search reaching a valid r. Without knowing the iteration bound and the r values actually used, one cannot tell whether an 'unsat' answer from the synthesis procedure means no weak Lyapunov function of the template exists or merely that the search stopped too early. This is exactly the kind of missing experimental parameter that should be reported before the empirical claims are treated as fully auditable. The correct response is therefore CONDITIONAL: the method is credible and the mathematical core is sound, but the LaSalle experiments need the missing r and bound specifications, plus a verification that increasing r does not change the answers.","tokens_in":18184,"tokens_out":25790,"duration_ms":263951,"concrete_test":"Inspect the archived code (DOI 10.5281/zenodo.15272621) to extract the exact r iteration schedule and the maximum r bound used for Z3-Complete-SR-LaSalle on E8-E10. Then re-run each example with the maximum r increased by at least 2 beyond the implemented bound, and also with condition (18) in place of (19), logging the first successful r and verifying every returned V by exact arithmetic. If any E8-E10 result changes from unsat to sat, or if condition (18) succeeds at an r where (19) fails, the paper's completeness and efficiency claims for the LaSalle procedure would need qualification.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The most load-bearing weakness is the LaSalle synthesis loop in Section 5.2. The paper says conditions (18) and (19) are checked in an iterative loop up to some degree-r Lie derivative, but it never specifies the loop's maximum r or the r values used for E8-E10. This matters because Proposition 2 only concludes GAS if a finite r satisfying (13) exists, and for a fixed template the existence of such an r is not guaranteed a priori. If the implementation stops at a fixed bound and reports unsatisfiable, it may incorrectly claim that no weak Lyapunov function of the given form exists even though one would satisfy the LaSalle condition for a larger r. The reported Lyapunov functions themselves can be checked by substitution, so this does not invalidate the concrete certificates, but it does undermine the 'complete synthesis' label and makes the central LaSalle-based empirical claims hard to audit. The paper cites [10] for finite termination via the descending chain condition, but it does not prove or bound r for its own procedure.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper proposes symbolic reduction rules for the formal synthesis of global polynomial Lyapunov functions. Proposition 1 gives necessary algebraic conditions on sign-definite polynomials, including parity constraints on lowest and highest homogeneous parts and on monomials that attain maximal exponent in a variable; these conditions are used to eliminate impossible terms from a Lyapunov template before SMT/LP synthesis. Proposition 2 reformulates LaSalle's invariance principle as a finite higher-order Lie derivative condition that can be checked by SMT. The authors present SMT-based complete synthesis for strict and weak Lyapunov functions, a LaSalle loop, instability tests, and CEGIS baselines with and without the reduction. Experiments on ten examples (E1–E10) and random instability tests up to dimension 10 show that the reduction improves success rates and runtimes, with code and data archived at a public DOI.","tokens_in":18268,"tokens_out":18046,"duration_ms":164096,"significance":"The core technical results are correct and practically useful. Proposition 1 is a clean, parameter-free necessary-condition result, and the symbolic reduction built on it addresses a real bottleneck: sample-based CEGIS can be misled by near-cancellations that are algebraically impossible for a sign-definite polynomial. Proposition 2's Lie-derivative condition is a practical sufficient condition for LaSalle, and the paper's use of exact SMT arithmetic to verify the synthesized certificates is a strength. The archived code (DOI 10.5281/zenodo.15272621) supports reproducibility. If the procedures are fully specified, the approach could make global Lyapunov synthesis substantially more robust than the SOS/SDP baseline in the tested regime. The paper does not overclaim the exhaustiveness of the reduction (Remark 2), and the proof of Claim 5.4 is self-contained.","major_comments":[{"comment":"The reduction procedure is only illustrated, not formally specified. The text says to “introduce symbolic equality and inequality constraints” from Proposition 1, but it does not define the algorithm for selecting which monomials to test, how to handle iterated reductions after coefficients are zeroed (e.g., when the lowest or highest degree changes), or when the procedure terminates. Since the paper's central claim is that symbolic reduction is a systematic preprocessing method, this under-specification makes the method unauditable from the manuscript alone; the archived code alleviates, but does not replace, a formal description of the algorithm.","section":"Section 5.1"},{"comment":"The iterative LaSalle loop is not specified: no maximum r, no increment rule, and no r values are reported for E8–E10. Proposition 2 requires existence of a finite r satisfying (13), but for a fixed template such an r is not guaranteed a priori. If the loop stops at an implementation-chosen bound and returns “unsatisfiable”, the procedure would incorrectly report that no weak Lyapunov function of the given form exists even though a larger r would work. The concrete certificates in Table 2 can be checked, so the reported Lyapunov functions are valid, but the “complete synthesis” label for the LaSalle module is not justified. The paper cites [10] for finite termination via the descending chain condition, but it does not prove that its own loop reaches such an r or provide a bound.","section":"Section 5.2, Eqs. (18)–(19)"},{"comment":"The strict-Lyapunov SMT query (16) does not encode radial unboundedness. Positive definiteness of a polynomial does not imply radial unboundedness (e.g., V(x1,x2)=x1^2+x2^2(1−x1)^2 is positive definite but bounded along the line x1=1). The text inserts “provided that V is also radially unbounded” after invoking Theorem 1, but the synthesis query and the subsequent verification step are not described as checking this condition. As written, a satisfying model of (16) may not satisfy the hypotheses of Theorem 1, so the procedure is not complete for global Lyapunov certificates unless radial unboundedness is added as a constraint or verified separately. The same omission affects the weak-Lyapunov query (17).","section":"Section 5.2, Eq. (16)"}],"minor_comments":[{"comment":"The claim in Section 5.4 is unnumbered, but Sections 1 and 5.4 refer to “Claim 5.4”; either number the claim or fix the cross-references.","section":"Section 5.4"},{"comment":"The sentence “Since pk(x) and pk(x) must be negative semi-definite” should read “Since p_l(x) and p_k(x) must be negative semi-definite”.","section":"Section 3.2, proof of Proposition 1, part (3)"},{"comment":"In the discussion after Example 2, “L1_f(x)” should be “L1_f V(x)” (or “\\dot V(x)”) for consistency with the notation in (11).","section":"Section 4"},{"comment":"The derivation “Setting 2c0−2c1=0, −c2=0, and c2=0 yields c0=c1 and c2=0” would be clearer if it stated explicitly that this follows from requiring the degree-7 homogeneous part of \\dot V to vanish identically (since 7 is odd), rather than from term-by-term coefficient matching.","section":"Section 5.1, Example 3"},{"comment":"The average times of 0.000 seconds for stable cases in high dimensions should be explained (e.g., timing resolution) to avoid suspicion about the measurements.","section":"Section 6, Table 3"}],"recommendation":"major_revision","confidential_remarks":"The paper is within scope for the journal, the core mathematics is correct, and the issues are addressable. The main risk is overclaiming “complete synthesis” for the LaSalle loop; this should be toned down or the loop specified. No concerns about citation patterns beyond the self-citation to the arXiv version, which is standard in this context."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper is a genuinely useful engineering contribution: it packages some elementary necessary conditions on sign-definite polynomials into symbolic reduction rules that prune Lyapunov templates before SMT or LP solving. It does not change the complexity landscape or answer any open decidability question, and Proposition 1 is not deep mathematics, but the pre-processing is clearly effective on the examples—LP-CEGIS and Z3-CEGIS with reduction solve cases that the same methods without reduction cannot. The formal justification in Claim 5.4, showing that sample-based CEGIS can be permanently misled on a simple quadratic template, is a nice touch. The LaSalle-type condition in Proposition 2 is correctly stated and the authors properly credit [10,17] for the underlying idea. The archived code and verifiable certificates in the appendix are real evidence: the synthesized functions can be checked by substitution, so the concrete results are not in doubt.\n\nThe soft spots are about auditability, not correctness. First, the symbolic reduction algorithm is only described informally via examples and a remark; there is no pseudocode or precise statement of which reduction rules are applied in which order. That is minor, since the idea is simple, but a formal specification would make the results reproducible. Second, the LaSalle synthesis loop in Section 5.2 is the main worry. The paper says (18) and (19) are checked in an iterative loop up to some degree-r Lie derivative, but it never reports the maximum r tried, the actual r used for E8–E10, or whether the loop terminates by finding a certificate or by hitting a bound. If the implementation stops at a fixed bound and returns unsatisfiable, that is not a valid \"complete\" verdict, because Proposition 2 only applies when the r actually satisfies (13), and for a fixed template no such r is guaranteed to exist a priori. The reported Lyapunov functions for E8–E10 are still valid certificates, so this is an under-auditable claim about completeness, not a broken result. Finally, Table 3 is confusing: the stable columns show 0.000 times while timeouts also appear as 0.0, and it is unclear what the Z3-complete-SR calls actually proved in the stable cases. The paper also leaves mu and other LP parameters unspecified.\n\nMy overall take: the core symbolic reduction idea is sound and worth knowing, and the paper deserves to go to peer review. It needs minor revision—specify the reduction procedure, report the LaSalle loop parameters, and clean up Table 3—but the contribution is solid and the negative result about CEGIS is a useful warning for the community. I would cite this if I were working on automated Lyapunov synthesis.","headline":"A practical symbolic pre-processing step that makes SMT/LP Lyapunov synthesis work on several benchmarks; worth a serious referee, but the LaSalle loop's unspecified r values and parameters need fixing before the empirical claims are fully auditable.","tokens_in":18874,"tokens_out":2186,"would_cite":true,"duration_ms":24496,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["93D30","93D20","34D20"],"pacs":[],"model":"deepseek-v4-flash","headline":"A simple parity condition on sign-definite polynomials lets automated synthesis of global Lyapunov functions succeed on problems where sampling-based and SMT baselines fail.","keywords":["polynomial Lyapunov functions","global asymptotic stability","symbolic reduction","sign-definite polynomials","satisfiability modulo theories","LaSalle invariance principle","SMT synthesis","counterexample-guided synthesis"],"falsifier":"Try to construct, using quantifier elimination on real closed fields, a polynomial $p$ with $p(x)\\le 0$ for all $x$ whose highest-degree homogeneous part has odd total degree; any such polynomial would falsify Proposition 1(1). For the LaSalle procedure, take a known globally asymptotically stable system with a weak Lyapunov function whose Lie derivative vanishes on a continuum containing nonzero points, and decide exactly whether $C_1\\cap\\cdots\\cap C_r=\\{0\\}$ for some finite $r$; if no finite $r$ collapses the chain, the finite-$r$ SMT check would incorrectly report that no such weak Lyapunov function exists.","tokens_in":17884,"feed_emoji":"📉","tokens_out":8619,"duration_ms":86544,"temperature":0.7,"pith_summary":"This paper makes the automated search for polynomial Lyapunov functions, which certify that a dynamical system converges to the origin from everywhere, more reliable by applying symbolic algebra before numerical or logical search. It proves that any polynomial staying nonpositive on all of $\\mathbb{R}^n$ must have even lowest and highest total degrees, nonpositive extremal homogeneous parts, and even exponent factors on certain leading monomials. These necessary conditions are turned into symbolic reduction rules that prune impossible terms from a Lyapunov template before an optimizer or an SMT solver runs. The paper also gives a LaSalle-type sufficient condition using higher Lie derivatives so that weak Lyapunov functions can still certify global asymptotic stability, and an SMT-encoded instability test that quickly disproves global stability for many random systems.","feed_headline":"A parity rule makes Lyapunov search feasible where baselines fail","feed_subtitle":"Before solving, rule out impossible terms; SMT then finds global stability certificates in seconds.","key_machinery":"The machinery is the pair of results built around sign-definite polynomials and the Lie-derivative chain. The first is the parity/degree identity of Proposition 1: a globally nonpositive polynomial cannot have an odd lowest or highest total degree, and its extremal homogeneous parts must themselves be nonpositive. Its computational use is symbolic reduction: compute the Lie derivative of the template $V$, impose the necessary coefficient constraints on the offending monomials, and solve those linear constraints to remove impossible terms before calling an SMT solver or an optimizer. The second is the LaSalle condition of Proposition 2, defined through the sets $C_k=\\{x: L^1_fV(x)=\\cdots=L^k_fV(x)=0\\}$: if $C_1\\cap\\cdots\\cap C_r=\\{0\\}$ for some finite $r$, then a weak Lyapunov function suffices to prove global asymptotic stability, and this condition is encoded as an SMT formula with higher Lie derivatives.","core_discovery":"The central discovery is Proposition 1: a polynomial $p(x)=\\sum_{l\\le|\\alpha|\\le k} c_\\alpha x^\\alpha$ that satisfies $p(x)\\le 0$ for all $x$ must have even lowest degree $l$ and even highest degree $k$; its lowest- and highest-degree homogeneous parts $p_l$ and $p_k$ must be negative semidefinite; and any monomial whose exponent in some variable is maximal among all monomials in $p$ must have that exponent even. The same conclusions hold with signs reversed for globally nonnegative polynomials. Section 5.1 turns these necessities into reduction rules: since $\\dot V=\\nabla V\\cdot f$ must be nonpositive for a valid global Lyapunov candidate, any terms in $\\dot V$ that violate the parity and degree conditions must be forced to vanish, yielding linear equations on the template coefficients. The experiments show that this converts cases where sampling-based synthesis times out or returns invalid certificates into fast successful synthesis, including four- and six-dimensional systems and weak-Lyapunov examples solved through LaSalle's principle.","pith_inferences":["A direct test of how much of the difficulty is algebraic rather than computational would be to run the reduced-template SMT synthesis against a brute-force coefficient search on the same examples; the gap measures the value of the symbolic step.","The LaSalle procedure's finite $r$ is a heuristic in the implementation: the paper cites an algebraic descending-chain argument for finite termination but gives no explicit bound, so an adaptive loop that keeps increasing $r$ until condition (13) holds would be a natural and testable extension.","The same parity and degree reduction should apply to local Lyapunov certificates outside a compact neighborhood of the origin, since the necessary conditions are purely algebraic and do not rely on global geometry; testing this on a compact-domain SMT formulation would check that extension.","For high-dimensional instability tests, the reduction appears to be the main enabler, suggesting that symbolic preprocessing could similarly accelerate neural or other template-based Lyapunov searches."],"forward_implications":["For any polynomial Lyapunov candidate of a polynomial vector field, the Lie derivative's lowest- and highest-degree homogeneous parts must be even and negative semidefinite, so templates violating this can be rejected before any solver runs.","Because the reduction rules are necessary conditions, they never discard a valid Lyapunov candidate, so complete SMT synthesis over the reduced template remains sound.","Weak, non-strict Lyapunov functions can certify global asymptotic stability by checking a finite chain of higher Lie derivatives, which the paper demonstrates on examples where strict Lyapunov search fails.","Sampling-based synthesis can fail in a strong sense without reduction: on the motivating example, every finite sample set admits invalid coefficients that satisfy the sampled inequalities, so no number of samples repairs the template.","Instability can be certified with the same reduction machinery, and the paper reports sub-second disproofs of global asymptotic stability for randomly generated systems up to ten dimensions.","The reduction rules shrink the parameter space before solving, which the experiments show is often the difference between timeout and a valid certificate."],"supporting_citations":[{"why":"Provides the Lyapunov and LaSalle theorem statements (Theorem 1 and Theorem 2) that the synthesis conditions are designed to satisfy.","marker":"[15]"},{"why":"Provides the invariance-principle formulation and the instability theorem (Theorem 3) used by the LaSalle and instability procedures.","marker":"[16]"},{"why":"Shows finite termination for an analogous LaSalle-type condition, cited to justify checking higher Lie derivatives up to some integer $r$.","marker":"[10]"},{"why":"Introduces the LP- and SMT-based counterexample-guided synthesis loops that this paper's symbolic reduction is added to.","marker":"[3]"},{"why":"Supplies the linear-programming synthesis approach and several benchmark examples used in the case studies.","marker":"[26]"},{"why":"Supplies the sum-of-squares Lyapunov construction and the high-dimensional example used as a comparison case.","marker":"[23]"},{"why":"Implements the SMT engine used by the satisfiability procedures for complete synthesis and verification.","marker":"[8]"}],"fun_headline_variants":["Parity rules prune Lyapunov search, making synthesis tractable","Necessary constraints speed Lyapunov synthesis, beating baselines","Symbolic reduction: from impossible to rapid Lyapunov certification","Rule out bad terms first: Lyapunov synthesis in seconds","Algebraic parity conditions enable fast global stability proofs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that a polynomial which is nonpositive on all of $\\mathbb{R}^n$ really must obey the parity and degree constraints of Proposition 1; for the LaSalle-based results, it is the additional assumption that every valid weak Lyapunov function has some finite number $r$ of higher Lie derivatives that collapses the zero-set chain to the origin, and the implementation gives no proof or explicit bound for the $r$ it searches.","fun_headline_variants_meta":{"raw":{"variants":["Parity rules prune Lyapunov search, making synthesis tractable","Necessary constraints speed Lyapunov synthesis, beating baselines","Symbolic reduction: from impossible to rapid Lyapunov certification","Rule out bad terms first: Lyapunov synthesis in seconds","Algebraic parity conditions enable fast global stability proofs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000221,"raw_usage":{"total_tokens":1445,"prompt_tokens":937,"completion_tokens":508,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":553,"completion_tokens_details":{"reasoning_tokens":423}},"tokens_in":553,"tokens_out":508,"duration_ms":5179,"temperature":1.0,"reasoning_tokens":423,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T18:55:36.196005+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Try to construct, using quantifier elimination on real closed fields, a polynomial $p$ with $p(x)\\le 0$ for all $x$ whose highest-degree homogeneous part has odd total degree; any such polynomial would falsify Proposition 1(1). For the LaSalle procedure, take a known globally asymptotically stable system with a weak Lyapunov function whose Lie derivative vanishes on a continuum containing nonzero points, and decide exactly whether $C_1\\cap\\cdots\\cap C_r=\\{0\\}$ for some finite $r$; if no finite $r$ collapses the chain, the finite-$r$ SMT check would incorrectly report that no such weak Lyapunov function exists.","supporting_citations":[{"cited_title":"Prentice-Hall (2002)","cited_arxiv_id":null,"evidence_quote":"Provides the Lyapunov and LaSalle theorem statements (Theorem 1 and Theorem 2) that the synthesis conditions are designed to satisfy."},{"cited_title":"Academic Press (1961) Symbolic Reduction for Formal Synthesis of Global Lyapunov Functions 19","cited_arxiv_id":null,"evidence_quote":"Provides the invariance-principle formulation and the instability theorem (Theorem 3) used by the LaSalle and instability procedures."},{"cited_title":"In: 2020 7th International Conference on Control, Decision and Information Technologies (CoDIT)","cited_arxiv_id":null,"evidence_quote":"Shows finite termination for an analogous LaSalle-type condition, cited to justify checking higher Lie derivatives up to some integer $r$."},{"cited_title":"In: Proc","cited_arxiv_id":null,"evidence_quote":"Introduces the LP- and SMT-based counterexample-guided synthesis loops that this paper's symbolic reduction is added to."},{"cited_title":"IFAC Proceedings Volumes46(23), 576–581 (2013)","cited_arxiv_id":null,"evidence_quote":"Supplies the linear-programming synthesis approach and several benchmark examples used in the case studies."},{"cited_title":"In: Proceedings of the 41st IEEE Conference on Decision and Control, 2002","cited_arxiv_id":null,"evidence_quote":"Supplies the sum-of-squares Lyapunov construction and the high-dimensional example used as a comparison case."}],"review_version":2}