Pith. sign in

REVIEW 5 major objections 4 minor 61 references

Stochastic Neural Control Barrier Functions

T0 review · 5 major / 4 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Finite samples can certify stochastic neural safety barriers

desk verdict 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. read the letter →

arxiv 2506.21697 v1 pith:B5FAAKYF submitted 2025-06-26 eess.SY cs.ROcs.SY

Hongchao Zhang , Manan Tayal , Jackson Cox , Pushpak Jagtap , Shishir Kolathaya , Andrew Clark This is my paper · ORCID
classification eess.SYcs.ROcs.SY MSC 93D3060H1068T0793C10
keywords stochasticcontrolbarrierfunctionsneuralcertificatessafetyverificationReLUnetworksTanaka'sformulaverification-in-the-loopdifferentialequations
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

5 major / 4 minor

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.

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 (5)
  1. [§IV-A, Eq. (10), Theorem 3] 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.
  2. [§IV-A, §VI-B] 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.
  3. [§V-A, Lemma 3, Eq. (27), Theorem 5] 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.
  4. [§V-B, Proposition 3] 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.
  5. [§V-A, Lemma 3, Definition 4, §VI-B] 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.
minor comments (4)
  1. [§III-C, Proposition 1] 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.
  2. [§IV-B, Proposition 2 and §V-B, Proposition 4] 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.
  3. [§VI-B, Table I and Figure 4] 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.
  4. [§IV-A, Theorem 4, Eq. (14)] 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.

Circularity Check

0 steps flagged · score 2.0 of 10

No circular reduction found; the finite-sample certificate and ReLU safety bound rest on external theorems, with only non-load-bearing self-citations.

full rationale

The paper's central safety bound is Proposition 1, quoted from [52] (Wang et al., CDC 2021), which is independent of the authors. Theorem 3 is a finite-sample-to-all-x extension via L-Lipschitz continuity of q_k; the optimization variable psi* is a training certificate, not a fitted prediction of the safety probability, so the conclusion is not statistically forced. The ReLU contribution derives A\tilde B and the lower bound \tilde B <= B using Tanaka's formula [51]; Theorem 5 applies the external Proposition 1 to \tilde B and uses \tilde D subset of D, so the worst-case probability is not equivalent to an input by construction. Self-citations appear ([24] for prior smooth SNCBF work, [28] for ReLU hyperplane decomposition, [32], [43]), but the load-bearing mathematical results ([52], [51], [56], and standard BFS completeness [59]) are external or elementary, so the self-citations are not load-bearing. The main caveat is a soundness gap, not circularity: Theorem 3's premise that q_k are Lipschitz is unsupported because q1 and q2 in Eq. (10) contain indicators 1_XI and 1_XU, which are discontinuous at set boundaries; also the required epsilon_bar-cover of D is assumed but never certified, since no sample counts are reported in Section VI. These flaws raise correctness risk but do not make the derivation equivalent to its inputs.

Assumptions & free parameters 5 free parameters · 9 assumptions · 0 invented entities

The paper introduces no new physical entities. The surrogate barrier Btilde in Eq. (27) is a mathematical construction for handling ReLU non-differentiability, not an independent postulated object. The main axiomatic burden is the unverified dense sampling condition and the Lipschitz assumption on functions that contain discontinuous indicators.

free parameters (5)
  • Lipschitz bounds Lh, Ldh, Ld2h = pendulum: 0.01, 0.4, 2; unicycle: 1, 1, 2
    User-chosen Lipschitz bounds on B, its derivative, and the Hessian term. They enter Lmax and the validity condition Lmax epsilon_bar + psi* <= 0, so the guarantee is only as strong as these manual choices.
  • sample radius epsilon_bar = 0.00016 (pendulum), 0.01 (unicycle)
    The finite-sample guarantee requires D to be covered by balls of radius epsilon_bar. Smaller epsilon_bar makes the validity condition easier but demands many more samples; coverage is never certified.
  • delta in Eq. (10) = not reported
    A small positive scalar used in q2 to enforce strict inequality B(x) < 0 on the unsafe set. It also creates the discontinuity in q2 at the safe set boundary.
  • gamma in alpha(B) = gamma B = 1
    The class-K function parameter in the stochastic CBF inequality. It affects the feasibility condition and the safety probability bound.
  • ReLU preactivation bounds Rj = not reported
    Lemma 3 and Theorem 5 assume |z_j| <= R_j whenever B(x) >= 0. These bounds appear in the safety condition, the verification programs, and the control law, but no values or computation method are given.
