arxiv: 2605.02526 · v1 · submitted 2026-05-04 · 📡 eess.SY · cs.AI· cs.SY

Recognition: 2 theorem links

· Lean Theorem

Set-Based Training of Neural Barrier Certificates for Safety Verification of Dynamical Systems

Miriam Kranzlm\"uller , Lukas Koller , Tobias Ladner , Matthias Althoff

Authors on Pith no claims yet

Pith reviewed 2026-05-08 18:27 UTC · model grok-4.3

classification 📡 eess.SY cs.AIcs.SY

keywords barrier certificatesneural networkssafety verificationdynamical systemsset-based trainingformal verification

0 comments

The pith

A set-based loss during neural network training proves barrier certificate validity when it reaches zero.

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

The paper aims to replace the usual loop of training a candidate neural barrier certificate and then formally checking it with a single training run. It does this by designing a loss function over sets of states that encodes every condition a valid barrier certificate must satisfy. Reaching zero loss then means the network separates all unsafe states from all reachable ones for the given dynamical system. A reader would care because this removes the separate verification step that often slows down safety proofs for high-dimensional or nonlinear systems.

Core claim

The authors establish that a neural network can be trained as a barrier certificate using a set-based loss function such that a loss value of zero formally proves the network satisfies all barrier certificate properties and therefore verifies the safety of the dynamical system. This collapses the previous iterative process of candidate generation followed by verification into one optimization procedure.

What carries the argument

A set-based loss function that encodes the barrier certificate conditions over sets of states to ensure the network separates unsafe states from reachable states for arbitrary nonlinear dynamics.

If this is right

Training and verification become a single procedure with no separate post-training check required.
The approach scales with increasing state dimension according to the reported experiments.
Complex nonlinear dynamics can be handled directly without linearization or other simplifications.
A zero-loss outcome supplies a formal safety guarantee for the system.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same set-based encoding idea could be adapted to certify properties beyond safety, such as stability or reachability.
Integrating this training method with policy optimization might produce controllers that are safe by construction.
If the loss can be extended to hybrid or switched systems, the method would apply to a wider class of control problems.

Load-bearing premise

That a differentiable set-based loss can be written and optimized to capture every barrier certificate property exactly without leaving any soundness gaps for arbitrary nonlinear systems.

What would settle it

An example dynamical system in which a network reaches zero loss yet still allows an unsafe state to be reachable, or a valid barrier certificate that the method fails to find.

Figures

Figures reproduced from arXiv: 2605.02526 by Lukas Koller, Matthias Althoff, Miriam Kranzlm\"uller, Tobias Ladner.

**Figure 1.** Figure 1: Overview: (a) Prior work trains a candidate barrier certificate Bθ using samples of the state space. The validity of the barrier certificate is verified using a separate verification step. If a counterexample is found, Bθ has to be retrained, resulting in repeated training-verification cycles. (b) In contrast, we use set-based training to integrate the verification directly into the training step, i.e., a … view at source ↗

**Figure 2.** Figure 2: Visualization of the neural barrier certificate at different stages of the training process. Finally, we penalize the upper bound of each set, i.e., for YZ,i = h yZ,i , yZ,i i and some small ϵ > 0: LIII(YZ) := X λ i=1 max(0, yZ,i + ϵ). (13) Hence, if LIII(YZ) = 0, then for all i ∈ [λ]: yZ,i +ϵ ≤ 0, i.e., yZ,i ≤ −ϵ < 0, and hence P III is satisfied. We require ϵ > 0 to enforce the strict inequality required… view at source ↗

**Figure 3.** Figure 3: We enclose the zero-level set by recursively splitting the state space and enclosing the preimage enclosure to discard input regions that do not contain a zero point. After four iterations we achieve a tight enclosure of the zero-level set. we can compute the flow exactly using an affine map (2); other dynamics have to be enclosed, e.g., using range bounding based on interval arithmetic [23, Sec. 2.3.3] or… view at source ↗

