{"id":"08cdcdda-eefd-4935-a924-98b4f21cdf34","arxiv_id":"2506.21697","paper_version":1,"verdict":"REJECT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"high","formal_verification":"none","parameter_count":5,"one_line_summary":"A framework for synthesizing and verifying neural control barrier functions for stochastic systems, including new Tanaka-formula-based safety conditions for ReLU networks.","lead":"Robots and control systems can be kept inside safe regions using learned barrier functions, but verifying the learned barrier when the system has random disturbances is hard. This paper proposes training and verification frameworks for stochastic neural control barrier functions, covering both smooth and ReLU neural networks.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 3's finite-sample certificate fails as stated: q1 and q2 in Eq. (10) contain indicator functions, so q_k are discontinuous and the Lipschitz premise used to extend psi* to all of X does not hold.","rationale":"The reader's weakest_assumption identifies exactly this issue: discontinuous indicators in q_k and uncertified epsilon_bar coverage, so I set agreement_with_reader='agree'. The central claim of the paper is a verifiable safety guarantee from finitely many samples, and the bridge from samples to all of X is Theorem 3. Its proof is invalid as written because the functions being extended are not Lipschitz. This is an internal correctness risk, not a matter of disagreeing with community consensus. The paper does contain useful independent material: the ReLU analysis via Tanaka's formula and the reduction of verification to nonlinear programs are plausible and testable, and the experiments demonstrate coverage improvements over the baseline. Those parts, however, do not rescue Algorithm 1, whose termination condition is exactly the unsupported condition of Theorem 3. A secondary sign inconsistency in Eq. (15) (the g*u and trace terms differ in sign from q3 in Eq. (10)) should also be fixed; it does not change my main concern but reinforces that the submitted artifact is not yet a certificate. The REJECT verdict is appropriate, and I do not see a reason to adjust it.","tokens_in":25745,"tokens_out":8314,"duration_ms":99606,"concrete_test":"For the trained inverted-pendulum SNCBF in Section VI-B.1 (epsilon_bar = 1.6e-4, Lmax = 2.4, psi* = -4.2e-4), evaluate q1 and q2 from Eq. (10) along a segment crossing the boundaries of XI and XU. If any two points within epsilon_bar on opposite sides of a boundary satisfy |q_k(x) - q_k(x')| / ||x - x'|| > Lmax, or if the jump across the boundary exceeds Lmax epsilon_bar, the Lipschitz premise of Theorem 3 is violated and the finite-sample condition cannot certify q_k <= 0 everywhere. Separately, report the number N of samples used; if N does not cover X with radius epsilon_bar (e.g., N < volume(X) / (c_n epsilon_bar^n) for the relevant dimension n), the coverage assumption is unverified.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The load-bearing step is Theorem 3's claim that Lmax epsilon_bar + psi* <= 0 implies q_k(x) <= 0 for every x. The proof uses q_k(x) <= q_k(x_i) + L_k||x - x_i||, which requires each q_k in Eq. (10) to be L-Lipschitz. But q_1(x) = (-B(x)) 1_XI(x) and q_2(x) = (B(x) + delta) 1_XU(x) contain indicator functions of XI and XU. These indicators are discontinuous at the boundaries of XI and XU unless B happens to take exactly the value needed to make the product continuous, a condition neither assumed, trained for, nor verified. Thus the sentence in Theorem 3, 'Suppose condition 1) in Assumption 3 holds so that the functions q_k are Lipschitz continuous,' is not a consequence of Assumption 3 and is false in general. The finite-sample certification step therefore does not go through for the reported smooth SNCBFs. In addition, the coverage radius epsilon_bar is assumed but never certified: no sample counts N are reported in Section VI, so even a repaired Lipschitz argument would lack the required coverage certificate.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes synthesis and verification frameworks for stochastic neural control barrier functions (SNCBFs) for continuous-time stochastic systems. For smooth (twice-differentiable) activations, it gives a 'verification-free' finite-sample certificate (Theorem 3) based on Lipschitz constants and sample coverage, together with an SMT/optimization-based verification-in-the-loop (VITL) procedure. For ReLU activations, it uses Tanaka's formula to construct a surrogate process ~B and derives a worst-case safety probability (Theorem 5), with enumeration-based verification and VITL synthesis. Experiments on an inverted pendulum, the Darboux system, and a unicycle model report safe-region coverage and training times, comparing against a fault-tolerant SNCBF baseline.","tokens_in":26014,"tokens_out":11365,"duration_ms":120138,"significance":"The intended contribution is timely and practically relevant: certifying stochastic neural safety filters over a continuous state space from finitely many samples, including a ReLU variant, would be a substantial advance. The use of Tanaka's formula to handle nondifferentiable ReLU barriers is original, and the VITL architecture with SMT-based nonlinear programs is a reasonable design. However, the central proofs contain load-bearing errors—the Lipschitz extension of discontinuous q_k in Theorem 3 and the lower-bound inequality in Lemma 3—so the claimed guarantees are not established. The paper does not provide code or machine-checked proofs, and the experiments report no coverage certification.","major_comments":[{"comment":"The finite-sample certificate in Theorem 3 does not follow from its hypotheses because the functions q1(x)=(-B(x))1_XI(x) and q2(x)=(B(x)+δ)1_XU(x) are discontinuous at the boundaries of XI and XU, so they are not Lipschitz continuous on X. Assumption 3(1) only asserts Lipschitz continuity of B, ∂B/∂x, ∂²B/∂x² and μ; it does not imply that products with indicator functions are Lipschitz, and the proof's inequality q_k(x) ≤ q_k(x_i)+L_k∥x−x_i∥ is therefore unjustified. The value Lmax in condition (12) is also never computed from the network and dynamics in a verifiable way.","section":"§IV-A, Eq. (10), Theorem 3"},{"comment":"The coverage hypothesis of Theorem 3—that the sample set covers D with balls of radius ε̄—is asserted but never certified. Section VI reports only ε̄ values (0.00016 and 0.01) and final ψ*, not the number of samples N or a proof that every point of D lies within ε̄ of a sample, so the experiments do not demonstrate the claimed whole-state-space guarantee even setting aside the Lipschitz issue.","section":"§IV-A, §VI-B"},{"comment":"Lemma 3 is false for ReLU networks with negative output weights. For a single neuron with W2j<0, the difference B(x)−~B(x) equals |W2j|/2(z_j^2/R_j − |z_j|), which is ≤0 whenever |z_j|≤R_j, so the asserted inequality ~B(x)≤B(x) can fail. Concrete example: W2=−1, R=1, z=0.5, r2=1 gives B=0.5 and ~B=0.625. Since ~D need not be contained in D, the chain of probabilities in Theorem 5, P[x_t∈int(D)] ≥ P[x_t∈int(~D)], is not established, and the worst-case guarantee for the original safe set D collapses.","section":"§V-A, Lemma 3, Eq. (27), Theorem 5"},{"comment":"Proposition 3 assumes without statement that the super-level set D is connected ('Since D is connected' in the proof); for an arbitrary trained ReLU network the super-level set can be disconnected, and no argument is given that the breadth-first enumeration still covers all activation sets needed for correctness and feasibility verification. The proof also invokes 'completeness' with a citation to a general AI textbook rather than a formal statement, leaving the enumeration guarantee insufficiently supported.","section":"§V-B, Proposition 3"},{"comment":"The paper never explains how the constants Rj satisfying |z_j|≤R_j whenever B(x)≥0 are obtained; they are not reported in Section VI, nor are they part of the training constraints or verification procedures, so condition (29) and Theorem 5 cannot be instantiated for the reported ReLU experiments.","section":"§V-A, Lemma 3, Definition 4, §VI-B"}],"minor_comments":[{"comment":"The statement of Proposition 1 uses an undefined set C in c = sup_{x∈C} B(x); this should be the domain of the probability estimate, presumably D.","section":"§III-C, Proposition 1"},{"comment":"The nonnegativity condition in (22a) is written [y]_i ≥ 0, while the analogous ReLU condition (31a) writes [y]_1 ≥ 0; the latter appears to be a typo.","section":"§IV-B, Proposition 2 and §V-B, Proposition 4"},{"comment":"The caption of Figure 4 mentions error bars over 5 seeds, but Table I reports single verification/synthesis times and coverage without uncertainty; please state whether these are means over seeds.","section":"§VI-B, Table I and Figure 4"},{"comment":"The sums in the definition of ¯W2 have upper index r (or j) but should run over the input dimension nx; as written the expression is ambiguous.","section":"§IV-A, Theorem 4, Eq. (14)"}],"recommendation":"reject","confidential_remarks":"This manuscript has substantial overlap with the authors' prior CDC 2024 paper [24], which already proposed smooth SNCBF verifiable synthesis; the genuinely new material is the ReLU extension and the VITL verification, but the ReLU proof error and the Theorem 3 gap prevent acceptance. I would not recommend transfer to another journal without correcting Lemma 3 and re-certifying the finite-sample step."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The ReLU SNCBF construction via Tanaka's formula is genuinely new, and the per-hyperplane enumeration and verification for ReLU networks is a solid engineering contribution. The smooth case is mostly an extension of the authors' prior CDC paper, but the stochastic ReLU machinery is a real step forward.\n\nThe problem is the main finite-sample guarantee. Theorem 3 claims that Lmax * epsilon_bar + psi* <= 0 implies safety over the whole state space, using Lipschitz continuity of q_k in (10). But q1 and q2 are products of a smooth-ish function with indicator functions of the safe/unsafe sets. Those indicators are discontinuous at the set boundaries, so the q_k are not Lipschitz unless B happens to exactly cancel the jump—something neither assumed nor verified. The sentence in Theorem 3 saying this follows from Assumption 3 is simply false. The proof's core inequality q_k(x) <= q_k(x_i) + L_k * norm(x - x_i) has no basis.\n\nThe coverage radius epsilon_bar is also just asserted. Section VI never reports sample counts N or anything that would certify D is covered with radius 0.00016 or 0.01, so even a repaired Lipschitz argument would lack the necessary input. For a paper whose abstract promises 'verifiably safe synthesis,' this is a load-bearing omission.\n\nSmaller issues: the loss in (15) does not match q3 in (10)—the signs on the drift and diffusion terms are wrong. The ReLU Proposition 3 proof assumes D is connected without saying so, and the Rj preactivation bounds in Lemma 3 are never reported in the experiments. Theorem 5's final inequality is a typo that compares a probability to itself, though the intended argument is likely fixable.\n\nWhat is here that is good: the Tanaka-based lower bound for ReLU barriers is a meaningful idea, and the verification algorithms are plausible and could be made sound with modest changes. The paper is not circular; the external bound from [52] and the stochastic tools are used legitimately.\n\nWho this is for: people working on neural CBF verification and learning-based safety filters, especially those interested in stochastic or ReLU networks. It deserves a serious referee—the core ideas are worth engaging with—but as is, the central guarantee is not established. I would send it to peer review with major revisions: fix the Lipschitz argument, certify the coverage, align the loss with the theory, and report the missing constants. Then it could be a solid paper.","headline":"New ReLU stochastic CBF construction is worth a look, but the paper's central finite-sample certificate does not hold as stated because the auxiliary functions it relies on are discontinuous.","tokens_in":26585,"tokens_out":3164,"would_cite":true,"duration_ms":31238,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["93D30","60H10","68T07","93C10"],"pacs":[],"model":"deepseek-v4-flash","headline":"Finite samples can certify stochastic neural safety barriers","keywords":["stochastic control barrier functions","neural certificates","safety verification","ReLU networks","Tanaka's formula","verification-in-the-loop","stochastic differential equations","control barrier functions"],"falsifier":"Measure the actual maximum distance from points in the safe set to the nearest sampled point for the reported coverage radii, such as $\\bar{\\epsilon}=0.00016$ for the inverted pendulum; if the measured covering radius exceeds $\\bar{\\epsilon}$, the certified guarantee does not follow. Alternatively, evaluate $q_k$ along a line crossing the boundary of the initial safe set and observe that the indicator-weighted functions jump, which would break the Lipschitz premise of Theorem 3.","tokens_in":25473,"feed_emoji":"🛡️","tokens_out":5638,"duration_ms":59159,"temperature":0.7,"pith_summary":"This paper aims to make neural-network-based safety filters provably safe in stochastic systems, where the state evolves under Brownian noise. The authors claim that a barrier function represented by a neural network can be certified over the entire state space using only finitely many sample constraints, provided a margin condition of the form $L_{\\max}\\bar{\\epsilon}+\\psi^*\\le 0$ holds. If true, this replaces the usual expensive verification of every state with a finite linear program plus a Lipschitz bound. The paper extends the same reasoning to ReLU networks by constructing a surrogate lower-bound process via Tanaka's formula, and demonstrates the frameworks on an inverted pendulum, a Darboux system, and a unicycle model.","feed_headline":"Finite samples can certify stochastic neural safety barriers","feed_subtitle":"Worst-case probability guarantees extend from sampled points to every state in the safe set.","key_machinery":"The machinery is the finite-sample validity condition $L_{\\max}\\bar{\\epsilon}+\\psi^*\\le 0$ for smooth SNCBFs, combined with scenario optimization: sample points $x_i$, solve a linear program in the slack $\\psi$ over the sampled constraints, then use Lipschitz continuity to extend the bound to every state. For ReLU SNCBFs, the central object is a surrogate stochastic process $\\tilde{B}$ that lies below the true barrier $B$ on the super-level set; Tanaka's formula expresses the generator of $\\tilde{B}$ in terms of activation sets and neuron pre-activation values, so a control satisfying $\\mathcal{A}\\tilde{B}\\ge -k\\tilde{B}$ yields the worst-case probability guarantee. The verification pipeline enumerates the piecewise-linear regions of the ReLU network and checks correctness and feasibility as nonlinear programs.","core_discovery":"The central claim is that Algorithms 1 and 3 synthesize stochastic neural control barrier functions (SNCBFs) whose super-level set $D$ stays safe with worst-case probability $\\mathbb{P}[x_t \\in \\operatorname{int}(D),\\, 0\\le t\\le T \\,\\vert\\, x_0\\in \\operatorname{int}(D)] \\ge (B(x_0)/c)e^{-cT}$. Theorem 3 states that this follows for smooth SNCBFs once the finite-sample optimal value $\\psi^*$ satisfies $L_{\\max}\\bar{\\epsilon}+\\psi^*\\le 0$, where $\\bar{\\epsilon}$ is the radius of a cover of the state space by sampled points and $L_{\\max}$ is the maximum Lipschitz constant of the sampled constraints. Theorem 5 states the analogous guarantee for ReLU SNCBFs, using a lower-bounding surrogate $\\tilde{B}$ derived from Tanaka's formula; a control that satisfies $\\mathcal{A}\\tilde{B}(x)\\ge -k\\tilde{B}(x)$ keeps the original barrier's super-level set safe with the same exponential probability bound. The verification-in-the-loop algorithms solve the correctness and feasibility questions as nonlinear programs via Farkas' lemma and Positivstellensatz, and use counterexamples to retrain the network.","pith_inferences":["A natural extension the authors leave open is multi-hidden-layer ReLU SNCBFs; their enumeration-based verification would likely grow combinatorially, so abstraction or branch-and-bound pruning would be needed for scalability.","The margin condition $L_{\\max}\\bar{\\epsilon}+\\psi^*\\le 0$ suggests a design trade-off: increasing sample density shrinks $\\bar{\\epsilon}$ and relaxes the required negativity of $\\psi^*$, so practitioners could tune sampling effort against the slack needed for the barrier.","Because the constraints $q_1$ and $q_2$ contain indicator functions, the Lipschitz constants used in Theorem 3 are only meaningful away from the boundary of the initial safe and unsafe sets; a more careful treatment of these discontinuities would be needed to make the finite-sample argument fully rigorous.","If the finite-sample certification transfers to higher-dimensional systems, it could make stochastic safety filters practical for robotic and autonomous-driving pipelines, where exhaustive verification is intractable; the paper's experiments are confined to two- and three-dimensional state spaces."],"forward_implications":["If Theorem 3 holds, a neural barrier can be certified over the whole state space from a finite sample set, eliminating the need to grid or symbolically verify every state.","The ReLU extension means non-smooth activation functions are eligible for certified stochastic safety, not just smooth activations like tanh or sigmoid.","The verification-in-the-loop framework turns counterexamples found by the verifier into training data, so synthesis and verification feed each other until the SNCBF passes.","The probability bound $e^{-cT}$ gives an explicit time-horizon safety guarantee, enabling risk-aware design for safety-critical controllers under Brownian disturbance.","For systems with input constraints, the Farkas-based feasibility check provides a necessary and sufficient condition for the existence of a safe control at every state."],"supporting_citations":[{"why":"Supplies the worst-case probability estimate (Proposition 1) that both the smooth and ReLU guarantees rely on.","marker":"[52]"},{"why":"Provides Tanaka's formula, the mathematical basis for the ReLU SNCBF surrogate lower bound.","marker":"[51]"},{"why":"Gives the hyperplane decomposition and exact verification logic for ReLU neural barrier functions that the ReLU verification inherits.","marker":"[28]"},{"why":"Supplies the infinitesimal generator formula for smooth SNCBFs used in the verification conditions.","marker":"[55]"},{"why":"Provides the LMI-based Lipschitz certificates used to bound the barrier and its derivatives and to enforce condition (12).","marker":"[56]"},{"why":"Positivstellensatz is used to derive the polynomial certificate for feasibility of smooth SNCBFs.","marker":"[53]"},{"why":"Farkas' lemma converts the existence of a safe control into a non-existence condition for a dual variable.","marker":"[54]"},{"why":"The fault-tolerant SNCBF baseline that the experiments compare against.","marker":"[43]"},{"why":"The authors' prior conference work on smooth SNCBF synthesis that this paper extends to ReLU activations and verification-in-the-loop.","marker":"[24]"}],"fun_headline_variants":["Verifiable synthesis for stochastic neural CBFs","Sample-based certification for smooth and ReLU barriers","Worst-case safety proven from finite data points","Stochastic safety filters with finite-sample guarantees"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole-state-space guarantee rests on the premise that the sampled points cover the safe set with a known radius $\\bar{\\epsilon}$ and that the constraint functions are Lipschitz with known constants, but the indicator functions used in the constraints are discontinuous at set boundaries, and the paper does not report sample counts that would certify the coverage.","fun_headline_variants_meta":{"raw":{"variants":["Verifiable synthesis for stochastic neural CBFs","Sample-based certification for smooth and ReLU barriers","Worst-case safety proven from finite data points","Stochastic safety filters with finite-sample guarantees"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000223,"raw_usage":{"total_tokens":1479,"prompt_tokens":992,"completion_tokens":487,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":608,"completion_tokens_details":{"reasoning_tokens":429}},"tokens_in":608,"tokens_out":487,"duration_ms":5956,"temperature":1.0,"reasoning_tokens":429,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T22:21:59.429946+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Measure the actual maximum distance from points in the safe set to the nearest sampled point for the reported coverage radii, such as $\\bar{\\epsilon}=0.00016$ for the inverted pendulum; if the measured covering radius exceeds $\\bar{\\epsilon}$, the certified guarantee does not follow. Alternatively, evaluate $q_k$ along a line crossing the boundary of the initial safe set and observe that the indicator-weighted functions jump, which would break the Lipschitz premise of Theorem 3.","supporting_citations":[{"cited_title":"Revuz and M","cited_arxiv_id":null,"evidence_quote":"Provides Tanaka's formula, the mathematical basis for the ReLU SNCBF surrogate lower bound."},{"cited_title":"Exact verification of relu neural control barrier functions,","cited_arxiv_id":null,"evidence_quote":"Gives the hyperplane decomposition and exact verification logic for ReLU neural barrier functions that the ReLU verification inherits."},{"cited_title":"Semidefinite programming relaxations for semialgebraic problems,","cited_arxiv_id":null,"evidence_quote":"Positivstellensatz is used to derive the polynomial certificate for feasibility of smooth SNCBFs."},{"cited_title":"Matou ˇsek and B","cited_arxiv_id":null,"evidence_quote":"Farkas' lemma converts the existence of a safe control into a non-existence condition for a dual variable."},{"cited_title":"Fault tolerant neural control barrier functions for robotic systems under sensor faults and attacks,","cited_arxiv_id":null,"evidence_quote":"The fault-tolerant SNCBF baseline that the experiments compare against."}],"review_version":1}