assumptions (9)
  • domain assumption Assumption 1: the SDE admits a unique strong solution and the initial state is deterministic.
    Invoked to apply stochastic calculus and the infinitesimal generator to the system in Eq. (1).
  • domain assumption Assumption 2: the barrier function B or the surrogate Btilde lies in the domain of the generator D(A), with finite expectation and existing limit.
    Needed to define A B and to apply the stochastic comparison argument in Theorem 5.
  • domain assumption Assumption 3: B, its derivatives, and the control policy are Lipschitz; B has one hidden layer; V is diagonal; activation derivatives are bounded.
    This is the premise of Theorem 3 and of the LMI-based Lipschitz certificates in Theorem 4.
  • standard math External probability bound of Proposition 1 from [52] for stochastic CBFs with linear class-K functions.
    The worst-case probability estimates in both the smooth and ReLU settings are imported from this cited result, not derived in the paper.
  • ad hoc to paper The finite sample set covers D with balls of radius epsilon_bar.
    This is the key sampling assumption of the verification-free synthesis. The paper does not certify it or report the sample count N.
  • ad hoc to paper The q_k functions in Eq. (10) are Lipschitz with known constant Lmax.
    Theorem 3 needs this for the finite-sample margin argument, but the indicator functions 1_XI and 1_XU are discontinuous at set boundaries.
  • ad hoc to paper ReLU preactivation z_j is uniformly bounded by R_j on the set where B(x) >= 0.
    This bound is assumed in Lemma 3 and Theorem 5 to construct the lower surrogate barrier Btilde.
  • ad hoc to paper The super-level set D is connected.
    The proof of Proposition 3 uses connectedness of D to justify breadth-first enumeration of activation sets, but the proposition and Algorithm 2 do not state this assumption.
  • standard math Positivstellensatz and Farkas' Lemma.
    Used to convert non-existence of feasibility counterexamples into algebraic and linear-programming conditions.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Stochastic Neural Control Barrier Functions." pith.science (2026). https://pith.science/paper/B5FAAKYF

@misc{pith2026250621697,
  author       = {Pith},
  title        = {Pith review of: Stochastic Neural Control Barrier Functions},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/B5FAAKYF}},
  note         = {Machine review of arXiv:2506.21697}
}
read the original abstract

Control Barrier Functions (CBFs) are utilized to ensure the safety of control systems. CBFs act as safety filters in order to provide safety guarantees without compromising system performance. These safety guarantees rely on the construction of valid CBFs. Due to their complexity, CBFs can be represented by neural networks, known as neural CBFs (NCBFs). Existing works on the verification of the NCBF focus on the synthesis and verification of NCBFs in deterministic settings, leaving the stochastic NCBFs (SNCBFs) less studied. In this work, we propose a verifiably safe synthesis for SNCBFs. We consider the cases of smooth SNCBFs with twice-differentiable activation functions and SNCBFs that utilize the Rectified Linear Unit or ReLU activation function. We propose a verification-free synthesis framework for smooth SNCBFs and a verification-in-the-loop synthesis framework for both smooth and ReLU SNCBFs. and we validate our frameworks in three cases, namely, the inverted pendulum, Darboux, and the unicycle model.

Figures

Figures reproduced from arXiv: 2506.21697 by the authors.