**Figure 4.** Figure 4: Visualization of computed barrier certificates for different benchmarks. In summary, our approach is the only method that solves all considered benchmarks at 100% success rate, handles more expressive dynamics and set representations than SynNBC and PRoTECT, and is faster than FOSSIL. B. Training Epochs vs. Training-Verification Cycles Recall that our approach does not require a separate verification step ( view at source ↗

read the original abstract

Barrier certificates are scalar functions over the state space of dynamical systems that separate all unsafe states from all reachable states. The existence of a barrier certificate formally verifies the safety of the dynamical system. Recent approaches synthesize barrier certificates by iteratively training a neural network. In each iteration, the candidate is formally verified - if successful, the barrier certificate is found. Instead, we propose a set-based training approach that tightly integrates verification into training via a set-based loss function that soundly encodes all barrier certificate properties. A loss of zero formally proves the validity of the barrier certificate, collapsing the iterative training and verification into a single training procedure. Our experiments demonstrate that our set-based training approach scales well with the system dimension and naturally handles complex nonlinear dynamics.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The set-based loss collapses training and verification only if the encoding of the Lie derivative over the full sublevel set is tight and gap-free for nonlinear f.

read the letter

The main takeaway is that this work trains a neural barrier certificate with a loss built from set-based bounds on the initial, unsafe, and Lie-derivative conditions, so that a zero loss is meant to certify validity without a separate verification step afterward. That integration is the concrete novelty relative to the iterative train-then-check loops in prior neural-barrier papers. The experiments reportedly show improved scaling with dimension and better handling of nonlinear dynamics, which addresses a practical bottleneck in robotics and control verification. Credit is due for making the set-propagation machinery part of the optimization rather than an after-the-fact check. The central soft spot is exactly the one the stress-test flags: for arbitrary nonlinear f, the loss must soundly upper-bound the violation of ∇B · f ≤ 0 over the entire sublevel set {x | B(x) ≤ 0}. If the sublevel-set representation or the set propagation (intervals, zonotopes, Taylor models) introduces looseness or relies on sampling, then zero loss on the surrogate does not entail the condition everywhere and post-training verification is still required. The abstract asserts soundness, but without the explicit loss terms and the error analysis it is hard to judge how tight the bounds stay during training. Minor additional questions are whether the method assumes Lipschitz or polynomial dynamics for the set operations and how initialization affects convergence to a true zero-loss point. This paper is aimed at people working on scalable formal safety verification for high-dimensional or nonlinear systems; a reader already familiar with barrier certificates and set-based reachability will extract the most value from the scaling data and the collapsed workflow. The claim is specific enough and the experimental focus on dimension and nonlinearity is relevant, so it deserves a serious referee even if the soundness details need tightening in revision.

Referee Report

3 major / 1 minor

Summary. The manuscript proposes a set-based training procedure for neural barrier certificates in dynamical systems. Instead of alternating between neural network training and separate formal verification, the authors define a set-based loss that encodes the three barrier conditions (B ≤ 0 on the initial set, B > 0 on the unsafe set, and Lie derivative condition on the sublevel set {B ≤ 0}). They claim that a loss value of exactly zero constitutes a formal proof that the trained network is a valid barrier certificate, thereby collapsing training and verification into a single optimization step. Experiments are reported to show favorable scaling with state dimension and applicability to nonlinear dynamics.

Significance. If the soundness claim holds, the work would meaningfully simplify the synthesis-verification loop that currently dominates neural barrier certificate methods. By embedding set-based over-approximations directly into the loss, the approach could reduce reliance on external verifiers and improve scalability. The paper correctly identifies the integration of set propagation (intervals, zonotopes, or Taylor models) as the technical enabler; credit is due for attempting a parameter-free, self-certifying training objective.

major comments (3)

[Abstract and §3] Abstract and §3 (loss definition): the central claim that 'a loss of zero formally proves the validity' is load-bearing yet unsupported by any explicit construction or soundness theorem in the abstract. The manuscript must supply the precise mathematical form of the set-based loss L together with a proof that L = 0 implies the three barrier conditions hold over the entire continuous state space, not merely on the computed abstractions.
[§3] §3 (Lie derivative encoding): for arbitrary nonlinear f the condition ∇B·f ≤ 0 must be enforced over the whole sublevel set {x | B(x) ≤ 0}. If the set propagation used to bound this expression introduces sampling, non-conservative operations, or loose abstractions whose error is not rigorously bounded, then L = 0 on the computed loss does not entail the property everywhere; post-training verification would still be required and the claimed collapse fails.
[§4] §4 (experiments): the reported scaling with dimension is promising, but without quantitative data on the computational cost and tightness of the set propagations (e.g., number of generators in zonotopes, Taylor model order, or observed over-approximation error), it is impossible to assess whether the method remains practical or sound for the higher-dimensional nonlinear cases claimed.

minor comments (1)

Notation for the set representations and the precise definition of the sublevel-set abstraction should be introduced once and used consistently; currently the abstract leaves the reader uncertain whether the loss is defined via interval arithmetic, zonotopes, or another method.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the constructive and detailed feedback. The comments help clarify the presentation of our soundness claims and experimental evaluation. We address each major comment below and indicate the revisions planned for the next version of the manuscript.

read point-by-point responses

Referee: [Abstract and §3] Abstract and §3 (loss definition): the central claim that 'a loss of zero formally proves the validity' is load-bearing yet unsupported by any explicit construction or soundness theorem in the abstract. The manuscript must supply the precise mathematical form of the set-based loss L together with a proof that L = 0 implies the three barrier conditions hold over the entire continuous state space, not merely on the computed abstractions.

Authors: We agree that the abstract should contain the explicit mathematical form of the loss and a reference to the soundness result. In the revised manuscript we will add the precise definition of the set-based loss L to the abstract together with a concise statement of the soundness theorem. The full proof already appears in §3: the loss is constructed as the sum of three non-negative terms, each an upper bound (via sound set propagation) on the maximum violation of one barrier condition. Consequently L = 0 forces every term to be zero, which in turn forces the three conditions to hold over the entire continuous state space because the abstractions are conservative. revision: yes
Referee: [§3] §3 (Lie derivative encoding): for arbitrary nonlinear f the condition ∇B·f ≤ 0 must be enforced over the whole sublevel set {x | B(x) ≤ 0}. If the set propagation used to bound this expression introduces sampling, non-conservative operations, or loose abstractions whose error is not rigorously bounded, then L = 0 on the computed loss does not entail the property everywhere; post-training verification would still be required and the claimed collapse fails.

Authors: The set-propagation operators employed (interval arithmetic, zonotopes, and Taylor models) are strictly conservative; they never employ sampling or non-conservative operations. In the revised §3 we will insert explicit remainder bounds for the Taylor-model case and a short lemma showing that the computed upper bound on the Lie derivative is a rigorous over-approximation of the true supremum over the sublevel set. Because these bounds are part of the loss, L = 0 continues to imply the Lie-derivative condition everywhere, preserving the collapse of training and verification. revision: partial
Referee: [§4] §4 (experiments): the reported scaling with dimension is promising, but without quantitative data on the computational cost and tightness of the set propagations (e.g., number of generators in zonotopes, Taylor model order, or observed over-approximation error), it is impossible to assess whether the method remains practical or sound for the higher-dimensional nonlinear cases claimed.

Authors: We accept that additional quantitative information is needed for a complete assessment. The revised §4 will include new tables reporting, for each benchmark, the number of generators in the zonotope representations, the Taylor-model order used, wall-clock time spent on set propagation, and measured over-approximation error (difference between the propagated set and a high-fidelity Monte-Carlo reference). These data will allow readers to judge both practicality and tightness for the higher-dimensional nonlinear examples. revision: yes

Circularity Check

0 steps flagged

No significant circularity; set-based loss is an independent construction

full rationale

The paper defines a set-based loss that is asserted to soundly encode the three barrier conditions (Init, Unsafe, Lie derivative on sublevel set) for neural B. Zero loss is claimed to prove validity, collapsing training and verification. This is a proposed encoding and optimization target rather than a self-referential definition, a fitted parameter renamed as prediction, or a result that reduces to prior self-citations by construction. No equations or steps in the abstract reduce the central claim to its own inputs; the soundness of the set-propagation encoding is an external design claim, not a tautology. The approach is therefore self-contained against external benchmarks for the purpose of this circularity check.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The approach rests on standard domain assumptions from dynamical systems and neural approximation theory; no free parameters, new entities, or ad-hoc axioms are mentioned in the abstract.

axioms (2)

domain assumption The system dynamics are known and permit set-based over-approximations
Required to compute the set-based loss during training.
domain assumption Neural networks can represent barrier certificates sufficiently well for the systems considered
Standard assumption enabling the use of neural networks in this context.

pith-pipeline@v0.9.0 · 5431 in / 1271 out tokens · 48333 ms · 2026-05-08T18:27:13.892249+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

56 extracted references · 1 canonical work pages

[1]

Formal synthesis of neural barrier certificates for continuous systems via counterexample guided learning,

H. Zhao, N. Qi, L. Dehbi, X. Zeng, and Z. Yang, “Formal synthesis of neural barrier certificates for continuous systems via counterexample guided learning,”TECS, vol. 22, no. 146, pp. 1–21, 2023

2023
[2]

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 HSCC, no. 26, 2024, pp. 1–10

2024
[3]

Using online verification to prevent autonomous vehicles from causing accidents,

C. Pek, S. Manzinger, M. Koschi, and M. Althoff, “Using online verification to prevent autonomous vehicles from causing accidents,” Nat. Mach. Intell., vol. 2, no. 9, pp. 518–528, 2020

2020
[4]

Online verification of automated road vehicles using reachability analysis,

M. Althoff and J. Dolan, “Online verification of automated road vehicles using reachability analysis,”IEEE Trans. Robot., vol. 30, pp. 903–918, 2014

2014
[5]

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,” inICRA, 2012, pp. 484–490

2012
[6]

Advances in the theory of control barrier functions: addressing practical challenges in safe control synthesis for autonomous and robotic systems,

K. Garg, J. Usevitch, J. Breeden, M. Black, D. Agrawal, H. Parwana, and D. Panagou, “Advances in the theory of control barrier functions: addressing practical challenges in safe control synthesis for autonomous and robotic systems,”ARC, vol. 57, no. 100945, 2024

2024
[7]

Verification using simulation,

A. Girard and G. J. Pappas, “Verification using simulation,” inHSCC, 2006, pp. 272–286

2006
[8]

Reachability analysis and its application to the safety as- sessment of autonomous cars,

M. Althoff, “Reachability analysis and its application to the safety as- sessment of autonomous cars,” Ph.D. dissertation, Technische Universit¨at M¨unchen, 2010

2010
[9]

Barrier certificates for nonlinear model validation,

S. Prajna, “Barrier certificates for nonlinear model validation,”Automat- ica, vol. 42, pp. 117–126, 2006

2006
[10]

Safety verification of hybrid systems using barrier certificates,

S. Prajna and A. Jadbabaie, “Safety verification of hybrid systems using barrier certificates,” inHSCC, 2004, pp. 477–492

2004
[11]

Safe reinforcement learning for dynam- ical systems using barrier certificates,

Q. Zhao, Y . Zhang, and X. Li, “Safe reinforcement learning for dynam- ical systems using barrier certificates,”Conn. Sci., vol. 34, pp. 2822– 2844, 2022

2022
[12]

Verification of quantum systems using barrier certificates,

M. Lewis, P. Zuliani, and S. Soudjani, “Verification of quantum systems using barrier certificates,” inQEST, 2023, p. 346–362

2023
[13]

Synthesizing barrier certificates using neural networks,

H. Zhao, X. Zeng, T. Chen, and Z. Liu, “Synthesizing barrier certificates using neural networks,” inHSCC, no. 25, 2020, pp. 1–11

2020
[14]

Automated and formal synthesis of neural barrier certificates for dynamical models,

A. Peruffo, D. Ahmed, and A. Abate, “Automated and formal synthesis of neural barrier certificates for dynamical models,” inTACAS, 2021, pp. 370–388

2021
[15]

G. M. Ziegler,Lectures on polytopes. Springer New York, 1995

1995
[16]

Rigorously computed orbits of dynamical systems without the wrapping effect,

W. K ¨uhn, “Rigorously computed orbits of dynamical systems without the wrapping effect,”Computing, vol. 61, pp. 47–67, 1998

1998
[17]

Reachability analysis of nonlinear systems using conserva- tive polynomialization and non-convex sets,

M. Athoff, “Reachability analysis of nonlinear systems using conserva- tive polynomialization and non-convex sets,” inHSCC, 2013, pp. 173– 182

2013
[18]

Constrained zonotopes: A new tool for set-based estimation and fault detection,

J. K. Scott, D. M. Raimondo, G. R. Marseglia, and R. D. Braatz, “Constrained zonotopes: A new tool for set-based estimation and fault detection,”Automatica, vol. 69, pp. 126–136, 2016

2016
[19]

C. M. Bishop,Pattern recognition and machine learning. Springer New York, 2006

2006
[20]

Automatic abstraction refinement in neural network verification using sensitivity analysis,

T. Ladner and M. Althoff, “Automatic abstraction refinement in neural network verification using sensitivity analysis,” inHSCC, no. 18, 2023, pp. 1–13

2023
[21]

Set-based training for neural network verification,

L. Koller, T. Ladner, and M. Althoff, “Set-based training for neural network verification,”TMLR, 2025

2025
[22]

Out of the shadows: Exploring a latent space for neural network verification,

——, “Out of the shadows: Exploring a latent space for neural network verification,” inICLR, 2026

2026
[23]

Jaulin, M

L. Jaulin, M. Kieffer, O. Didrit, and E. Walter,Applied interval analysis. Springer London, 2001. KRANZLM ¨ULLERet al.: SET -BASED TRAINING OF NEURAL BARRIER CERTIFICATES FOR SAFETY VERIFICATION OF DYNAMICAL SYSTEMS xi

2001
[24]

Reachability analysis of nonlin- ear systems with uncertain parameters using conservative linearization,

M. Althoff, O. Stursberg, and M. Buss, “Reachability analysis of nonlin- ear systems with uncertain parameters using conservative linearization,” inIEEE CDC, 2008, pp. 4042–4048

2008
[25]

An introduction to CORA 2015,

M. Althoff, “An introduction to CORA 2015,” inARCH Workshop, vol. 34, 2015, pp. 120–151

2015
[26]

CORA manual,

M. Althoff, N. Kochdumper, T. Ladner, M. Perschl, and M. Wetzlinger, “CORA manual,” inTechnical University of Munich, 2025. [Online]. Available: https://cora.in.tum.de/manual

2025
[27]

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,” inEMSOFT, no. 11, 2016, pp. 1–10

2016
[28]

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,”TACON, vol. 52, pp. 1415–1428, 2007

2007
[29]

Providing a basin of attraction to a target region of polynomial systems by computation of lyapunov-like functions,

S. Ratschan and Z. She, “Providing a basin of attraction to a target region of polynomial systems by computation of lyapunov-like functions,” vol. 48, no. 7, 2006, pp. 4377–4394

2006
[30]

Abstraction of elementary hybrid systems by variable transformation,

J. Liu, N. Zhan, H. Zhao, and L. Zou, “Abstraction of elementary hybrid systems by variable transformation,” inFM, 2015, pp. 360–377

2015
[31]

Simulation based computation of certificates for safety of dynamical systems,

S. Ratschan, “Simulation based computation of certificates for safety of dynamical systems,” inFORMATS, 2017, pp. 303–317

2017
[32]

Understanding the difficulty of training deep feedforward neural networks,

X. Glorot and Y . Bengio, “Understanding the difficulty of training deep feedforward neural networks,” inAISTATS, vol. 9, 2010, pp. 249–256

2010
[33]

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,” inHSCC, no. 24, 2021, pp. 1–11

2021
[34]

Protect: Parallel construction of barrier certificates for safety verification of polynomial systems,

B. Wooding, V . Horbanov, and A. Lavaei, “Protect: Parallel construction of barrier certificates for safety verification of polynomial systems,” 2025, preprint: arXiv:2404.14804

work page arXiv 2025
[35]

A new barrier certificate for safety verification of hybrid systems,

H. Kong, X. Song, D. Han, M. Gu, and J. Sun, “A new barrier certificate for safety verification of hybrid systems,”Comp. J., vol. 57, pp. 1033– 1045, 2014

2014
[36]

Compositional safety analysis using barrier certificates,

C. Sloth, G. J. Pappas, and R. Wisniewski, “Compositional safety analysis using barrier certificates,” inHSCC, 2012, p. 15–24

2012
[37]

Barrier certificates revisited,

L. Dai, T. Gan, B. Xia, and N. Zhan, “Barrier certificates revisited,” Journal of Symbolic Computation, vol. 80, pp. 62–86, 2017

2017
[38]

Computation of parametric barrier functions for dynamical systems using interval analysis,

O. Bouissou, A. Chapoutot, A. Djaballah, and M. Kieffer, “Computation of parametric barrier functions for dynamical systems using interval analysis,” inCDC, 2014, pp. 753–758

2014
[39]

Simulation-guided lyapunov analysis for hybrid dynamical systems,

J. Kapinski, J. V . Deshmukh, S. Sankaranarayanan, and N. Arechiga, “Simulation-guided lyapunov analysis for hybrid dynamical systems,” inHSCC, 2014, p. 133–142

2014
[40]

Stochastic safety verification using barrier certificates,

S. Prajna, A. Jadbabaie, and G. J. Pappas, “Stochastic safety verification using barrier certificates,” inCDC, 2004, pp. 929–934

2004
[41]

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,” inECC, 2019, pp. 3420–3431

2019
[42]

Constructive safety using control barrier functions,

P. Wieland and F. Allg ¨ower, “Constructive safety using control barrier functions,” inIFAC, vol. 40, 2007, pp. 462–467

2007
[43]

Approximation by superpositions of a sigmoidal function,

G. V . Cybenko, “Approximation by superpositions of a sigmoidal function,”MCSS, vol. 2, pp. 303–314, 1989

1989
[44]

Multilayer feedforward networks are universal approximators,

K. Hornik, M. Stinchcombe, and H. White, “Multilayer feedforward networks are universal approximators,”Neural Netw., vol. 2, pp. 359– 366, 1989

1989
[45]

Multilayer feedforward networks with a nonpolynomial activation function can approximate any function,

M. Leshno, V . Y . Lin, A. Pinkus, and S. Schocken, “Multilayer feedforward networks with a nonpolynomial activation function can approximate any function,”Neural Netw., vol. 6, pp. 861–867, 1993

1993
[46]

A novel counterexample- guided inductive synthesis framework for barrier certificate generation,

M. Ding, K. Lin, W. Lin, and Z. Ding, “A novel counterexample- guided inductive synthesis framework for barrier certificate generation,” inISSRE, 2022, pp. 263–273

2022
[47]

Polynomial neural barrier certificate synthesis of hybrid systems via counterexample guidance,

H. Zhao, B. Liu, L. Dehbi, H. Xie, Z. Yang, and H. Qian, “Polynomial neural barrier certificate synthesis of hybrid systems via counterexample guidance,”TCAD, vol. 43, pp. 3756–3767, 2024

2024
[48]

Data- driven barrier certificate generation using deep learning and symbolic regression,

X. Ma, X. Zhang, N. Lv, X. Cao, W. Lin, and Z. Ding, “Data- driven barrier certificate generation using deep learning and symbolic regression,”JSA, vol. 165, p. 103419, 2025

2025
[49]

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,” inNeurIPS, 2024, pp. 101 367 – 101 392

2024
[50]

Neural Lyapunov control,

Y .-C. Chang, N. Roohi, and S. Gao, “Neural Lyapunov control,” in NeurIPS, 2019, pp. 3245–3254

2019
[51]

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 Trans. Robot., vol. 39, no. 3, pp. 1749–1767, 2023

2023
[52]

AI2: Safety and robustness certification of neural networks with abstract interpretation,

T. Gehr, M. Mirman, D. Drachsler-Cohen, P. Tsankov, S. Chaudhuri, and M. Vechev, “AI2: Safety and robustness certification of neural networks with abstract interpretation,” inIEEE S&P, 2018, pp. 3–18

2018
[53]

An abstract domain for certifying neural networks,

G. Singh, T. Gehr, M. P ¨uschel, and M. Vechev, “An abstract domain for certifying neural networks,”Proc. ACM Program. Lang., no. 41, 2019

2019
[54]

Reluplex: An efficient SMT solver for verifying deep neural networks,

G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer, “Reluplex: An efficient SMT solver for verifying deep neural networks,” inCAV, 2017, pp. 97–117

2017
[55]

Differentiable abstract interpre- tation for provably robust neural networks,

M. Mirman, T. Gehr, and M. Vechev, “Differentiable abstract interpre- tation for provably robust neural networks,” inICML, 2018

2018
[56]

Scalable verified training for provably robust image classification,

S. Gowal, K. Dvijotham, R. Stanforth, R. Bunel, C. Qin, J. Uesato, R. Arandjelovic, T. Mann, and P. Kohli, “Scalable verified training for provably robust image classification,” inICCV, 2019, pp. 4841–4850. Miriam Kranzlm ¨ ullerreceived the B.Sc. de- grees in mathematics and in computer science from Ludwig-Maximilians-Universit ¨at in Munich, Germany, in...

2019