REVIEW 3 major objections 4 minor 37 references
Sample Efficient Certification of Discrete-Time Control Barrier Functions
T0 review · 3 major / 4 minor · reviewed 2026-08-05 · deepseek-v4-flash
Pith's one-line read Verifying a discrete-time control barrier function can be done with progressively fewer samples toward the interior of the safe set.
desk verdict Real theoretical contribution, but the numerical certificate uses a lower bound as an upper bound—repairable, but the sample-efficiency claim needs rework. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
Level-segment epsilon-net certification. The central device is the partition of S(0) into level sets C_i = {x : gamma_{i-1} <= h(x) <= gamma_i} together with an epsilon_i-net D_i over each C_i. The proof mechanism is a Lipschitz propagation inequality that bounds h(f(x)) - (1-alpha_bar)h(x) at an arbitrary x by its value at the nearest sample plus terms proportional to epsilon_i, so a sample-level check plus a distance bound yields the pointwise certificate. The second device is the recurrence gamma_{i+1} = a gamma_i + b delta from Proposition 4, which chooses the level thresholds so that the segment widths track the admissible epsilon_i; its fixed point gamma_hat defines the invariant subse
What would settle it
Reproduce the numerical example, then compute the maximum ratio ||f(x1,u(x1))-f(x2,u(x2))||/||x1-x2|| over a much denser set of pairs inside the segment closest to h=0. If any ratio exceeds the reported Lf=1.4325, use that pair's neighborhood to locate an x whose nearest verified sample is within the epsilon_i used in Table I and evaluate r(x)+alpha_bar h(x); a positive value is a direct counterexample to the certified barrier inequality (20).
Extended reading notes
Core claim
Proposition 2 is the load-bearing result. Let alpha in [0,1] be the decay used in synthesis, alpha_bar in [alpha,1] the decay to be certified, and suppose each level segment C_i is sampled by a set D_i that is an epsilon_i-net. If every sample satisfies r(x) = h(f(x))-h(x) <= -alpha h(x) - delta, then the barrier inequality r(x) <= -alpha_bar h(x) holds for every x in S(0) whenever epsilon_i <= (delta + (alpha_bar-alpha)|gamma_i|)/(L_h L_f + (1-alpha_bar)L_h), with L_h and L_f upper bounds on the Lipschitz constants of h and the closed-loop map. Because |gamma_i| is largest for segments far from the boundary, the admissible epsilon_i grows toward the interior. The paper also converts this in
Load-bearing premise
The proof requires a genuine upper bound on the Lipschitz constant of the closed-loop dynamics f(x,u(x)), but Algorithm 1 only estimates a lower bound from finitely many sampled pairs; if the true constant is larger, the required sampling densities in (21) are too optimistic and the certificate may not hold.
Editorial extensions
If this is right
- Under Proposition 2, a user who only needs safety rather than a specified decay rate can set alpha_bar = 1 and use the loosest epsilon_i bounds, making pure invariance certification the cheapest case.
- Enforcing a positive margin delta buys a quantifiable inner invariant set S(gamma_hat), so the certificate includes an explicit safety buffer between the certified region and the boundary of S(0).
- A failed verification returns a concrete violating state, so the certifier can be scripted as a loop: certify, append the violating sample to the training set, re-solve the penalized synthesis, and re-certify.
- The reported 2D example needs roughly 1.1e5 to 2.7e5 samples where a one-shot cover needs 2.0e6 to 2.8e6, making verification computationally accessible for this class of problems.
- The probabilistic bound (36) grows exponentially with state dimension, so the practical payoff is currently concentrated in low-dimensional settings unless tighter 0-1 risk bounds are found.
Reading between the lines
- A natural extension not developed in the paper would replace the sampled lower-bound estimate of L_f with a certified upper bound, for example from interval propagation or Lipschitz-bounded network architectures; then the certificates would be logically unconditional rather than contingent on the estimate.
- The same level-segment stratification could be used during synthesis to place training samples preferentially near the boundary, where the verification epsilon_i is smallest, instead of sampling uniformly over D.
- The result suggests an adaptive refinement strategy for higher-dimensional problems: allocate samples only to segments where the current epsilon_i bound is binding, and keep coarse nets where |gamma_i| is large, rather than refining the whole grid at once.
- One can test whether the approach extends to continuous-time CBFs by applying the same stratification to a sampled flow map of the closed-loop continuous system; the paper's bounds are explicitly discrete-time, so that extension would require a new derivation.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper proposes a certification procedure for discrete-time control barrier functions (DT-CBFs) based on Lipschitz continuity and level-set decomposition. The core idea is that the sampling density required for verifying the barrier decrease condition can be coarser away from the boundary of the CBF's sublevel set. The authors formalize this through Proposition 2, which gives a bound on the sampling resolution ϵ_i in terms of the CBF level γ_i, and then derive probabilistic sample-complexity bounds (Propositions 7–9). A synthesis formulation via a penalized learning problem and a certification algorithm (Algorithm 1) are provided, with a numerical example demonstrating improved sample efficiency over a one-shot verification approach.
Significance. If the identified gaps are addressed, the paper makes a useful contribution: it gives a level-dependent discretization criterion for DT-CBF verification, which is a natural and nontrivial extension of grid-based and Lipschitz-based certification methods. The theoretical framework is clearly presented, with deterministic and probabilistic sample-complexity bounds, and the authors provide a code link for reproducibility. However, the numerical validation currently rests on an invalid Lipschitz estimate, and the probabilistic and set-certification claims are incomplete as written. The core Proposition 2 is mathematically plausible, but the numerical evidence for the central sample-efficiency claim is not yet justified.
major comments (3)
- [Section IV-C, Eq. (21)] Algorithm 1 Step 1 estimates 'a lower bound to Lf' by sampling pairs, but Proposition 2 requires Lf to be an upper bound on the true closed-loop Lipschitz constant. In Section V, the value Lf=1.4325 is then used directly in (21). Since a sampled lower bound cannot certify an upper bound, the resulting ε_i values may exceed the admissible resolution, and the implication from (18) to (20) does not follow. The certificate reported in Table I is therefore not justified. Please use a certified upper bound (e.g., via Lipschitz bounds for the neural-network controller and dynamics) or clearly state a confidence interval and account for the uncertainty in the final certificate.
- [Section V, Algorithm 1] The parameter θ is an input to Algorithm 1 and appears in κθ(Ni) in Proposition 7 and in the confidence statement of Proposition 9, but no value of θ is reported in the numerical example. Without θ, the reported sample counts Ntot in Table I cannot be reproduced and the confidence of the probabilistic certificate is unspecified. Please report the chosen θ (and the resulting confidence (1−θ)^q).
- [Section IV.A, Problem 2] Proposition 4 verifies invariance of S(γ̂), not of S(0). In the verification procedure, the authors set γ_q = γ̂ and certify the barrier condition only on S(γ̂). However, Problem 2 asks for conditions under which S(0) is a CI set, and the paper's abstract/conclusion claim certification of the 0-sublevel set. This is a mismatch between the verified object and the stated certificate. To resolve this, either verify that X_s ⊆ S(γ̂) and adapt the problem statement, or provide conditions under which certification on S(γ̂) implies the original S(0) claim.
minor comments (4)
- [Eq. (25)] The denominator in the definition of b appears to be missing an L_h: it should be L_h L_f + (1−ᾱ)L_h, consistent with the preceding derivation. Although L_h cancels in the final expression for γ̂, the displayed formula is incorrect.
- [Section V] Typo: 'warm-staded' should be 'warm-started'.
- [Proposition 9] The confidence statement '(1−θ)^q' implicitly assumes independence across the q segments; if only individual segment bounds are used, the union bound gives 1−qθ. Please state the independence assumption explicitly.
- [Notation] The symbol B is overloaded: it denotes a box in Proposition 5, the unit 2-norm ball in Proposition 6, and a set in the numerical example. Please use distinct symbols to avoid confusion.
Circularity Check
No significant circularity: the verification bounds are derived from Lipschitz and concentration arguments, not from the target certificate.
full rationale
The derivation chain from synthesis constraints (11) to verification bounds (21), (31), (36) is self-contained and does not reduce to its own inputs. Proposition 2 is a Lipschitz propagation argument: condition (18) verified on an epsilon_i-net over each level segment C_i is extended to all of S(0) using upper bounds L_h, L_f and the level bound gamma_i; the bound (21) is exactly the sufficient condition that makes the propagated residual non-positive, not a restatement of (18). The sample-size formulas (31)-(36) come from an external empirical-Bernstein bound [23] and a measure-concentration lemma [7]; neither is a self-citation, and neither assumes the barrier inequality at unsampled points. The numerical comparison N_tot < N_base compares two sample counts computed from the same formula for q=1 vs q>1; this is a mathematical consequence of the derived bound, not a fit to the certificate. The only self-citation is [27] (including Del Prete), which is a related-work pointer and is not load-bearing. A non-circular correctness caveat should be flagged: Proposition 2 requires L_f to be an upper Lipschitz bound, while Section IV-C (Algorithm 1, Step 1) explicitly samples pairs to 'estimate a lower bound to L_f', and Section V uses that estimate directly in (21); if the true closed-loop Lipschitz constant is larger, the numerical certificate in Table I would not be justified. This is an input-assumption violation, not a circular reduction, so it does not raise the circularity score. No circular step is present.
Assumptions & free parameters
free parameters (6)
- alpha (synthesis decay rate) =
0.01
- delta (verification slack) =
0.01
- alpha_bar (target verification decay rate) =
0.4, 0.6, 0.8 in Table I
- Lf (closed-loop Lipschitz estimate) =
1.4325
- Lh (barrier Lipschitz estimate) =
1.6854
- theta (confidence level) =
not reported
assumptions (7)
- domain assumption f(x,u) and h(x) are Lipschitz continuous on the relevant sets with constants Lf and Lh
- domain assumption The samples Di are i.i.d. draws from the uniform distribution on Ci
- standard math The empirical Bernstein bound of Maurer-Pontil [23, Theorem 4] is valid in the stated form
- standard math Lemma C.1 of Boffi et al. [7] bounding the in-radius of a measure-kappa set is valid
- domain assumption The QP-based controller u(x; theta_u) is continuous and Lipschitz in x, so the closed-loop system is Lipschitz
- ad hoc to paper The estimated Lf is an upper bound on the true closed-loop Lipschitz constant
- ad hoc to paper The safe set Xs is contained in S(gamma_hat), so that certifying S(gamma_hat) suffices for safety
Cite this review
Pith. "Pith review of Sample Efficient Certification of Discrete-Time Control Barrier Functions." pith.science (2026). https://pith.science/paper/73GUBEMQ
@misc{pith2026250903899,
author = {Pith},
title = {Pith review of: Sample Efficient Certification of Discrete-Time Control Barrier Functions},
year = {2026},
howpublished = {\url{https://pith.science/paper/73GUBEMQ}},
note = {Machine review of arXiv:2509.03899}
}
read the original abstract
Control Invariant (CI) sets are instrumental in certifying the safety of dynamical systems. Control Barrier Functions (CBFs) are effective tools to compute such sets, since the zero sublevel sets of CBFs are CI sets. However, computing CBFs generally involves addressing a complex robust optimization problem, which can be intractable. Scenario-based methods have been proposed to simplify this computation. Then, one needs to verify if the CBF actually satisfies the robust constraints. We present an approach to perform this verification that relies on Lipschitz arguments, and forms the basis of a certification algorithm designed for sample efficiency. Through a numerical example, we validated the efficiency of the proposed procedure.
Figures
Reference graph
Works this paper leans on
-
[1]
Ayush Agrawal and Koushil Sreenath. Discrete control barrier functions for safety-critical control of discrete systems with application to bipedal robot navigation. In Robotics: Science and Systems, volume 13, pages 1–10. Cambridge, MA, USA, 2017
work page 2017
-
[2]
Mohamadreza Ahmadi, Andrew Singletary, Joel W. Burdick, and Aaron D. Ames. Safe policy synthesis in multi-agent pomdps via discrete-time barrier functions. In 2019 IEEE 58th Conference on Decision and Control (CDC), pages 4797–4803, 2019
work page 2019
-
[3]
Lus F. C. Alberto, Tas R. Calliero, and Andre C. P. Martins. An invariance principle for nonlinear discrete autonomous dynamical systems. IEEE Transactions on Automatic Control, 52(4):692– 697, 2007
work page 2007
-
[4]
Ames, Samuel Coogan, Magnus Egerstedt, Gennaro Notomista, Koushil Sreenath, and Paulo Tabuada
Aaron D. Ames, Samuel Coogan, Magnus Egerstedt, Gennaro Notomista, Koushil Sreenath, and Paulo Tabuada. Control barrier functions: Theory and applications. In 2019 18th European Control Conference (ECC), pages 3420–3431, 2019
work page 2019
- [5]
-
[6]
Set-Theoretic Methods in Control
Franco Blanchini and Stefano Miani. Set-Theoretic Methods in Control. Springer International Publishing, 2015
work page 2015
-
[7]
Learning stability certificates from data
Nicholas Boffi, Stephen Tu, Nikolai Matni, Jean-Jacques Slo- tine, and Vikas Sindhwani. Learning stability certificates from data. In Jens Kober, Fabio Ramos, and Claire Tomlin, editors, Proceedings of the 2020 Conference on Robot Learning, volume 155 of Proceedings of Machine Learning Research, pages 1341–
work page 2020
- [8]
Show all 37 references
-
[9]
Brown, M
S. Brown, M. Khajenejad, S. Z. Yong, and S. Mart ´ınez. Comput- ing controlled invariant sets of nonlinear control-affine systems. arXiv preprint arXiv:2304.11757, 2023
2023 arXiv
-
[10]
Byrd, Peihuang Lu, Jorge Nocedal, and Ciyou Zhu
Richard H. Byrd, Peihuang Lu, Jorge Nocedal, and Ciyou Zhu. A limited memory algorithm for bound constrained optimization. SIAM Journal on Scientific Computing, 16(5):1190–1208, 1995
1995
-
[11]
Verification- aided learning of neural network barrier functions with termina- tion guarantees
Shaoru Chen, Lekan Molu, and Mahyar Fazlyab. Verification- aided learning of neural network barrier functions with termina- tion guarantees. arXiv preprint arXiv:2403.07308, 2024
2024 arXiv
-
[12]
G. Chesi. Domain of Attraction: Analysis and Control via SOS Programming. Lecture Notes in Control and Information Sciences. Springer London, 2011
2011
-
[13]
Verification and synthesis of control barrier functions
Andrew Clark. Verification and synthesis of control barrier functions. In 2021 60th IEEE Conference on Decision and Control (CDC), pages 6105–6112, 2021
2021
-
[14]
Safe reinforcement learning using robust control barrier functions
Yousef Emam, Gennaro Notomista, Paul Glotfelter, Zsolt Kira, and Magnus Egerstedt. Safe reinforcement learning using robust control barrier functions. IEEE Robotics and Automation Letters, pages 1–8, 2022
2022
-
[15]
Efficient and accurate estimation of lipschitz constants for deep neural networks
Mahyar Fazlyab, Alexander Robey, Hamed Hassani, Manfred Morari, and George Pappas. Efficient and accurate estimation of lipschitz constants for deep neural networks. Advances in neural information processing systems, 32, 2019
2019
-
[16]
Fiacchini, T
M. Fiacchini, T. Alamo, and E.F. Camacho. On the computation of convex robust control invariant sets for nonlinear systems. Automatica, 46(8):1334–1338, 2010
2010
-
[17]
Victor Freire and Marco M. Nicotra. Systematic design of discrete-time control barrier functions using maximal output admissible sets. IEEE Control Systems Letters, 7:1891–1896, 2023
2023
-
[18]
Ad- vances in the theory of control barrier functions: Addressing practical challenges in safe control synthesis for autonomous and robotic systems
Kunal Garg, James Usevitch, Joseph Breeden, Mitchell Black, Devansh Agrawal, Hardik Parwana, and Dimitra Panagou. Ad- vances in the theory of control barrier functions: Addressing practical challenges in safe control synthesis for autonomous and robotic systems. Annual Reviews...
2024
-
[19]
On the effectiveness of interval bound propagation for training verifiably robust models
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timo- thy Mann, and Pushmeet Kohli. On the effectiveness of interval bound propagation for training verifiably robust models. arXiv preprint arXiv:1810.12715, 2018
2018 arXiv
-
[20]
Kerrigan
Eric C. Kerrigan. Robust Constraint Satisfaction: Invariant Sets and Predictive Control. PhD thesis, University of Cambridge, 2000
2000
-
[21]
D. P. Kingma and J. Ba. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980, 2015
2015 arXiv
-
[22]
Milan Korda, Didier Henrion, and Colin N. Jones. Convex com- putation of the maximum controlled invariant set for discrete- time polynomial control systems. In 52nd IEEE Conference on Decision and Control, pages 7107–7112, 2013
2013
-
[23]
Empirical Bernstein Bounds and Sample-Variance Penalization
Andreas Maurer and Massimiliano Pontil. Empirical Bernstein Bounds and Sample-Variance Penalization. In Proc. 22nd Annual Conference on Learning Theory (COLT), July 2009
2009
-
[24]
Mitchell, A.M
I.M. Mitchell, A.M. Bayen, and C.J. Tomlin. A time-dependent hamilton-jacobi formulation of reachable sets for continuous dynamic games. IEEE Transactions on Automatic Control, 50(7):947–957, 2005
2005
-
[25]
Jorge Nocedal and Stephen J. Wright. Numerical Optimization. Springer, New York, NY , USA, 2e edition, 2006
2006
-
[26]
Fast verification of control barrier functions via linear programming
Ellie Pond and Matthew Hale. Fast verification of control barrier functions via linear programming. IFAC-PapersOnLine, 56(2):10595–10600, 2023. 22nd IFAC World Congress
2023
-
[27]
Vboc: Learning the viability boundary of a robot manipulator us- ing optimal control
Asia La Rocca, Matteo Saveriano, and Andrea Del Prete. Vboc: Learning the viability boundary of a robot manipulator us- ing optimal control. IEEE Robotics and Automation Letters, 8(11):6971–6978, 2023
2023
-
[28]
Scalable computation of robust control invariant sets of nonlinear systems
Lukas Sch ¨afer, Felix Gruber, and Matthias Althoff. Scalable computation of robust control invariant sets of nonlinear systems. IEEE Transactions on Automatic Control, 69(2):755–770, 2024
2024
-
[29]
Shakhesi
E. Shakhesi. Verification and synthesis of discrete-time control barrier functions. Master’s thesis, TU Eindhoven, Nov 2023. Accessed: date-of-access
2023
-
[30]
Strong and Leila J
Amy K. Strong and Leila J. Bridgeman. Data driven verification of positive invariant sets for discrete, nonlinear systems. In Alessandro Abate, Mark Cannon, Kostas Margellos, and Anto- nis Papachristodoulou, editors, Proceedings of the 6th Annual Learning for Dynamics &; Contr...
2024
-
[31]
Intriguing properties of neural networks
Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus. Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199, 2013
2013 arXiv
-
[32]
Dimarogonas
Xiao Tan and Dimos V . Dimarogonas. Compatibility checking of multiple control barrier functions for input constrained systems. In 2022 IEEE 61st Conference on Decision and Control (CDC), pages 939–944, 2022
2022
-
[33]
Predictive control barrier functions: Enhanced safety mechanisms for learning- based control
Kim P Wabersich and Melanie N Zeilinger. Predictive control barrier functions: Enhanced safety mechanisms for learning- based control. IEEE Transactions on Automatic Control, 68(5):2638–2651, 2022
2022
-
[34]
Safety verification and controller synthesis for systems with input constraints
Han Wang, Kostas Margellos, and Antonis Papachristodoulou. Safety verification and controller synthesis for systems with input constraints. IFAC-PapersOnLine, 56(2):1698–1703, 2023. 22nd IFAC World Congress
2023
-
[35]
Safety-critical model predictive control with discrete-time control barrier func- tion
Jun Zeng, Bike Zhang, and Koushil Sreenath. Safety-critical model predictive control with discrete-time control barrier func- tion. In 2021 American Control Conference (ACC), pages 3882– 3889, 2021
2021
-
[36]
Exact verification of relu neural control barrier functions
Hongchao Zhang, Junlin Wu, Yevgeniy V orobeychik, and An- drew Clark. Exact verification of relu neural control barrier functions. Advances in neural information processing systems, 36:5685–5705, 2023
2023
-
[1350]
PMLR, 16–18 Nov 2021
2021
Reviewed August 5, 2026 · model on record in the stance chip above.
Discussion (0). Sign in to comment.