Figure 1
Figure 1. Workflow of the synthesis with verification in the loop. [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
Figure 2
Figure 2. This figure presents the experimental results on the inverted pendulum system. Fig. [PITH_FULL_IMAGE:figures/full_fig_p014_2.png] view at source ↗
Figure 3
Figure 3. Proposed safe control comparison among different [PITH_FULL_IMAGE:figures/full_fig_p014_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Comparison of coverage and training time across [PITH_FULL_IMAGE:figures/full_fig_p014_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

61 extracted references · 42 canonical work pages

  1. [52]

    Safety-critical control of stochastic systems using stochastic control barrier functions,

    C. Wang, Y . Meng, S. L. Smith, and J. Liu, “Safety-critical control of stochastic systems using stochastic control barrier functions,” in 2021 60th IEEE Conference on Decision and Control (CDC) . IEEE, 2021, pp. 5924–5931

    2021

  2. [1]

    Safety critical systems: Challenges and directions,

    J. C. Knight, “Safety critical systems: Challenges and directions,” in 24th International Conference on Software Engineering , 2002, pp. 547–550

    work page 2002

  3. [2]

    Planning and decision- making for autonomous vehicles,

    W. Schwarting, J. Alonso-Mora, and D. Rus, “Planning and decision- making for autonomous vehicles,” Annual Review of Control, Robotics, and Autonomous Systems , vol. 1, pp. 187–210, 2018

    work page 2018

  4. [3]

    Learning safe, generalizable perception-based hybrid control with certificates,

    C. Dawson, B. Lowenkamp, D. Goff, and C. Fan, “Learning safe, generalizable perception-based hybrid control with certificates,” IEEE Robotics and Automation Letters , vol. 7, no. 2, pp. 1904–1911, 2022

    work page 1904

  5. [4]

    Control barrier functions: Theory and applications,

    A. D. Ames, S. Coogan, M. Egerstedt, G. Notomista, K. Sreenath, and P. Tabuada, “Control barrier functions: Theory and applications,” in 18th European control conference (ECC) . IEEE, 2019, pp. 3420–3431

    work page 2019

  6. [5]

    Hamilton-jacobi reachability: A brief overview and recent advances,

    S. Bansal, M. Chen, S. Herbert, and C. J. Tomlin, “Hamilton-jacobi reachability: A brief overview and recent advances,” in 2017 IEEE 56th Annual Conference on Decision and Control (CDC) . IEEE, 2017, pp. 2242–2253

    work page 2017

  7. [6]

    A Physics-Informed Machine Learning Framework for Safe and Optimal Control of Autonomous Systems

    M. Tayal, A. Singh, S. Kolathaya, and S. Bansal, “A physics-informed machine learning framework for safe and optimal control of autonomous systems,” arXiv preprint arXiv:2502.11057 , 2025

    work page Pith review arXiv 2025

  8. [7]

    Robust control barrier–value functions for safety-critical control,

    J. J. Choi, D. Lee, K. Sreenath, C. J. Tomlin, and S. L. Herbert, “Robust control barrier–value functions for safety-critical control,” in 2021 60th IEEE Conference on Decision and Control (CDC) . IEEE, 2021, pp. 6814–6821

    work page 2021

Show all 61 references
  1. [8]

    Safe learning in robotics: From learning-based control to safe reinforcement learning,

    L. Brunke, M. Greeff, A. W. Hall, Z. Yuan, S. Zhou, J. Panerati, and A. P. Schoellig, “Safe learning in robotics: From learning-based control to safe reinforcement learning,” Annual Review of Control, Robotics, and Autonomous Systems , vol. 5, pp. 411–444, 2022

    2022

  2. [9]

    Combining model-based design and model-free policy optimization to learn safe, stabilizing controllers,

    T. Westenbroek, A. Agrawal, F. Castaneda, S. S. Sastry, and K. Sreenath, “Combining model-based design and model-free policy optimization to learn safe, stabilizing controllers,” IFAC-PapersOnLine, vol. 54, no. 5, pp. 19–24, 2021. 15

    2021

  3. [10]

    Lyapunov-based safe policy optimization for continuous control,

    Y . Chow, O. Nachum, A. Faust, E. Duenez-Guzman, and M. Ghavamzadeh, “Lyapunov-based safe policy optimization for continuous control,” arXiv preprint arXiv:1901.10031 , 2019

    1901 arXiv

  4. [11]

    Control barrier function based quadratic programs with application to adaptive cruise control,

    A. D. Ames, J. W. Grizzle, and P. Tabuada, “Control barrier function based quadratic programs with application to adaptive cruise control,” in 53rd IEEE Conference on Decision and Control . IEEE, 2014, pp. 6271–6278

    2014

  5. [12]

    Formal synthesis of stochastic systems via control barrier certificates,

    P. Jagtap, S. Soudjani, and M. Zamani, “Formal synthesis of stochastic systems via control barrier certificates,” IEEE Transactions on Automatic Control, vol. 66, no. 7, pp. 3097–3110, 2020

    2020

  6. [13]

    Verification and synthesis of control barrier functions,

    A. Clark, “Verification and synthesis of control barrier functions,” in 2021 60th IEEE Conference on Decision and Control (CDC) . IEEE, 2021, pp. 6105–6112

    2021

  7. [14]

    Synthesis of partially observed jump-diffusion systems via control barrier functions,

    N. Jahanshahi, P. Jagtap, and M. Zamani, “Synthesis of partially observed jump-diffusion systems via control barrier functions,” IEEE Control Systems Letters , vol. 5, no. 1, pp. 253–258, 2020

    2020

  8. [15]

    Safe control with learned certificates: A survey of neural Lyapunov, barrier, and contraction methods for robotics and control,

    C. Dawson, S. Gao, and C. Fan, “Safe control with learned certificates: A survey of neural Lyapunov, barrier, and contraction methods for robotics and control,” IEEE Transactions on Robotics , 2023

    2023

  9. [16]

    A semi-algebraic framework for verification and synthesis of control barrier functions,

    A. Clark, “A semi-algebraic framework for verification and synthesis of control barrier functions,” IEEE Transactions on Automatic Control , 2024

    2024

  10. [17]

    Verification and synthesis of robust control barrier functions: Multilevel polynomial optimization and semidefinite relaxation,

    S. Kang, Y . Chen, H. Yang, and M. Pavone, “Verification and synthesis of robust control barrier functions: Multilevel polynomial optimization and semidefinite relaxation,” in 2023 62nd IEEE Conference on Decision and Control (CDC) . IEEE, 2023, pp. 8215–8222

    2023

  11. [18]

    Convex synthesis and verification of control- lyapunov and barrier functions with input constraints,

    H. Dai and F. Permenter, “Convex synthesis and verification of control- lyapunov and barrier functions with input constraints,” in 2023 American Control Conference (ACC). IEEE, 2023, pp. 4116–4123

    2023

  12. [19]

    A survey of end-to-end driving: Architectures and training methods,

    A. Tampuu, T. Matiisen, M. Semikin, D. Fishman, and N. Muhammad, “A survey of end-to-end driving: Architectures and training methods,” IEEE Transactions on Neural Networks and Learning Systems , vol. 33, no. 4, pp. 1364–1384, 2020

    2020

  13. [20]

    Physics-informed neural networks: A deep learning framework for solving forward and inverse problems involving nonlinear partial differential equations,

    M. Raissi, P. Perdikaris, and G. E. Karniadakis, “Physics-informed neural networks: A deep learning framework for solving forward and inverse problems involving nonlinear partial differential equations,” Journal of Computational Physics , vol. 378, pp. 686–707, 2019

    2019

  14. [21]

    Deep learning for time-series analysis,

    J. C. B. Gamboa, “Deep learning for time-series analysis,” arXiv preprint arXiv:1701.01887, 2017

    2017 arXiv

  15. [22]

    How to train your neural control barrier function: Learning safety filters for complex input-constrained systems,

    O. So, Z. Serlin, M. Mann, J. Gonzales, K. Rutledge, N. Roy, and C. Fan, “How to train your neural control barrier function: Learning safety filters for complex input-constrained systems,” in 2024 IEEE International Conference on Robotics and Automation (ICRA) . IEEE, 2024, pp...

    2024

  16. [23]

    Safe nonlinear control using robust neural Lyapunov-barrier functions,

    C. Dawson, Z. Qin, S. Gao, and C. Fan, “Safe nonlinear control using robust neural Lyapunov-barrier functions,” in Conference on Robot Learning. PMLR, 2022, pp. 1724–1735

    2022

  17. [24]

    Learning a formally verified control barrier function in stochastic environment,

    M. Tayal, H. Zhang, P. Jagtap, A. Clark, and S. Kolathaya, “Learning a formally verified control barrier function in stochastic environment,” in 2024 IEEE 63rd Conference on Decision and Control (CDC) , 2024, pp. 4098–4104

    2024

  18. [25]

    Learning barrier functions with memory for robust safe navigation,

    K. Long, C. Qian, J. Cort ´es, and N. Atanasov, “Learning barrier functions with memory for robust safe navigation,” IEEE Robotics and Automation Letters, vol. 6, no. 3, pp. 4931–4938, 2021

    2021

  19. [26]

    Barriernet: Differentiable control barrier functions for learning of safe robot control,

    W. Xiao, T.-H. Wang, R. Hasani, M. Chahine, A. Amini, X. Li, and D. Rus, “Barriernet: Differentiable control barrier functions for learning of safe robot control,” IEEE Transactions on Robotics , 2023

    2023

  20. [27]

    Learning safe neural network controllers with barrier certificates,

    H. Zhao, X. Zeng, T. Chen, Z. Liu, and J. Woodcock, “Learning safe neural network controllers with barrier certificates,” Formal Aspects of Computing, vol. 33, pp. 437–455, 2021

    2021

  21. [28]

    Exact verification of relu neural control barrier functions,

    H. Zhang, J. Wu, Y . V orobeychik, and A. Clark, “Exact verification of relu neural control barrier functions,” Advances in neural information processing systems, vol. 36, pp. 5685–5705, 2023

    2023

  22. [29]

    Fossil: A software tool for the formal synthesis of Lyapunov functions and barrier certificates using neural networks,

    A. Abate, D. Ahmed, A. Edwards, M. Giacobbe, and A. Peruffo, “Fossil: A software tool for the formal synthesis of Lyapunov functions and barrier certificates using neural networks,” in Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control ...

    2021

  23. [30]

    Fossil 2.0: Formal certificate synthesis for the verification and control of dynamical models,

    A. Edwards, A. Peruffo, and A. Abate, “Fossil 2.0: Formal certificate synthesis for the verification and control of dynamical models,” in Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control , 2024, pp. 1–10

    2024

  24. [31]

    Design-while- verify: correct-by-construction control learning with verification in the loop,

    Y . Wang, C. Huang, Z. Wang, Z. Wang, and Q. Zhu, “Design-while- verify: correct-by-construction control learning with verification in the loop,” in Proceedings of the 59th ACM/IEEE Design Automation Con- ference, 2022, pp. 925–930

    2022

  25. [32]

    Seev: Synthesis with efficient exact verification for relu neural barrier functions,

    H. Zhang, Z. Qin, S. Gao, and A. Clark, “Seev: Synthesis with efficient exact verification for relu neural barrier functions,” Advances in Neural Information Processing Systems , vol. 37, pp. 101 367–101 392, 2025

    2025

  26. [33]

    Set invariance in control,

    F. Blanchini, “Set invariance in control,” Automatica, vol. 35, no. 11, pp. 1747–1767, 1999

    1999

  27. [34]

    Deepreach: A deep learning approach to high-dimensional reachability,

    S. Bansal and C. J. Tomlin, “Deepreach: A deep learning approach to high-dimensional reachability,” in 2021 IEEE International Conference on Robotics and Automation (ICRA) . IEEE, 2021, pp. 1817–1824

    2021

  28. [35]

    End-to-end safe reinforcement learning through barrier functions for safety-critical continuous control tasks,

    R. Cheng, G. Orosz, R. M. Murray, and J. W. Burdick, “End-to-end safe reinforcement learning through barrier functions for safety-critical continuous control tasks,” in Proceedings of the AAAI conference on artificial intelligence, vol. 33, no. 01, 2019, pp. 3387–3395

    2019

  29. [36]

    A framework for worst- case and stochastic safety verification using barrier certificates,

    S. Prajna, A. Jadbabaie, and G. J. Pappas, “A framework for worst- case and stochastic safety verification using barrier certificates,” IEEE Transactions on Automatic Control, vol. 52, no. 8, pp. 1415–1428, 2007

    2007

  30. [37]

    Safety index synthesis via sum-of-squares programming,

    W. Zhao, T. He, T. Wei, S. Liu, and C. Liu, “Safety index synthesis via sum-of-squares programming,” in 2023 American Control Conference (ACC). IEEE, 2023, pp. 732–737

    2023

  31. [38]

    Verification and synthesis of compatible control lyapunov and control barrier functions,

    H. Dai, C. Jiang, H. Zhang, and A. Clark, “Verification and synthesis of compatible control lyapunov and control barrier functions,” arXiv preprint arXiv:2406.18914, 2024

    2024 arXiv

  32. [39]

    SOS construc- tion of compatible control lyapunov and barrier functions,

    M. Schneeberger, F. D ¨orfler, and S. Mastellone, “SOS construc- tion of compatible control lyapunov and barrier functions,” IFAC- PapersOnLine, vol. 56, no. 2, pp. 10 428–10 434, 2023

    2023

  33. [40]

    Learning safe multi-agent control with decentralized neural barrier certificates,

    Z. Qin, K. Zhang, Y . Chen, J. Chen, and C. Fan, “Learning safe multi-agent control with decentralized neural barrier certificates,” arXiv preprint arXiv:2101.05436, 2021

    2021 arXiv

  34. [41]

    Quantifying safety of learning-based self-driving control using almost-barrier functions,

    Z. Qin, T.-W. Weng, and S. Gao, “Quantifying safety of learning-based self-driving control using almost-barrier functions,” in 2022 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS) . IEEE, 2022, pp. 12 903–12 910

    2022

  35. [42]

    Safe control under input limits with neural control barrier functions,

    S. Liu, C. Liu, and J. Dolan, “Safe control under input limits with neural control barrier functions,” in Conference on Robot Learning . PMLR, 2023, pp. 1970–1980

    2023

  36. [43]

    Fault tolerant neural control barrier functions for robotic systems under sensor faults and attacks,

    H. Zhang, L. Niu, A. Clark, and R. Poovendran, “Fault tolerant neural control barrier functions for robotic systems under sensor faults and attacks,” in 2024 IEEE International Conference on Robotics and Automation (ICRA). IEEE, 2024, pp. 9901–9907

    2024

  37. [44]

    Efficient neural network robustness certification with general activation functions,

    H. Zhang, T.-W. Weng, P.-Y . Chen, C.-J. Hsieh, and L. Daniel, “Efficient neural network robustness certification with general activation functions,” Advances in Neural Information Processing Systems, vol. 31, pp. 4939–4948, 2018. [Online]. Available: https://arxiv.org/pdf/181...

    2018

  38. [45]

    Automatic perturbation analysis for scalable certified robustness and beyond,

    K. Xu, Z. Shi, H. Zhang, Y . Wang, K.-W. Chang, M. Huang, B. Kailkhura, X. Lin, and C.-J. Hsieh, “Automatic perturbation analysis for scalable certified robustness and beyond,” Advances in Neural Information Processing Systems , vol. 33, 2020

    2020

  39. [46]

    A convex relaxation barrier to tight robustness verification of neural networks,

    H. Salman, G. Yang, H. Zhang, C.-J. Hsieh, and P. Zhang, “A convex relaxation barrier to tight robustness verification of neural networks,” Advances in Neural Information Processing Systems , vol. 32, pp. 9835– 9846, 2019

    2019

  40. [47]

    Fast and Complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers,

    K. Xu, H. Zhang, S. Wang, Y . Wang, S. Jana, X. Lin, and C.-J. Hsieh, “Fast and Complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers,” in International Conference on Learning Representations , 2021. [Online]. Available:...

    2021

  41. [48]

    Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verifi- cation,

    S. Wang, H. Zhang, K. Xu, X. Lin, S. Jana, C.-J. Hsieh, and J. Z. Kolter, “Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verifi- cation,” Advances in Neural Information Processing Systems , vol. 34, 2021

    2021

  42. [49]

    A branch and bound framework for stronger adversarial attacks of ReLU networks,

    H. Zhang, S. Wang, K. Xu, Y . Wang, S. Jana, C.-J. Hsieh, and Z. Kolter, “A branch and bound framework for stronger adversarial attacks of ReLU networks,” in Proceedings of the 39th International Conference on Machine Learning , vol. 162, 2022, pp. 26 591–26 604

    2022

  43. [50]

    Verification of neural control barrier functions with symbolic derivative bounds propagation,

    H. Hu, Y . Yang, T. Wei, and C. Liu, “Verification of neural control barrier functions with symbolic derivative bounds propagation,” arXiv preprint arXiv:2410.16281, 2024

    2024 arXiv

  44. [51]

    Revuz and M

    D. Revuz and M. Yor, Continuous martingales and Brownian motion . Springer Science & Business Media, 2013, vol. 293

    2013

  45. [53]

    Semidefinite programming relaxations for semialgebraic problems,

    P. A. Parrilo, “Semidefinite programming relaxations for semialgebraic problems,” Mathematical programming, vol. 96, pp. 293–320, 2003. 16

    2003

  46. [54]

    Matou ˇsek and B

    J. Matou ˇsek and B. G ¨artner, Understanding and using linear program- ming. Springer, 2007, vol. 1

    2007

  47. [55]

    Almost-sure safety guarantees of stochastic zero-control barrier functions do not hold,

    O. So, A. Clark, and C. Fan, “Almost-sure safety guarantees of stochastic zero-control barrier functions do not hold,” arXiv preprint arXiv:2312.02430, 2023

    2023 arXiv

  48. [56]

    Training robust neural networks using lipschitz bounds,

    P. Pauli, A. Koch, J. Berberich, P. Kohler, and F. Allg ¨ower, “Training robust neural networks using lipschitz bounds,” IEEE Control Systems Letters, vol. 6, pp. 121–126, 2021

    2021

  49. [57]

    Constructive feedforward neural networks using hermite polynomial activation functions,

    L. Ma and K. Khorasani, “Constructive feedforward neural networks using hermite polynomial activation functions,” IEEE Transactions on Neural Networks, vol. 16, no. 4, pp. 821–833, 2005

    2005

  50. [58]

    Karatzas and S

    I. Karatzas and S. Shreve, Brownian motion and stochastic calculus . Springer Science & Business Media, 1991, vol. 113

    1991

  51. [59]

    S. J. Russell and P. Norvig, Artificial intelligence: a modern approach . pearson, 2016

    2016

  52. [60]

    Darboux-type barrier certificates for safety verification of nonlinear hybrid systems,

    X. Zeng, W. Lin, Z. Yang, X. Chen, and L. Wang, “Darboux-type barrier certificates for safety verification of nonlinear hybrid systems,” in Proceedings of the 13th International Conference on Embedded Software, 2016, pp. 1–10

    2016

  53. [61]

    Safety verification of reactive controllers for uav flight in cluttered environments using barrier certificates,

    A. J. Barry, A. Majumdar, and R. Tedrake, “Safety verification of reactive controllers for uav flight in cluttered environments using barrier certificates,” in 2012 IEEE International Conference on Robotics and Automation. IEEE, 2012, pp. 484–490. Hongchao Zhang (SM’24) is a P...

    2016

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.