{"id":"e39eeb74-3ec0-434f-8a95-a49a3bee53cc","arxiv_id":"2412.17432","paper_version":1,"verdict":"REJECT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"high","formal_verification":"none","parameter_count":4,"one_line_summary":"A neural network can be trained and then formally verified to give lower-bound probabilities for reach-avoid-stay specifications of stochastic differential equations.","lead":"This paper trains neural networks to act as mathematical certificates that bound the probability a continuous-time stochastic control system reaches a target, avoids hazards, and stays safe. It is the first such neural-certificate framework for continuous-time stochastic systems, offering formal guarantees beyond discrete-time approximations.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The stay-property proof of Theorem 1 relies on an unjustified bound E[V(0,X_ψ)]≤αS; without it, the claimed δ=1−αS/βS is not established.","rationale":"The paper's central claim is Theorem 1: a function satisfying the six conditions of Definition 2 certifies an RAS specification with the stated ε and δ. The reader's weakest-assumption analysis identifies the stay-property step of the proof as the point where the argument breaks. My reading of the technical appendix confirms this: the proof bounds the probability of leaving the sublevel set after ψ by assuming the restarted supermartingale has initial expectation at most αS, but the only available bound is αRA, and the stopping time ψ can exit through the high side. This is not a minor typo, because the entire δ guarantee depends on an inequality of the form P(sup_{t≥ψ} V ≥ βS) ≤ αS/βS, and no chain of the stated conditions produces that inequality. The secondary concern about the verification step is also real: Algorithm 1 checks the decrease condition only on cells with Vlow > αS and Vup ≤ βRA, so cells crossing the αS boundary or the X⋆ boundary may contain violations of Definition 2. However, the theorem gap is the more fundamental issue, since the algorithm's output inherits the theorem's quantitative soundness. I do not see an internal contradiction that makes the whole framework false; a revised proof using a different stopping time or additional assumptions might salvage a similar result. But as written, the formal probabilistic guarantees for persistence are not derived, so the reader's REJECT verdict is appropriate.","tokens_in":18223,"tokens_out":14438,"duration_ms":150171,"concrete_test":"Re-derive the stay-property bound rigorously from Definition 2: let ρ = inf{t ≥ ψ : V(t,X_{π,t}) = αS} and apply the strong Markov property and the maximal inequality to the process restarted at ρ, stopped at the first time V ≥ βS. Check whether the resulting unconditional bound is P(sup_{t≥ψ} V ≥ βS) ≤ αS/βS or contains an additional term of the form P(V(ψ,X_ψ) ≥ βRA) ≥ 0. If the additional term appears, Theorem 1's δ is not a consequence of the stated conditions, and the empirical certificate guarantees in Section 'Experiments' are not formally justified.","verdict_should_be":"UNCHANGED","load_bearing_attack":"In the Technical Appendix proof of Theorem 1, after defining the stopping time ψ as the first exit from [αS,βRA), the proof asserts P(sup_{t≥ψ} V(t,X_{π,t}) ≥ βS) ≤ (1/βS) E[V(0,X_{π,ψ})] ≤ αS/βS. The first inequality is an application of the maximal inequality to a time-shifted process, but the initial value of that shifted process is V(ψ,X_{π,ψ}), not V(0,X_{π,ψ}). The second inequality is not derived from Definition 2: optional stopping only gives E[V(ψ,X_{π,ψ})] ≤ V(0,x0) ≤ αRA, and no condition in Definition 2 bounds this expectation by αS. Since ψ can exit the interval through the high side, the event {V(ψ,X_ψ) ≥ βRA} has positive probability bounded only by αRA/βRA, and the arguments in the proof do not eliminate its contribution to the escape probability. The subsequent decomposition of {sup_{t≥ψ} V(t,X_π,t) < βS} is also algebraically false, although a simpler subset argument would suffice. Because the stay guarantee δ is the direct product of this step, the central quantitative claim of the paper is unsupported as written. The framework may be repairable by conditioning on the first post-ψ hit of level αS, but that repair would add an extra term and would not yield the stated bound without additional assumptions.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a framework for neural certificate-based verification of continuous-time stochastic dynamical systems against probabilistic reach-avoid-stay (RAS) specifications. The main theoretical contribution is Theorem 1, which states that a function V satisfying six conditions (nonnegativity, initial, safety, decrease, goal, stay) with constants αS < βS < αRA < βRA certifies the specification with avoidance probability ε = 1 - αRA/βRA and stay probability δ = 1 - αS/βS. The paper also presents a training algorithm that samples from the dynamics and an interval-bound-propagation (IBP) verifier, with experiments on an inverted pendulum and a bivariate geometric Brownian motion.","tokens_in":18569,"tokens_out":13661,"duration_ms":120966,"significance":"If the proof of Theorem 1 were correct, the paper would make a substantial contribution: it would extend neural supermartingale certificates to continuous-time SDEs, provide quantitative probabilistic guarantees, and include a reproducible prototype with code. The claimed first-ness of continuous-time neural supermartingale certification is plausible based on the related work review. However, the stay-property proof in the Technical Appendix contains a load-bearing gap, and the training and verification pipeline has internal inconsistencies. The central quantitative claim (the stay probability δ) is therefore not established as written.","major_comments":[{"comment":"The proof asserts P(sup_{t≥ψ} V(t,X_{π,t}) ≥ βS) ≤ (1/βS) E[V(0,X_{π,ψ})] ≤ αS/βS. The first inequality misapplies Proposition 5: after shifting time by ψ, the initial value of the shifted process is V(ψ,X_{π,ψ}), not V(0,X_{π,ψ}). The second inequality is not derived from Definition 2: optional stopping applied to the ψ-stopped supermartingale gives E[V(ψ,X_{π,ψ})] ≤ V(0,x0) ≤ αRA, and no condition in Definition 2 bounds this expectation by αS. Since ψ can exit the interval [αS,βRA) through the high side with probability only bounded by αRA/βRA, the contribution of that exit event to the expectation is not controlled by αS. Consequently, the stated stay probability δ = 1 - αS/βS is unsupported.","section":"Technical Appendix, Proof of Theorem 1 (stay part)"},{"comment":"The decomposition of the complement of {sup_{t≥ψ} V ≥ βS} as {∀t≥ψ: V < βS} ∩ {∄γ < βS: ∀t≥ψ: V < γ} is false: the second clause is equivalent to sup_{t≥ψ} V ≥ βS, so the intersection is the null event {sup = βS}, not the complement. The intended conclusion P(∀t≥ψ: V < βS) ≥ 1 - αS/βS would follow directly from the maximal inequality, but the erroneous decomposition makes the argument invalid as written.","section":"Technical Appendix, Proof of Theorem 1 (opposite event)"},{"comment":"The goal loss L⋆ = Σ_{x∈B∩X⋆} (βS - Vθ(x))_+ penalizes the certificate for being below βS inside the target set. This is the reverse of the goal condition (Definition 2, condition 5), which requires the existence of a sublevel set L^-_{βS}(V) within X⋆, i.e., values V ≤ βS somewhere in X⋆. The intended penalty should be (Vθ(x) - βS)_+. As written, the training objective drives Vθ away from satisfying the goal condition, so Algorithm 1 cannot learn a certificate in the direction required by Theorem 1.","section":"Eq. (13), Training"},{"comment":"The generator decrease/stay conditions are checked only on cells with Vlow(C) > αS and Vup(C) ≤ βRA. Cells that intersect the level set {V = αS} or {V = βRA} are excluded and never split, although Definition 2 requires GπV ≤ -ζ (and GπV ≤ -ξ) on the full sets L^-_{βRA}\\int X⋆ and X⋆∩L^-_{βRA}\\int L^-_{αS}. Thus a successful verification does not imply that the certificate conditions hold on the domains used in the proof of Theorem 1, so the formal guarantee is not discharged by the algorithm.","section":"Eq. (18), Verification"}],"minor_comments":[{"comment":"There are typos in this appendix: 'recurreny citerion' should be 'recurrence criterion', and the statement 'β ≤ ρ' in Lemma 2 should read 'αS ≤ βRA'.","section":"Technical Appendix, Proposition 2 and Lemma 2"},{"comment":"The entire paragraph on the 'opposite event' could be removed, since the maximal inequality already gives the desired bound directly; as written it is confusing and mathematically incorrect.","section":"Technical Appendix, Proof of Theorem 1 (opposite event)"},{"comment":"The goal-condition verification only checks V ≥ βS on cells intersecting ∂X⋆. To establish L^-_{βS} ⊆ X⋆ one needs a lower bound on V on all of X \\ X⋆, or an explicit topological assumption ensuring that a sublevel set crossing outside X⋆ must intersect ∂X⋆.","section":"Eq. (17), Verification"},{"comment":"The statement 'we can fix either αRA or βRA beforehand' is unclear, since the ratios are fixed by the specification; consider rewording to explain how the free scaling is used.","section":"Remark 3"}],"recommendation":"reject","confidential_remarks":"The loss-function sign error in Eq. (13) is concerning because it suggests the reported experimental successes may not have been obtained with the algorithm as written; please ask the authors to double-check the code and the equation. The stay-property gap is the primary reason for rejection: the central quantitative claim of Theorem 1 is not established as stated, and the verification algorithm is incomplete on boundary-crossing cells. A revision would need to either prove a modified bound with additional assumptions or weaken the theorem accordingly."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Two things worth knowing about arXiv:2412.17432. First, it does something genuinely new: it extends neural supermartingale certificates to continuous-time stochastic systems, with a training pipeline and an interval-bound-propagation verifier that checks the certificate conditions independently of the training loss. Second, the proof of Theorem 1 has a real gap in the stay-property part, and as written the claimed guarantee δ = 1 − αS/βS is not established. The reach-avoid part looks sound; the stay part does not.\n\nCredit where it is due. The framework is a sensible bridge between discrete-time neural supermartingale certificates and continuous-time neural Lyapunov methods, and the paper is honest that no prior work gives provable continuous-time stochastic guarantees with neural certificates. The code is released, the experiments cover two nontrivial benchmarks with neural policies, and the verification step uses IBP rather than trusting the learned function. Circularity is not a real concern here: the probability bounds are derived from the certificate conditions, not fitted to data.\n\nThe soft spot is in the technical appendix, proof of Theorem 1. After defining ψ as the first exit from [αS, βRA), the proof applies the maximal inequality to a time-shifted process and asserts E[V(0, X_{π,ψ})] ≤ αS. That is wrong on two counts. The shifted process starts at V(ψ, X_{π,ψ}), not V(0, X_{π,ψ}), and no condition in Definition 2 bounds that expectation by αS; optional stopping only gives E[V(ψ, X_{π,ψ})] ≤ V(0, x0) ≤ αRA. Since ψ can exit through the high side, the contribution of {V(ψ, X_ψ) ≥ βRA} to the escape probability is not eliminated. The subsequent decomposition of the complement event is also algebraically false, though a simpler subset argument would repair that piece. The net effect is that the quantitative stay guarantee δ is unsupported. This is a load-bearing flaw, not a cosmetic one.\n\nThe verification step has a secondary issue: the decrease condition is only checked on cells with Vlow > αS and Vup ≤ βRA, leaving regions near the αS boundary and the target boundary unverified. That is a practical concern and could be addressed with more exhaustive splitting or a different cell predicate, but it is minor compared to the proof gap.\n\nWho is this for? Researchers working on neural certificates for stochastic control and formal verification of learning-enabled systems. The paper is worth a serious referee because the idea is important and the flaw is plausibly repairable, perhaps by conditioning on the first post-ψ hit of level αS and paying an extra term, though the stated bound would need modification. My recommendation: send it to review, but expect major revision. Do not accept the theorem as proved.","headline":"New continuous-time neural supermartingale framework, but the stay-property proof has a load-bearing gap that invalidates the stated persistence bound as written.","tokens_in":19045,"tokens_out":2004,"would_cite":false,"duration_ms":19609,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["60H10","60G46","68Q60","93E15"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper introduces the first neural-certificate framework that yields formally certified probability bounds for reachability, avoidance, and persistence in continuous-time stochastic systems.","keywords":["neural certificates","supermartingale","continuous-time stochastic systems","reach-avoid-stay","formal verification","interval bound propagation","stochastic differential equations","probabilistic control guarantees"],"falsifier":"Run the trained certificate on the bivariate geometric Brownian motion example under many simulated trajectories, record the certificate value $V(\\psi, X_\\psi)$ at the first time it leaves $[\\alpha_S,\\beta_{RA})$, and compute the empirical average of those values. If the average exceeds $\\alpha_S$, the maximal-inequality step of the stay proof fails and the claimed stay probability does not follow from the stated conditions.","tokens_in":18008,"feed_emoji":"🎯","tokens_out":11896,"duration_ms":101931,"temperature":0.7,"pith_summary":"The paper seeks to establish that a single learned function—a reach-avoid-stay certificate—can provide formally certified probability bounds for a continuous-time stochastic system: the probability that trajectories from a given initial set reach a target while avoiding unsafe states, and the probability that they stay in the target afterwards. This matters because existing neural certificates either assume discrete time or ignore stochasticity, so they cannot give sound guarantees for physical systems governed by stochastic differential equations. The authors propose a proof rule (Theorem 1) that connects six local conditions on the certificate and its infinitesimal generator to the specification probabilities $\\varepsilon$ and $\\delta$, and an algorithm that trains such a certificate by gradient descent and verifies it by interval bound propagation. They demonstrate the method on an inverted pendulum with a neural controller and on a bivariate geometric Brownian motion.","feed_headline":"One learned function certifies reach, avoid, and stay probabilities","feed_subtitle":"A trained supermartingale turns sampled drift and diffusion into formally verified safety probability bounds.","key_machinery":"The load-bearing object is the reach-avoid-stay certificate (RAS-C): a nonnegative, smooth function $V(t,x)$ whose infinitesimal generator $G_\\pi V$ is forced to decrease outside the target and, inside the target, outside a small sublevel set, with four thresholds $\\alpha_S < \\beta_S < \\alpha_{RA} < \\beta_{RA}$. Around it the proof wraps a stopped process $Y_t = V(t \\wedge \\psi, X_{t\\wedge\\psi})$, where $\\psi$ is the first time the certificate leaves $[\\alpha_S,\\beta_{RA})$; because the decrease and stay conditions make $\\psi$ finite almost surely and $Y$ a nonnegative supermartingale, optional stopping bounds the certificate's expected value at stopping times and the maximal inequality converts that expectation into tail probabilities. The algorithmic counterpart is a neural network trained by a loss that penalizes violations of each condition, with the generator evaluated through analytic Hessian computations, and a verifier using interval bound propagation over axis-aligned cells that splits cells until the decrease condition is checked on a cover of the required region.","core_discovery":"The central claim is Theorem 1: if a twice continuously differentiable function $V$ satisfies six conditions—nonnegativity, an upper bound $\\alpha_{RA}$ on initial states, a lower bound $\\beta_{RA}$ on unsafe states, a generator-decrease condition outside the target, a sub-$\\beta_S$ goal set inside the target, and a generator-decrease condition inside the target outside a sub-$\\alpha_S$ set—with constants ordered $\\alpha_S < \\beta_S < \\alpha_{RA} < \\beta_{RA}$, then the controlled process satisfies the reach-avoid-stay specification with reach-avoid probability at least $\\varepsilon = 1 - \\alpha_{RA}/\\beta_{RA}$ and stay probability at least $\\delta = 1 - \\alpha_S/\\beta_S$. The proof constructs the first time $\\psi$ at which the certificate leaves the interval $[\\alpha_S, \\beta_{RA})$, shows that the stopped process is a supermartingale, and applies maximal and optional-stopping inequalities to turn the local decrease conditions into global probability bounds. The authors further claim that this is the first neural-certificate framework for continuous-time stochastic systems, and that the training-plus-verification pipeline produces sound lower bounds on the specification probabilities.","pith_inferences":["Beyond the paper: because the generator includes $\\partial/\\partial t$ and the sets are allowed to depend on time, the same proof structure should extend to moving or growing target and unsafe sets.","Beyond the paper: the ratio form of the bounds suggests that optimizing the level thresholds, rather than fixing them, could improve certified probabilities without changing the network architecture.","Beyond the paper: since training only needs samples of drift and diffusion, the certificate could be trained jointly with the control policy, turning verification into a synthesis objective rather than a post-hoc check.","Beyond the paper: adding an explicit condition that the certificate's expected value at $\\psi$ is below $\\alpha_S$ would make the persistence bound self-contained and is directly testable on the two benchmarks."],"forward_implications":["A successful verification run yields a sound lower bound on each specification probability, so a valid certificate gives an honest guarantee about every trajectory from the initial set.","Systems with non-polynomial drift or diffusion, including neural-network policies, become verifiable because the certificate is trained and checked without symbolically integrating the dynamics.","The same certificate covers reachability, avoidance, and persistence simultaneously, and omitting unused conditions certifies reach-avoid or stay alone.","The verified probabilities are set by the ratios $\\alpha_{RA}/\\beta_{RA}$ and $\\alpha_S/\\beta_S$, so choosing the four thresholds controls how strong each guarantee is."],"supporting_citations":[{"why":"Supplies the recurrence criterion that makes the stopping time finite almost surely and the first-exit lemma that makes the stopped process a supermartingale.","marker":"Khasminskii (2011)"},{"why":"Supplies the maximal inequality for nonnegative supermartingales used to bound the stay probability.","marker":"Prajna, Jadbabaie, and Pappas (2004)"},{"why":"Supplies the optional stopping theorem that transfers the initial-condition bound to stopping times.","marker":"Le Gall (2016)"},{"why":"Supplies the analytic Hessian computation used to evaluate the infinitesimal generator of the neural certificate.","marker":"Singla and Feizi (2020)"},{"why":"Supplies the interval bound propagation engine that formally verifies the certificate conditions cell by cell.","marker":"Xu et al. (2020)"},{"why":"Provides the discrete-time neural supermartingale reach-avoid framework that the continuous-time proof extends and whose style is reused for the corollary.","marker":"Žikelić et al. (2023a)"}],"fun_headline_variants":["First neural certificates for continuous-time stochastic systems","Supermartingale nets certify reach-avoid-stay probabilities","Continuous-time neural proofs for probabilistic safety","Learn a supermartingale, certify reach-avoid-stay","Formal probability bounds via learned supermartingales"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The stay-probability proof assumes, without derivation, that the expected certificate value at the stopping time $\\psi$ is at most $\\alpha_S$; if that expectation can exceed $\\alpha_S$, the claimed persistence probability is unsupported.","fun_headline_variants_meta":{"raw":{"variants":["First neural certificates for continuous-time stochastic systems","Supermartingale nets certify reach-avoid-stay probabilities","Continuous-time neural proofs for probabilistic safety","Learn a supermartingale, certify reach-avoid-stay","Formal probability bounds via learned supermartingales"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000148,"raw_usage":{"total_tokens":1172,"prompt_tokens":908,"completion_tokens":264,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":524,"completion_tokens_details":{"reasoning_tokens":189}},"tokens_in":524,"tokens_out":264,"duration_ms":3030,"temperature":1.0,"reasoning_tokens":189,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T05:29:05.681410+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the trained certificate on the bivariate geometric Brownian motion example under many simulated trajectories, record the certificate value $V(\\psi, X_\\psi)$ at the first time it leaves $[\\alpha_S,\\beta_{RA})$, and compute the empirical average of those values. If the average exceeds $\\alpha_S$, the maximal-inequality step of the stay proof fails and the claimed stay probability does not follow from the stated conditions.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the recurrence criterion that makes the stopping time finite almost surely and the first-exit lemma that makes the stopped process a supermartingale."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the maximal inequality for nonnegative supermartingales used to bound the stay probability."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the optional stopping theorem that transfers the initial-condition bound to stopping times."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the analytic Hessian computation used to evaluate the infinitesimal generator of the neural certificate."}],"review_version":1}