{"id":"c28b86c7-9973-45bb-9ec1-ff42ecd4c782","arxiv_id":"2506.06564","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"Neural controllers trained to satisfy a learned dissipativity inequality are shown to stabilize the closed loop and to solve a constructed infinite-horizon optimal control problem.","lead":"This paper trains neural controllers with formal stability and optimality certificates using learned storage and supply functions from dissipativity theory. A generalist would read it to see a verification-guided scheme that guarantees closed-loop stability and yields a controller that is optimal for a cost derived from the learned functions.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"SMT verification via scalar conditions (31)-(32) is dimensionally invalid for n≠m and cannot certify the matrix definiteness hypotheses of Theorems 5-6, so the promised formal guarantees are not established as stated.","rationale":"The reader's weakest assumption is exactly the load-bearing concern: the SMT-verifiable scalar conditions used in §4.2 do not certify the matrix definiteness conditions required by The central theorems. I agree with this assessment and with the CONDITIONAL verdict. The main theorems are correct in their mathematical content when the matrix hypotheses are actually verified; the proof of Theorem 6 is a standard inverse-optimality completion-of-squares argument, and Theorem 5 only needs x^T Δ(x)x > 0 for the Lyapunov decrease, which is weaker than Δ(x)≻0. Thus the core approach is not invalidated. However, the paper's promised 'provable guarantees' rest on the soundness of the verification step, and that step is not sound as written: the expression x^T R(x)x is dimensionally invalid in the reported experiments, and it cannot certify matrix positivity at any fixed x, nor at x=0. The optimality certificate is especially affected because R(x)^{-1} and the nonnegativity of v^T R(x)v require genuine matrix positive definiteness. I also noted a separate internal inconsistency: the bi-Lipschitz condition in §4 is stated with 0 < ν < μ, which is infeasible for any nonzero state, indicating the manuscript has not been carefully proofread. This reinforces the need for a revised, precise verification statement, but it is not the central concern. A concrete check on the released code and trained networks would settle whether the verifier actually attempts a dimensionally invalid predicate or silently substitutes a scalar check, and whether the learned matrices are positive definite on the region of interest. Given that the gaps are addressable and the underlying theory appears sound, the reader's CONDITIONAL verdict should remain.","tokens_in":15492,"tokens_out":13643,"duration_ms":137937,"concrete_test":"Run the released verifier on the inverted-pendulum benchmark (n=2, m=1) exactly as described in §4.2, and inspect what predicate is actually sent to dReal: (a) if Eq. (32) is instantiated as x^T R(x)x > 0, the expression is undefined because x is 2-dimensional while R(x) is a scalar; (b) if it is silently replaced by R(x) > 0, record whether R(x) > 0 is certified on all of X. Independently, on a dense grid in X, compute the minimum eigenvalues of R(x) and Δ(x) using the released trained networks. If any grid point has eigmin(R(x)) ≤ 0 or eigmin(Δ(x)) ≤ 0 while the scalar inequalities (31)-(32) hold, the SMT certificate does not imply the theorems' hypotheses, confirming the verification gap.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 4.2 reduces the matrix definiteness conditions R(x)≻0 and Δ(x)≻0 required by Theorems 5 and 6 to the scalar inequalities x^T R(x)x > 0 and x^T Δ(x)x > 0 for all x in X (Eqs. (31)-(32)). This reduction is not valid as stated. In the supply rate (6), R(x) is m×m and x is n-dimensional, so x^T R(x)x is only defined when n=m. The paper's own experiments have n>m (e.g., inverted pendulum n=2, m=1; rod-on-cart n=4, m=1), making Eq. (32) dimensionally ill-posed. Even when n=m, x^T R(x)x>0 on X does not imply R(x)≻0 at each x: it only certifies positivity along the state directions evaluated, and at x=0 the expression is identically 0, so R(0)>0 cannot be certified. For Δ(x), the proof of Theorem 5 only needs x^T Δ(x)x>0 along closed-loop trajectories, so the scalar condition (31) is actually sufficient for the stability conclusion; however, the theorem's stated hypothesis Δ(x)≻0 is stronger, and the verification does not establish it. The optimality theorem is more sensitive: it requires R(x) to be positive definite as a matrix to define R(x)^{-1} and to ensure v^T R(x)v ≥ 0 for all control directions v in the completion-of-squares argument. Scalar verification does not provide this. Therefore, the SMT certificate as described does not imply the antecedents of Theorems 5-6, and the paper's central claim of provable stability and optimality guarantees for the learned neural controller is not supported by the stated verification procedure. The gap is repairable (e.g., by verifying R(x)≻0 directly for scalar input, or using symbolic eigenvalue/SDP-based checks), but as written the formal claim fails.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The manuscript proposes a framework for learning neural-network storage functions V(x) and QSR supply-rate functions (Q(x),S(x),R(x)) such that a nonlinear control-affine system satisfies an input-output dissipativity inequality; the controller π(x) = -R(x)^{-1} S(x)^T x is then claimed to asymptotically stabilize the closed loop and to be optimal for an infinite-horizon cost constructed from the learned functions. A counterexample-guided training loop with PGD candidate generation and SMT verification is used to certify the required inequalities, and numerical experiments on an electric circuit, an inverted pendulum, and a rod-on-cart compare the resulting controllers against NCLF and trajectory-based optimal control baselines.","tokens_in":15971,"tokens_out":7398,"duration_ms":71641,"significance":"The central idea of learning dissipativity certificates to obtain simultaneously stabilizing and inverse-optimal neural controllers is attractive and timely, and the state-only reformulation of the dissipativity condition (Proposition 8) is a useful dimensionality reduction for sampling. The stability result (Theorem 5) and the inverse-optimality result (Theorem 6) are self-contained and, modulo presentation issues, the underlying algebra is standard and plausible. The paper also ships reproducible code and compares against reasonable baselines. However, the formal verification step in Section 4.2 does not certify the matrix definiteness hypotheses of the theorems, which undermines the claimed stability and optimality guarantees as stated.","major_comments":[{"comment":"The reduction of Δ(x)≻0 and R(x)≻0 to the scalar inequalities x^T Δ(x)x > 0 and x^T R(x)x > 0 for all x in X is not a valid certificate. First, R(x) is m×m while x is n-dimensional, so x^T R(x)x is undefined unless n=m; in the paper's own experiments n≠m (pendulum n=2,m=1; rod-on-cart n=4,m=1). Second, even in the square case, at x=0 the inequality reads 0>0 and is false, so the stated condition cannot hold on any set X containing the origin; if X\\{0} is intended, the condition only tests the state directions, not arbitrary control directions, and cannot certify strict positive definiteness of R at the origin, which is needed to define R(x)^{-1} and to make the completion-of-squares argument in Theorem 6 valid. Consequently, the SMT certificate as described does not imply the antecedents of Theorems 5 and 6, and the formal guarantees claimed in Sections 3 and 5 are not established.","section":"Section 4.2, Eqs. (31)-(32)"},{"comment":"The proof contains an unjustified separation: it writes J = - min_u ∫ Vdot dt + min_v ∫ v^T R v dt, suggesting that the two minimizations can be performed independently. In fact ∫ Vdot over [0,∞) equals V(x(∞)) - V(x(0)) = -V(x(0)) for every admissible trajectory with lim x(t)=0, so it is a constant independent of u and the separation can be made rigorous; as written, however, the displayed equality is not justified. The same line also replaces u^T R(x)u in the cost integrand (18) with x^T R(x)x, a typo that obscures the argument. These issues are repairable, but the proof as printed is not fully correct.","section":"Theorem 6 proof"},{"comment":"The optimality guarantee is inverse-optimal by construction: Theorem 6 certifies π as optimal for the cost l̃ + u^T R u + x^T Δ x, which is written in terms of the learned functions V,Q,S,R. The user-defined cost l(x,u) enters only through the soft least-squares shaping loss (29), and Theorem 6 gives no bound on the suboptimality of π with respect to that user cost. The abstract's phrase 'inheriting optimality properties that can be shaped towards user-defined control objectives' should be qualified accordingly; the experimental match to LQR on the circuit is encouraging but is not a certificate.","section":"Section 3.2, Eq. (18); Section 4.1, Eq. (29)"},{"comment":"The theorem statement says '0 ≺ R(x) : X → R^{n×n}', but R(x) should map to R^{m×m} since u ∈ R^m in the supply rate (6). This is not merely cosmetic: the dimensional mismatch in Eq. (32) is partly caused by conflating the state dimension n with the input dimension m, and correcting the statement makes it clear that the scalar verification cannot cover the required matrix inequality.","section":"Theorem 5 statement"}],"minor_comments":[{"comment":"The expression 'min_v ∫ v^T R(x)vdt' near the end of the proof is missing the 'dt' inside the integrand; it should read 'min_v ∫ v^T R(x)v dt'.","section":"Theorem 6 proof"},{"comment":"The 'Region of interest' entries are ambiguous: 'Pendulum Static [π, 2]' presumably denotes [-π,π]×[-2,2], and 'RodCart [0.1, 0.1, 0.1, 0.1]' presumably denotes [-0.1,0.1]^4; please state the intended boxes explicitly.","section":"Table 1"},{"comment":"The paragraph on necessity refers to 'the dissipativity matrix condition (22)' before Eq. (22) is introduced in Proposition 8; reorder these two parts or add a forward reference.","section":"After Theorem 5"},{"comment":"The phrase 'equivalent and verifiable algebraic constraints' is misleading for (31)-(32) given the issues raised in the major comments; please use a formulation such as 'relaxations used in verification' and state the exact conditions that the SMT solver checks.","section":"Section 4.2"},{"comment":"dReal is δ-complete, so the verification results are only correct up to the precision parameter δ (set to 10^{-3} in the experiments); the paper should state clearly that the certificates are approximate in this sense.","section":"Section 4.2"}],"recommendation":"major_revision","confidential_remarks":"The verification gap is the main concern; it is local and repairable, so I am recommending major revision rather than rejection. The authors should also be more careful in the presentation to distinguish inverse optimality for a learned cost from optimality for the user-specified cost. The paper is a reasonable fit for Automatica provided these points are addressed."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know two things about 2506.06564. First, the stability theorem is explicitly based on Madeira's earlier dissipativity result, and the optimality theorem is the standard inverse-optimality construction. The genuinely new bit is the learning pipeline: training neural storage and QSR supply-rate functions against an SMT verifier, with the state-only reformulation in Proposition 8 to avoid sampling over the input space. That is a reasonable and useful engineering contribution, and the experiments on the three benchmarks are encouraging.\n\nSecond, the formal guarantee as stated does not follow from the verification the paper actually runs. Section 4.2 reduces R(x)≻0 and Δ(x)≻0 to the scalar inequalities x^T R(x)x > 0 and x^T Δ(x)x > 0 for all x in X. This is problematic. R is an m×m matrix acting on the input, so x^T R x is not even defined when n≠m, which is the case in every experiment (n=2 or 4, m=1). If R is scalar, the condition collapses to R(x)>0 and could be checked directly, but the paper's stated condition is still dimensionally wrong. For Δ, the inequality x^T Δ x > 0 on a neighborhood of the origin does imply Δ≻0 because the state directions span R^n, but the condition must hold for all x in X and fails at x=0 unless you exclude the origin. The optimality theorem is more sensitive: it needs R(x) positive definite as a matrix in the input space to define R^{-1} and to complete the square. Scalar checks over state directions do not provide that. So the certificates described in Section 4.2 do not imply the antecedents of Theorems 5 and 6 as written.\n\nThe good news is that the gap is repairable. For scalar inputs, verifying R(x)>0 directly with SMT is easy, and Δ≻0 can be checked with the quadratic form on a set containing a neighborhood of the origin. For MIMO, one would need eigenvalue or SDP checks. The core approach is not invalidated; the verification section just oversells what it proves.\n\nOne more thing: the empirical section claims OURS beats NODE on optimality, but Table 2 shows NODE achieving lower cumulative cost on the dynamic pendulum and the rod-on-cart. That overstatement should be corrected. There are also several typos and notational inconsistencies (R's codomain, the integrand in Theorem 6) that a careful revision should clean up.\n\nWho is this for? People working on learning-based control with formal certificates will appreciate the training pipeline and the benchmarks. It deserves a serious referee, but it needs major revision on the verification argument and the empirical claims. I would send it out.","headline":"The learning pipeline is useful and the experiments are promising, but the SMT verification as written does not certify the matrix definiteness conditions that the stability and optimality theorems require; the gap is concrete and repairable, and the paper deserves a serious referee after revision.","tokens_in":16487,"tokens_out":7771,"would_cite":true,"duration_ms":70605,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper constructs a neural feedback controller $\\pi(x) = -R(x)^{-1}S(x)^{\\top}x$ and proves, under learned dissipativity certificates, that it asymptotically stabilizes the closed loop and is optimal for an explicitly built…","keywords":["learning-based control","input-output dissipativity","storage function","optimal control","inverse optimality","formal verification","neural controller","stability guarantees"],"falsifier":"Run the verifier on a two-state system with $R(x) = \\begin{bmatrix}1&2\\\\2&1\\end{bmatrix}$ and a region contained in a small ball around $(1,1)$. Within that region $x^{\\top}R x > 0$ for every $x$, but $R$ is indefinite because it has eigenvalue $-1$ along $(1,-1)$, which lies outside the region, so the paper's scalar check would certify $R(x)\\succ0$ even though the positive-definiteness assumption of Theorems 5 and 6 is false. At $x=0$ the same scalar conditions read $0>0$ and are trivially unsatisfiable, so the verification protocol must either exclude the origin or switch to genuine matrix definiteness checks.","tokens_in":15281,"feed_emoji":"🎛️","tokens_out":11802,"duration_ms":111743,"temperature":0.7,"pith_summary":"This paper tries to close the gap between learned and certified controllers: it shows that a neural feedback derived from an input-output dissipativity certificate is not just stable but provably optimal for an infinite-horizon cost that is constructed alongside the controller. The recipe is to learn a storage function $V(x)$ — an energy-like Lyapunov candidate — together with state-dependent matrices $Q(x)$, $S(x)$, $R(x)$ that define how much energy the system can absorb from each state-input pair. If the learned functions pass a formal verifier, the explicit formula $\\pi(x) = -R(x)^{-1}S(x)^{\\top}x$ stabilizes the system and solves an optimal control problem whose value function is exactly $V(x)$. A cost-shaping term lets the user point the optimality certificate toward a desired performance objective. A sympathetic reader would take the contribution to be a design-with-guarantees alternative to rollout-trained neural controllers, with numerical experiments showing it outperforms neural Lyapunov baselines in cumulative cost.","feed_headline":"A neural controller formula certifies stability and cost-optimality","feed_subtitle":"Learning a storage function and supply rate yields a provably stabilizing, cost-optimal feedback.","key_machinery":"The load-bearing identity is the completion of squares in the dissipation inequality: with $v = u + R(x)^{-1}S(x)^{\\top}x$, the supply rate becomes $x^{\\top}\\Delta(x)x + v^{\\top}R(x)v$, and the feedback that zeros $v$ is $\\pi = -R^{-1}S^{\\top}x$. The matrix $\\Delta = S R^{-1} S^{\\top} - Q$ measures the excess of the cross and control terms over the state term, and it is the margin that makes $V$ a Lyapunov function. A second ingredient is the matrix inequality (22), whose positive definiteness is equivalent to the $u$-dependent dissipation inequality, reducing the sampling dimension; the same Schur-complement form is what the SMT verifier checks. The cost-shaping loss (29) aligns the constructed running cost with a user-specified objective, so the optimality certificate is with respect to the user's intended performance metric.","core_discovery":"The central result is Theorem 6, stated on the paper's own terms: if $V(x)>0$ and $Q,S,R$ satisfy the dissipation inequality $\\partial_x V\\,[f(x)+g(x)u] \\le x^{\\top}Q(x)x + 2x^{\\top}S(x)u + u^{\\top}R(x)u$ for all $x,u$, with $R(x)>0$ and $\\Delta(x)=S(x)R(x)^{-1}S(x)^{\\top}-Q(x)>0$, then $\\pi(x)=-R(x)^{-1}S(x)^{\\top}x$ is the optimal feedback for the infinite-horizon problem with running cost $\\tilde{l}(x,u)+u^{\\top}R(x)u+x^{\\top}\\Delta(x)x$, where $\\tilde{l}$ captures the residual of the dissipation inequality, and $V(x)$ is the value function. Theorem 5 is the companion stability statement: the same controller gives closed-loop decrease $\\dot{V}(x) \\le -x^{\\top}\\Delta(x)x < 0$. Proposition 8 re-expresses the dissipation inequality as a matrix inequality $M(x)\\succ 0$ that depends on $x$ alone, so training and verification sample states instead of state-input pairs. Under extra equalities, Proposition 7 reduces the optimality cost to $u^{\\top}R(x)u + x^{\\top}\\Delta(x)x$.","pith_inferences":["Beyond the paper: the optimality theorem is inverse optimality — it constructs a cost for which the stabilizing feedback is optimal; it does not say the learned controller is optimal for an arbitrary user cost, only that the shaped cost approximates it, and the paper does not quantify the suboptimality gap when those differ.","Beyond the paper: the scalar verification shortcuts in Section 4.2 are safe only for scalar-input systems and state regions that contain all state directions; for multi-input plants the theorems require checking matrix positive definiteness, so the framework would need a semidefinite-capable verifier or a parameterization that guarantees $R(x)\\succ0$ and $\\Delta(x)\\succ0$ by construction.","Beyond the paper: treating $V$ simultaneously as a storage function and a value function suggests a natural way to certify suboptimality — the residual between the learned cost and the true user cost is measurable and could be quoted as a certificate or used to drive further training."],"forward_implications":["A trained and verified tuple $(V,Q,S,R)$ yields a controller with an explicit Lyapunov function $V$ on the verified region, so stability is certified rather than inferred from rollouts.","The same controller is optimal for a cost the paper explicitly constructs, and Proposition 7 identifies conditions under which that cost is exactly $u^{\\top}R(x)u + x^{\\top}\\Delta(x)x$.","Cost shaping (29) lets the designer steer the constructed running cost toward a user-defined $l(x,u)$, making the optimality guarantee meaningful for a chosen objective.","Because the certificate is input-output based, the resulting controller stabilizes any system sharing the same dissipativity property, not only the nominal training dynamics.","The framework extends to dynamic controllers through an augmented state, which the paper shows generalizes nonlinear PI control."],"supporting_citations":[{"why":"Defines dissipativity, storage functions and supply rates; the theoretical foundation the controller construction relies on.","marker":"[21]"},{"why":"Supplies the dissipativity-based feedback stabilization result that Theorem 5 is built on, including the structured controller form.","marker":"[25]"},{"why":"Connects dissipativity to inverse optimal control, the basis for the optimality claim of Theorem 6.","marker":"[22]"},{"why":"Provides the counterexample-guided inductive synthesis loop used by the training and verification algorithm.","marker":"[16]"},{"why":"The SMT solver used to formally verify the learned storage and supply rate functions.","marker":"[17]"},{"why":"Neural Lyapunov control baseline that this work compares against in the optimality experiments.","marker":"[11]"},{"why":"Supplies the rod-on-cart benchmark and the closed-loop dissipativity formulation extended here to learning.","marker":"[28]"},{"why":"The neural PI control framework that the paper shows is a special case of its dynamic controller extension.","marker":"[27]"}],"fun_headline_variants":["Dissipativity-trained neural controllers with stability and optimality proofs","Neural feedback with formal stability and cost-optimality guarantees","Stable and optimal neural control via learned dissipation functions","Certified neural controllers: stability and optimality from dissipation"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that verifying the scalar inequalities $x^{\\top}\\Delta(x)x > 0$ and $x^{\\top}R(x)x > 0$ over the state region certifies the matrix positive-definiteness conditions $\\Delta(x)\\succ0$ and $R(x)\\succ0$ required by Theorems 5 and 6, an equivalence that fails when the region does not contain all state directions, when the system has multiple inputs, or at $x=0$.","fun_headline_variants_meta":{"raw":{"variants":["Dissipativity-trained neural controllers with stability and optimality proofs","Neural feedback with formal stability and cost-optimality guarantees","Stable and optimal neural control via learned dissipation functions","Certified neural controllers: stability and optimality from dissipation"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000234,"raw_usage":{"total_tokens":1508,"prompt_tokens":968,"completion_tokens":540,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":584,"completion_tokens_details":{"reasoning_tokens":472}},"tokens_in":584,"tokens_out":540,"duration_ms":5364,"temperature":1.0,"reasoning_tokens":472,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T05:55:31.443214+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the verifier on a two-state system with $R(x) = \\begin{bmatrix}1&2\\\\2&1\\end{bmatrix}$ and a region contained in a small ball around $(1,1)$. Within that region $x^{\\top}R x > 0$ for every $x$, but $R$ is indefinite because it has eigenvalue $-1$ along $(1,-1)$, which lies outside the region, so the paper's scalar check would certify $R(x)\\succ0$ even though the positive-definiteness assumption of Theorems 5 and 6 is false. At $x=0$ the same scalar conditions read $0>0$ and are trivially unsatisfiable, so the verification protocol must either exclude the origin or switch to genuine matrix definiteness checks.","supporting_citations":[{"cited_title":"Dissipative dynamical systems part i: General theory,","cited_arxiv_id":null,"evidence_quote":"Defines dissipativity, storage functions and supply rates; the theoretical foundation the controller construction relies on."},{"cited_title":"Necessary and sufficient dissipativity- based conditions for feedback stabilization,","cited_arxiv_id":null,"evidence_quote":"Supplies the dissipativity-based feedback stabilization result that Theorem 5 is built on, including the structured controller form."},{"cited_title":"Nonlinear regulator theory and an inverse optimal control problem,","cited_arxiv_id":null,"evidence_quote":"Connects dissipativity to inverse optimal control, the basis for the optimality claim of Theorem 6."},{"cited_title":"Counterexample guided inductive synthesis modulo theories,","cited_arxiv_id":null,"evidence_quote":"Provides the counterexample-guided inductive synthesis loop used by the training and verification algorithm."},{"cited_title":"dreal: An smt solver for nonlinear theories over the reals,","cited_arxiv_id":null,"evidence_quote":"The SMT solver used to formally verify the learned storage and supply rate functions."},{"cited_title":"Neural lyapunov control,","cited_arxiv_id":null,"evidence_quote":"Neural Lyapunov control baseline that this work compares against in the optimality experiments."},{"cited_title":"Structured neural- pi control with end-to-end stability and output tracking guarantees,","cited_arxiv_id":null,"evidence_quote":"The neural PI control framework that the paper shows is a special case of its dynamic controller extension."}],"review_version":1}