{"id":"23125fac-e3fd-41b4-a030-18931676e761","arxiv_id":"2508.21213","paper_version":1,"verdict":"REJECT","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"A PINN trained on the stochastic Zubov equation, with SMT-based verification of the stochastic Lyapunov condition, produces formally certified probabilistic regions of attraction for stochastic systems.","lead":"This paper trains neural Lyapunov functions on a stochastic version of Zubov's equation to estimate regions of attraction for noisy nonlinear systems, then uses an SMT solver to formally verify the stochastic Lyapunov conditions. The method is demonstrated on a reversed Van der Pol oscillator, where it certifies a larger probabilistic region of attraction than sum-of-squares and quadratic Lyapunov functions.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 14's proof silently assumes LV<0 on Vc1\\{0}; its stated hypotheses allow LV>0 there, and a 1D deterministic example satisfies all assumptions yet violates the conclusion.","rationale":"The reader's weakest-assumption field emphasizes the lack of a PINN error bound, which is a real limitation but secondary. Their rationale also flags that Theorem 14 is not proven as stated, and that is the sharper problem. My counterexample shows the theorem's stated assumptions do not imply its conclusion: the proof uses Theorem 13(ii) for V, whose hypotheses are only present in the application (a quadratic Lyapunov function from Proposition 11), not in Theorem 14. Since the paper's main claimed contribution is precisely these sufficient conditions, this is a central mathematical flaw. The flaw is fixable by adding the missing local Lyapunov assumption on V, and the numerical example may still be valid, but the theorem as written is unsound. This confirms the reader's REJECT verdict, so no verdict adjustment is needed. The independent numerical experiment is a useful sanity check but cannot compensate for an incorrect theorem; a reproducible verification script would help, but the theorem gap is the decisive issue.","tokens_in":13155,"tokens_out":15298,"duration_ms":150176,"concrete_test":"Run the following analytic check. For the 1D system dx=(x−2x^3)dt, take V=W=x^2, c1=β1=0.75, c2=β2=1.5. Compute LV and the deterministic flow, and confirm that: (i) V satisfies Theorem 13(iii) on Vc2\\Vc1; (ii) Wβ1⊆Vc1⊆Vc2⊆Wβ2; (iii) at x0=1/√2, the true probability of convergence to 0 is 0; (iv) the Theorem 14 lower bound is positive. If all four points hold, Theorem 14 is false as stated. If not, identify exactly which hypothesis is violated. This check isolates the gap without relying on training or SMT details.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central sufficient condition is Theorem 14, but the proof upgrades its hypotheses without stating them. The theorem assumes only that V satisfies the hypotheses of Theorem 13(iii), i.e., existence of 0<c1<c2 and ζ>0 with LV≤−ζ on Vc2\\Vc1. To obtain convergence after the trajectory first enters Vc1, the proof invokes Theorem 13(ii), which requires LV<0 on all of Vc2\\{0} and positive definiteness of V. Nothing in the stated hypotheses controls LV inside Vc1.\n\nThis is not a cosmetic omission. For the smooth deterministic system dx=(x−2x^3)dt, take D=R, V(x)=W(x)=x^2, c1=β1=0.75, c2=β2=1.5. Then V satisfies Theorem 13(iii) on Vc2\\Vc1 because LV=2x^2(1−2x^2)≤−0.75 there; Wβ1⊆Vc1⊆Vc2⊆Wβ2; and all smoothness assumptions hold. But inside Vc1, LV>0 (e.g. at x^2=0.3), and every nonzero deterministic trajectory converges to ±1/√2, not to 0. For x0=1/√2, W(x0)=0.5, so the claimed lower bound is (1−0.75/1.5)(1−0.5/1.5)≈0.333, while the true probability of convergence to 0 is 0. Thus Theorem 14's sufficient conditions are not sufficient as stated. The missing assumption—e.g., that V also satisfies Theorem 13(ii) on Vc2—is load-bearing for the central verification claim.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper develops a physics-informed neural network (PINN) approach to approximate the value function of a stochastic Zubov equation, yielding a learned neural Lyapunov function for the probabilistic region of attraction (ROA) of stochastic nonlinear systems. It then derives sufficient conditions, checkable by SMT solvers, for stochastic stability and probabilistic ROA. The main theoretical result is Theorem 14, which combines a locally verified quadratic Lyapunov function V with a neural Lyapunov function W that satisfies a Lyapunov inequality on an annulus W^{β2}\\W^{β1}, in order to certify a probability lower bound on convergence from an enlarged set W^{β2}. Numerical experiments on a reversed Van der Pol oscillator illustrate that the method yields larger verified probabilistic ROAs than SOS-based Lyapunov functions.","tokens_in":13617,"tokens_out":33503,"duration_ms":334575,"significance":"If correct, the paper would provide a formally verifiable, SMT-based certification procedure for probabilistic region-of-attraction estimates using neural Lyapunov functions, going beyond SOS methods and capturing larger regions in the demonstrated example. The verification approach is independent of the training procedure: the SMT solver checks the trained function itself, not the training objective, so there is no circularity of fitted constants. The numerical study is concrete and reproducible in principle. However, the central sufficient condition in Theorem 14 is false as stated; the proof silently uses a much stronger hypothesis than the theorem assumes. This is a load-bearing flaw that affects the main theoretical claim and the soundness of Proposition 15.","major_comments":[{"comment":"The theorem is false as stated because its proof upgrades the hypothesis without justification. The theorem assumes only that V satisfies Theorem 13 iii), i.e., LV ≤ -ζ on the annulus V^{c2}\\V^{c1}. The proof, however, invokes Theorem 13 ii) to conclude convergence to 0 after the trajectory enters V^{c1}, which requires LV < 0 on all of V^{c2}\\{0} and positive definiteness of V. These stronger properties are not implied by the stated assumptions. A deterministic counterexample satisfies all hypotheses but violates the conclusion: take dx = (x - 2x^3)dt, V=W=x^2, c1=β1=0.75, c2=β2=1.5. Then LV = 2x^2(1-2x^2) ≤ -0.75 on V^{c2}\\V^{c1}, all sublevel inclusions hold, and all smoothness assumptions are met. But for x0 = 1/√2 (W(x0)=0.5), the claimed lower bound is (1-0.75/1.5)(1-0.5/1.5) ≈ 0.333, whereas the deterministic trajectory converges to ±1/√2, so the probability of convergence to 0 is","section":"Section IV-B, Theorem 14"},{"comment":"The proof contains an unjustified step: 'With a slightly modified argument as in the proof of part ii), we can show that P{Xt ∈ Vc2, ∀t ≥ t0} ≥ 1 - V(x0)/c2.' This conclusion does not follow from the assumptions, because LV may be positive inside Vc1, so the supermartingale argument of part i) is not available on the entire sublevel set Vc2. The proof needs a direct treatment of the exit probability, e.g., an optional-stopping argument applied only on the annulus, and a separate argument controlling the behavior after entering Vc1. As written, the proof is incomplete; the authors should either provide a correct proof of iii) or weaken the statement.","section":"Section IV-B, proof of Theorem 13 iii)"},{"comment":"The probability lower bound p(x0) is not supported by the results as stated. For W(x0) < β1, the proposition claims P(x0) ≥ 1 - V(x0)/c2, attributing this to Theorem 13 iii), but Theorem 13 iii) applies only to x0 ∈ Vc2\\Vc1, whereas W(x0)<β1 places x0 inside Vc1. Moreover, the proof of Proposition 15 relies on Theorem 14, which is false as stated (see first major comment). After repairing Theorem 14 by adding the assumption that V satisfies Theorem 13 ii) on Vc2, Proposition 15 can be made valid, but it must be restated and reproved accordingly.","section":"Section IV-B, Proposition 15"}],"minor_comments":[{"comment":"Typo: 'preform' should be 'perform'.","section":"Section V, Example 17"},{"comment":"In the continuity argument, '1 − V (x0)' should read '1 − V (x0)/c2'.","section":"Section IV-B, Proposition 15 proof"},{"comment":"The black curve is described as 'the region where the neural Lyapunov function is not well-trained'; as a curve it is presumably the boundary of such a region. Please clarify.","section":"Figure 1 caption"},{"comment":"The statement 'W(x) < 1 if and only if LW(x) < 0 when x ≠ 0' presumes W is positive definite and sufficiently smooth; the viscosity solution may not be C^2. This is used as intuition, but should be phrased more carefully.","section":"Section II-B"}],"recommendation":"major_revision","confidential_remarks":"The paper's main theoretical result has a statement-proof mismatch that makes Theorem 14 false as stated. The counterexample is simple and convincing. The error is fixable by adding the stronger but natural hypothesis that the quadratic Lyapunov function V satisfies LV<0 on the entire sublevel set V^{c2}, which is what the numerical experiment actually verifies. I therefore believe a major revision is appropriate rather than outright rejection, provided the authors correct the theorem, its proof, and the dependent Proposition 15. The paper is also highly self-referential (refs [7], [8], [13]); while not itself a technical flaw, the novelty relative to those works should be articulated more clearly."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper extends neural Lyapunov verification to stochastic systems by training a PINN on the stochastic Zubov equation and then using dReal to verify the learned function. The idea is timely and the combination is new as far as I can tell. Proposition 11, the local stability condition, looks sound. That said, the central contribution, Theorem 14, is not valid as stated. The proof invokes Theorem 13(ii)—which requires LV<0 on the entire sublevel set V^{c2}\\{0}—but the theorem's hypotheses only give LV≤−ζ on the annulus V^{c2}\\V^{c1}. I checked the stress-test counterexample and it holds up: for the deterministic scalar system dx=(x−2x^3)dt with V=W=x^2, c1=β1=0.75, c2=β2=1.5, all hypotheses are satisfied, yet trajectories starting inside V^{c1} converge to ±1/√2, not 0. The claimed lower bound of (1−c1/c2)(1−W(x0)/β2) is then ~1/3 for x0^2=0.5, while the true convergence probability to 0 is 0. Deterministic systems are a special case, so this is not a contrived edge case.\n\nThis is not a cosmetic gap: Theorem 14 is what enables the two-Lyapunov enlargement argument and the piecewise probability bound in Proposition 15. Without an additional assumption, e.g., that V also satisfies Theorem 13(ii) on V^{c2}, the paper's verification results are unsupported. The numerical section also gives only a single 2D example and no code or verification scripts, which makes it hard to reproduce. The abstract's \"largest probabilistic ROA\" language overstates what is actually certified, since the verified region is a sublevel set where the conditions hold, not the true C.\n\nWhat the paper does well: the PINN training with data from (3) is a sensible extension of prior deterministic work, and the local verification via the stochastic Lyapunov equation seems correct. The writing is clear and the related work is well positioned.\n\nBottom line: this is a serious paper with a load-bearing flaw. It deserves peer review, but only with the expectation of major revision and a corrected theorem. I would not cite it in its current form.","headline":"Theorem 14 is false as stated — a deterministic 1D example satisfies its hypotheses yet violates the conclusion, so the two-Lyapunov verification claim is currently unsupported.","tokens_in":14082,"tokens_out":4254,"would_cite":false,"duration_ms":38062,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["93D30","93E15","60H10","68T07"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper claims that a physics-informed neural network solving the stochastic Zubov equation, combined with satisfiability-modulo-theories verification, certifies probabilistic regions of attraction that are larger than those obtained with","keywords":["stochastic Zubov equation","probabilistic region of attraction","neural Lyapunov functions","physics-informed neural networks","SMT verification","stochastic Lyapunov stability","stochastic differential equations"],"falsifier":"On a stochastic system where the true Zubov solution can be computed accurately (dense Monte-Carlo or a fine numerical PDE solve), run the training-plus-SMT pipeline. If the solver reports no constants $\\beta_1 < \\beta_2$ and $c_1 < c_2$ satisfying $W^{\\beta_1} \\subseteq V^{c_1} \\subseteq V^{c_2} \\subseteq W^{\\beta_2}$ with $L W_{NN} \\leq -\\zeta$ on the annulus, while the true probabilistic region of attraction is large, the claimed enlargement mechanism has failed. Alternatively, take a point inside the verified $W^{\\beta_2}$ whose predicted bound from Proposition 15 is high and simulate many trajectories: an observed convergence frequency below that bound would contradict th","tokens_in":1722,"feed_emoji":"✅","tokens_out":1812,"duration_ms":80211,"temperature":0.7,"texified_at":"2026-08-05T20:17:41.433107+00:00","pith_summary":"The paper claims that a physics-informed neural network approximating the stochastic Zubov equation can produce a Lyapunov function whose probabilistic region of attraction is certified by SMT solvers, and that this certified region is larger than what sum-of-squares or quadratic Lyapunov functions give on a nonlinear stochastic example. The central move is to prove sufficient conditions under which a quadratic Lyapunov function handles the small neighborhood of the origin and a separately trained neural function handles the outer shell; nesting the two sublevel sets yields a pointwise lower bound on the probability of convergence. If the claim holds, engineers get a practical route from unverified neural candidates to formal stochastic stability guarantees, complete with a probability for each initial condition.","texify_model":"deepseek-v4-flash","texify_usage":{"total_tokens":6891,"prompt_tokens":825,"completion_tokens":6066,"prompt_tokens_details":{"cached_tokens":0},"prompt_cache_hit_tokens":0,"prompt_cache_miss_tokens":825,"completion_tokens_details":{"reasoning_tokens":5228}},"feed_headline":"Neural Lyapunov certificates enlarge probabilistic attraction regions","feed_subtitle":"A stochastic Zubov equation solver plus satisfiability-modulo-theories checks verifies wider p-ROAs than SOS methods.","key_machinery":"Stochastic Zubov equation and the annulus-nesting condition. $W(x) = 1 - \\mathbb{E}\\left[\\exp\\left(-\\int g(X_s(x))\\,ds\\right)\\right]$ solves $LW = -g(1-W)$ and characterizes the probabilistic region of attraction as $\\{W<1\\}$. The theorem that carries the argument is the nesting $W^{\\beta_1} \\subseteq V^{c_1} \\subseteq V^{c_2} \\subseteq W^{\\beta_2}$ with $LW \\leq -\\zeta$ on the annulus, which lets two Lyapunov functions cooperate: one local near the origin, one global on the shell, and yields the product lower bound on attraction probability.","core_discovery":"The paper's discovery is a verification theorem (Theorem 14) plus a training pipeline. Training solves the stochastic Zubov equation $LW = -g(1-W)$ with $W(0)=0$; its viscosity solution's strict sublevel set $\\{W<1\\}$ is exactly the set of initial conditions attracted with positive probability. Verification does not try to check $LW<0$ everywhere. Instead, after a quadratic Lyapunov function $V$ has been certified on $V^{c_2}$, a neural $W$ is certified only on the annulus $W^{\\beta_2} \\setminus W^{\\beta_1}$, with $W^{\\beta_1} \\subset V^{c_1} \\subset V^{c_2} \\subset W^{\\beta_2}$. Then every $x_0 \\in W^{\\beta_2}$ converges with probability at least $\\left(1 - \\frac{c_1}{c_2}\\right)\\left(1 - \\frac{W(x_0)}{\\beta_2}\\right)$. The numerical example on a reversed Van der Pol oscillator shows the verified neural sublevel set exceeding the","pith_inferences":["Since no error bound links PINN training loss to the certified constants, one could interleave training with SMT queries: if the solver cannot find β1, β2, add collocation points inside the annulus and retrain, making the pipeline an anytime certification method; the paper does not explore this.","The same nesting could be iterated with a chain of Lyapunov functions, each certified on its own annulus, to enlarge the certified region further than two functions allow.","The probability lower bound in Proposition 15 is conservative; sampling from the certified region with rare-event estimators could tighten the practical p-ROA estimate, although the formal bound would remain the conservative certificate.","Theorem 13's exit-time argument is a supermartingale property that could be reused for finite-time reach-avoid or barrier-style specifications, not just asymptotic attraction."],"forward_implications":["Formal certificates replace simulation checks: every verified sublevel set W^{β2} comes with a probability bound for every initial condition inside it.","The method's verified region can extend beyond the deterministic region of attraction: on the example, stochastic effects stabilize some points outside the deterministic limit cycle.","Because the neural function only needs a negative Lyapunov derivative on an annulus, PINN training is relieved of the hardest part of reproducing the equilibrium singularity.","Applying the same verification pipeline to SOS and quadratic candidates yields smaller certified regions, indicating the Zubov-based candidate carries more of the true probabilistic region of attraction.","Any improvement in SMT solvers or in PINN accuracy translates directly into larger certified probabilistic regions without changing the theorem."],"supporting_citations":[{"why":"Introduces the stochastic Zubov equation and the probabilistic region of attraction characterization this paper builds on.","marker":"[16]"},{"why":"Establishes the unique viscosity solution and the identification of C with {W<1}, the theoretical basis for training W.","marker":"[17]"},{"why":"Supplies the PINN training scheme for neural Lyapunov functions and the SMT verification workflow adapted here to the stochastic setting.","marker":"[8]"},{"why":"Provides the satisfiability-modulo-theories solver dReal used to formally check the stochastic Lyapunov inequalities and sublevel-set inclusions.","marker":"[23]"},{"why":"Demonstrates learning and verification of maximal neural Lyapunov functions via Zubov's equation, the direct predecessor of this approach.","marker":"[7]"},{"why":"Gives the stochastic Lyapunov theorems used to translate LV<0 into stochastic asymptotic stability.","marker":"[25]"},{"why":"Supplies the stochastic Lyapunov-barrier reach-avoid-stay framework reformulated as Theorem 13 for probabilistic safe stability.","marker":"[28]"},{"why":"Provides local Lyapunov functions for stochastic systems by linearization, underlying Proposition 11.","marker":"[27]"}],"fun_headline_variants":["Larger verified stochastic attraction basins via neural Lyapunov","SMT-verified neural Lyapunov proves probabilistic stability","Neural Zubov solver widens verified attraction regions","Formal proof of larger probabilistic ROA with neural Lyapunov","Verified p-ROA beats SOS via stochastic Zubov and neural Lyapunov"],"cache_read_input_tokens":15744,"weakest_assumption_plain":"The certification depends on the trained neural network being close enough to the true stochastic Zubov solution that some annulus $W^{\\beta_2} \\setminus W^{\\beta_1}$ satisfies the stochastic Lyapunov inequality and nests around the verified quadratic region; the paper provides no error bound or training guarantee for this nearness.","fun_headline_variants_meta":{"raw":{"variants":["Larger verified stochastic attraction basins via neural Lyapunov","SMT-verified neural Lyapunov proves probabilistic stability","Neural Zubov solver widens verified attraction regions","Formal proof of larger probabilistic ROA with neural Lyapunov","Verified p-ROA beats SOS via stochastic Zubov and neural Lyapunov"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000537,"raw_usage":{"total_tokens":2404,"prompt_tokens":720,"completion_tokens":1684,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":464,"completion_tokens_details":{"reasoning_tokens":1595}},"tokens_in":464,"tokens_out":1684,"duration_ms":12754,"temperature":1.0,"reasoning_tokens":1595,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-05T14:29:52.850747+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"On a stochastic system where the true Zubov solution can be computed accurately (dense Monte-Carlo or a fine numerical PDE solve), run the training-plus-SMT pipeline. If the solver reports no constants $\\beta_1 < \\beta_2$ and $c_1 < c_2$ satisfying $W^{\\beta_1} \\subseteq V^{c_1} \\subseteq V^{c_2} \\subseteq W^{\\beta_2}$ with $L W_{NN} \\leq -\\zeta$ on the annulus, while the true probabilistic region of attraction is large, the claimed enlargement mechanism has failed. Alternatively, take a point inside the verified $W^{\\beta_2}$ whose predicted bound from Proposition 15 is high and simulate many trajectories: an observed convergence frequency below that bound would contradict th","supporting_citations":[{"cited_title":"A characterization of the domain of attraction for a locally exponentially stable stochastic system","cited_arxiv_id":null,"evidence_quote":"Introduces the stochastic Zubov equation and the probabilistic region of attraction characterization this paper builds on."},{"cited_title":"Characterizing attraction probabilities via the stochastic zubov equation","cited_arxiv_id":null,"evidence_quote":"Establishes the unique viscosity solution and the identification of C with {W<1}, the theoretical basis for training W."},{"cited_title":"Physics-informed neural network Lyapunov functions: PDE charac- terization, learning, and verification","cited_arxiv_id":null,"evidence_quote":"Supplies the PINN training scheme for neural Lyapunov functions and the SMT verification workflow adapted here to the stochastic setting."},{"cited_title":"dReal: An SMT solver for nonlinear theories over the reals","cited_arxiv_id":null,"evidence_quote":"Provides the satisfiability-modulo-theories solver dReal used to formally check the stochastic Lyapunov inequalities and sublevel-set inclusions."},{"cited_title":"Towards learning and verifying maximal neural Lyapunov functions","cited_arxiv_id":null,"evidence_quote":"Demonstrates learning and verification of maximal neural Lyapunov functions via Zubov's equation, the direct predecessor of this approach."},{"cited_title":"Stochastic Differential Equations and Applications","cited_arxiv_id":null,"evidence_quote":"Gives the stochastic Lyapunov theorems used to translate LV<0 into stochastic asymptotic stability."},{"cited_title":"Stochastic Lyapunov-barrier functions for robust probabilistic reach-avoid-stay specifications","cited_arxiv_id":null,"evidence_quote":"Supplies the stochastic Lyapunov-barrier reach-avoid-stay framework reformulated as Theorem 13 for probabilistic safe stability."},{"cited_title":"Local Lyapunov functions for nonlinear stochastic differen- tial equations by linearization","cited_arxiv_id":null,"evidence_quote":"Provides local Lyapunov functions for stochastic systems by linearization, underlying Proposition 11."}],"review_version":1}