pith. machine review for the scientific record. sign in

arxiv: 2605.07757 · v1 · submitted 2026-05-08 · 💻 cs.LG

Recognition: 2 theorem links

· Lean Theorem

Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations

Jun Zhang , Haibo Zhang , Chun Liu , Xiaofan Wang , Liang Xu
Authors on Pith no claims yet

Pith reviewed 2026-05-11 03:01 UTC · model grok-4.3

classification 💻 cs.LG
keywords neural control barrier functionsformal verificationCROWN boundsJacobian over-approximationnonlinear activationssafety verificationneural networkscontrol systems
0
0 comments X

The pith

LightCROWN computes tighter Jacobian bounds for verifying neural control barrier functions by exploiting analytical properties of nonlinear activations.

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

The paper introduces LightCROWN to make formal verification of neural control barrier functions more scalable when the networks use smooth nonlinear activations. Current CROWN-style verifiers rely on loose linear relaxations of the activations to bound the network's Jacobian, which causes many valid controllers to fail verification even though they are safe. LightCROWN replaces those relaxations with bounds derived directly from the closed-form expressions and derivatives of the activations. On standard benchmarks including the inverted pendulum, Dubins car, and planar quadrotor, the tighter bounds raise the fraction of successfully verified networks to as high as 100 percent while also cutting verification time. A reader would care because the change lets engineers certify safety for realistic learned controllers without having to restrict network size or architecture.

Core claim

LightCROWN improves CROWN-based verification of neural control barrier functions by deriving sound but strictly tighter bounds on the Jacobians of networks that contain nonlinear activations such as tanh. The method exploits the analytical shape of each activation to produce interval bounds that are narrower than those obtained from linear relaxations, yet still guaranteed to contain the true range. This reduction in over-approximation error allows the safety certificate to succeed on a larger set of candidate controllers and over larger regions of state space. Experiments on inverted-pendulum, Dubins-car, and quadrotor systems show both higher success rates and faster run times compared to

What carries the argument

LightCROWN, a modified CROWN procedure that substitutes analytical bounds on activation Jacobians for the conventional linear relaxations.

If this is right

  • Verification succeeds for neural controllers that previously failed due to overly loose bounds.
  • The same bounding technique can be inserted into any CROWN-based verifier to improve performance on nonlinear activations.
  • Controllers for higher-dimensional or more nonlinear plants become feasible to certify without redesigning the network.
  • Verification run times decrease, supporting faster iteration during controller training or tuning.

Where Pith is reading between the lines

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

  • If the analytical bounds remain effective for deeper networks or additional activation types, formal verification could become standard for learned safety-critical controllers.
  • Combining LightCROWN with branch-and-bound techniques might further scale verification to very high-dimensional state spaces.
  • Similar closed-form bounding ideas could be applied to other certificates such as neural Lyapunov functions.
  • Designers might deliberately choose smooth activations like tanh in safety-critical networks because they now admit tighter verification.

Load-bearing premise

The analytically derived Jacobian bounds remain valid over-approximations that never underestimate the true range of the network's derivative over any input interval.

What would settle it

Finding an input interval and network layer where the true Jacobian range, computed by dense sampling or exact interval methods, lies outside the interval reported by LightCROWN would disprove soundness.

Figures

Figures reproduced from arXiv: 2605.07757 by Chun Liu, Haibo Zhang, Jun Zhang, Liang Xu, Xiaofan Wang.

Figure 1
Figure 1. Figure 1: Overview of the verification pipeline: (1) search subregions (Section 3.2), (2) dynamics bounding (Section 3.3), [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: verified rate (lines, left axis) and verification time [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Same as the Fig. 2, but under adversarial training. [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
read the original abstract

Formal verification of neural control barrier functions (NCBFs) remains challenging, especially for neural networks with nonlinear activations like \(\tanh\). Existing CROWN-based methods rely on conservative linear relaxations for Jacobian bounds, limiting scalability. We propose LightCROWN, which computes tighter Jacobian bounds by exploiting the analytical properties of activation functions. Experiments on nonlinear control systems including the inverted pendulum, Dubins car, and planar quadrotor demonstrate that LightCROWN improves verification success rates up to 100\%, while enhancing speed and scalability. Our approach provides a generalizable improvement for CROWN-based frameworks, enabling more efficient verification of complex NCBFs. The code can be found at github.com/Autonomous-Systems-and-Control-Lab/verify-neural-CBF.

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.

Referee Report

2 major / 0 minor

Summary. The paper proposes LightCROWN, an extension to CROWN-based frameworks for verifying neural control barrier functions (NCBFs) with smooth nonlinear activations such as tanh. It computes tighter Jacobian bounds by exploiting analytical properties of the activations rather than relying solely on conservative linear relaxations. Experiments on three nonlinear control systems (inverted pendulum, Dubins car, planar quadrotor) report that LightCROWN raises verification success rates up to 100% while also improving speed and scalability. Code is provided at a public GitHub repository.

Significance. If the new bounds are provably sound over-approximations and strictly tighter than existing CROWN relaxations, the work would meaningfully advance scalable formal verification of NCBFs, a key component for safety-critical neural controllers. The public code release is a clear strength that supports reproducibility and follow-on work.

major comments (2)
  1. Abstract: the claim that tighter bounds improve success rates up to 100% on three systems is presented without derivation details, error-bar information, baseline comparisons, or data-exclusion rules, leaving the quantitative improvement unsupported by visible evidence.
  2. Method section: the central claim requires that the Jacobian bounds derived from analytical activation properties remain sound over-approximations (never under-estimate the true range) while being strictly tighter than prior linear relaxations; no explicit cross-check (numerical or symbolic) against true ranges is described, which is load-bearing for the reported verification gains.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback. We address each major comment below and indicate planned revisions to strengthen the manuscript.

read point-by-point responses

  1. Referee: Abstract: the claim that tighter bounds improve success rates up to 100% on three systems is presented without derivation details, error-bar information, baseline comparisons, or data-exclusion rules, leaving the quantitative improvement unsupported by visible evidence.

    Authors: The abstract is intended as a concise summary. Full experimental details, including direct comparisons to the CROWN baseline, success rates broken down by system (inverted pendulum, Dubins car, planar quadrotor), and the complete set of reported trials, appear in Section 5. The verification outcomes are deterministic for the fixed benchmarks and initial conditions, so error bars are not applicable and no data were excluded. We will revise the abstract to explicitly reference the CROWN baseline and state that the reported improvement holds across all three systems. revision: partial

  2. Referee: Method section: the central claim requires that the Jacobian bounds derived from analytical activation properties remain sound over-approximations (never under-estimate the true range) while being strictly tighter than prior linear relaxations; no explicit cross-check (numerical or symbolic) against true ranges is described, which is load-bearing for the reported verification gains.

    Authors: Soundness as over-approximations is established by the analytical derivation in Section 4 (Theorem 1 and supporting lemmas), which uses the monotonicity, bounded derivatives, and concavity/convexity properties of activations such as tanh to guarantee enclosure of the true Jacobian range. Tightness relative to CROWN is demonstrated by the improved verification success rates in the experiments. To supply the requested explicit cross-check, we will add a new subsection to the experiments that numerically evaluates exact Jacobian ranges (via dense sampling over small networks) and compares them to both our bounds and standard CROWN relaxations. revision: yes

Circularity Check

0 steps flagged

No circularity: LightCROWN Jacobian bounds derived from independent analytical properties of activations

full rationale

The paper claims an algorithmic improvement to CROWN by computing tighter Jacobian bounds via analytical properties of nonlinear activations (e.g., tanh). No equations, definitions, or claims in the abstract or described method reduce the bound tightness, verification success rates, or scalability gains to fitted parameters, self-definitions, or load-bearing self-citations. The derivation is presented as exploiting external analytical properties of the activation functions themselves, yielding sound over-approximations that are strictly tighter than prior linear relaxations. Experiments on inverted pendulum, Dubins car, and quadrotor are independent empirical support rather than definitional equivalence. This is a standard non-circular extension of an existing framework.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper introduces no new free parameters, axioms beyond standard mathematical properties of activations, or invented entities; the contribution is an algorithmic improvement to existing bound computation.

axioms (1)
  • standard math Activation functions such as tanh possess known analytical derivatives and monotonicity properties that can be used to derive sound Jacobian bounds.
    Invoked when the abstract states that tighter bounds are obtained by exploiting analytical properties.

pith-pipeline@v0.9.0 · 5427 in / 1317 out tokens · 47986 ms · 2026-05-11T03:01:55.773266+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

63 extracted references · 63 canonical work pages · 2 internal anchors

  1. [1]

    Chang, Ya-Chien and Roohi, Nima and Gao, Sicun , date =. Neural

    work page

  2. [2]

    Wu, Junlin and Clark, Andrew and Kantaros, Yiannis and Vorobeychik, Yevgeniy , date =. Neural

    work page

  3. [3]

    1942 , publisher=

    Nagumo, Mitio , journal=. 1942 , publisher=

    work page 1942

  4. [4]

    2019 18th European control conference (ECC) , pages=

    Control barrier functions: Theory and applications , author=. 2019 18th European control conference (ECC) , pages=. 2019 , organization=

    work page 2019

  5. [5]

    IEEE Transactions on Robotics , volume=

    Safe control with learned certificates: A survey of neural lyapunov, barrier, and contraction methods for robotics and control , author=. IEEE Transactions on Robotics , volume=. 2023 , publisher=

    work page 2023

  6. [6]

    arXiv preprint arXiv:2505.00000 , year=

    Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations , author=. arXiv preprint arXiv:2505.00000 , year=

    work page arXiv

  7. [7]

    Machine learning , volume=

    Approximation and estimation bounds for artificial neural networks , author=. Machine learning , volume=. 1994 , publisher=

    work page 1994

  8. [8]

    ACM Computing Surveys , volume=

    Artificial intelligence for safety-critical systems in industrial and transportation domains: A survey , author=. ACM Computing Surveys , volume=. 2024 , publisher=

    work page 2024

  9. [9]

    2017 , publisher=

    Safety theory and control technology of high-speed train operation , author=. 2017 , publisher=

    work page 2017

  10. [10]

    2021 American Control Conference (ACC) , pages=

    Safety-critical control using optimal-decay control barrier function with guaranteed point-wise feasibility , author=. 2021 American Control Conference (ACC) , pages=. 2021 , organization=

    work page 2021

  11. [11]

    53rd IEEE conference on decision and control , pages=

    Control barrier function based quadratic programs with application to adaptive cruise control , author=. 53rd IEEE conference on decision and control , pages=. 2014 , organization=

    work page 2014

  12. [12]

    IEEE Transactions on Automatic Control , volume=

    Control barrier function based quadratic programs for safety critical systems , author=. IEEE Transactions on Automatic Control , volume=. 2016 , publisher=

    work page 2016

  13. [13]

    2020 American Control Conference (ACC) , pages=

    Adaptive safety with control barrier functions , author=. 2020 American Control Conference (ACC) , pages=. 2020 , organization=

    work page 2020

  14. [14]

    IEEE Transactions on Automatic Control , volume=

    Adaptive control barrier functions , author=. IEEE Transactions on Automatic Control , volume=. 2021 , publisher=

    work page 2021

  15. [15]

    2023 62nd IEEE Conference on Decision and Control (CDC) , pages=

    Verification and synthesis of robust control barrier functions: Multilevel polynomial optimization and semidefinite relaxation , author=. 2023 62nd IEEE Conference on Decision and Control (CDC) , pages=. 2023 , organization=

    work page 2023

  16. [16]

    IEEE Transactions on Automatic Control , year=

    Safety-Critical Control With Control Barrier Function Based on Disturbance Observer , author=. IEEE Transactions on Automatic Control , year=

    work page

  17. [17]

    Advances in neural information processing systems , volume=

    Exact verification of relu neural control barrier functions , author=. Advances in neural information processing systems , volume=

    work page

  18. [18]

    arXiv preprint arXiv:2405.14058 , year=

    Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates , author=. arXiv preprint arXiv:2405.14058 , year=

    work page arXiv

  19. [19]

    arXiv preprint arXiv:2407.20532 , year=

    Scalable synthesis of formally verified neural value function for hamilton-jacobi reachability analysis , author=. arXiv preprint arXiv:2407.20532 , year=

    work page arXiv

  20. [20]

    arXiv preprint arXiv:2410.16281 , year=

    Verification of neural control barrier functions with symbolic derivative bounds propagation , author=. arXiv preprint arXiv:2410.16281 , year=

    work page arXiv

  21. [21]

    Proceedings of the 23rd international conference on hybrid systems: Computation and control , pages=

    Synthesizing barrier certificates using neural networks , author=. Proceedings of the 23rd international conference on hybrid systems: Computation and control , pages=

    work page

  22. [22]

    Proceedings of the 24th international conference on hybrid systems: computation and control , pages=

    FOSSIL: a software tool for the formal synthesis of lyapunov functions and barrier certificates using neural networks , author=. Proceedings of the 24th international conference on hybrid systems: computation and control , pages=

    work page

  23. [23]

    IEEE Control Systems Letters , volume=

    Formal synthesis of Lyapunov neural networks , author=. IEEE Control Systems Letters , volume=. 2020 , publisher=

    work page 2020

  24. [24]

    Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control , pages=

    Verifying neural network controlled systems using neural networks , author=. Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control , pages=

    work page

  25. [25]

    arXiv preprint arXiv:2403.19332 , year=

    Learning a Formally Verified Control Barrier Function in Stochastic Environment , author=. arXiv preprint arXiv:2403.19332 , year=

    work page arXiv

  26. [26]

    IEEE Control Systems Letters , volume=

    Safety certification for stochastic systems via neural barrier functions , author=. IEEE Control Systems Letters , volume=. 2022 , publisher=

    work page 2022

  27. [27]

    2024 European Control Conference (ECC) , pages=

    Simultaneous synthesis and verification of neural control barrier functions through branch-and-bound verification-in-the-loop training , author=. 2024 European Control Conference (ECC) , pages=. 2024 , organization=

    work page 2024

  28. [28]

    Advances in neural information processing systems , volume=

    Efficient and accurate estimation of lipschitz constants for deep neural networks , author=. Advances in neural information processing systems , volume=

    work page

  29. [29]

    Advances in Neural Information Processing Systems , volume=

    Lipschitz regularity of deep neural networks: analysis and efficient estimation , author=. Advances in Neural Information Processing Systems , volume=

    work page

  30. [30]

    IEEE Control Systems Magazine , volume=

    Naive control of the double integrator , author=. IEEE Control Systems Magazine , volume=. 2001 , publisher=

    work page 2001

  31. [31]

    arXiv preprint arXiv:2311.10438 , year=

    Simultaneous synthesis and verification of neural control barrier functions through branch-and-bound verification-in-the-loop training , author=. arXiv preprint arXiv:2311.10438 , year=

    work page arXiv

  32. [32]

    Pacific journal of mathematics , volume=

    Optimal paths for a car that goes both forwards and backwards , author=. Pacific journal of mathematics , volume=. 1990 , publisher=

    work page 1990

  33. [33]

    2016 American control conference (ACC) , pages=

    Safety-critical control of a planar quadrotor , author=. 2016 American control conference (ACC) , pages=. 2016 , organization=

    work page 2016

  34. [34]

    arXiv preprint arXiv:2403.07308 , year=

    Verification-Aided Learning of Neural Network Barrier Functions with Termination Guarantees , author=. arXiv preprint arXiv:2403.07308 , year=

    work page arXiv

  35. [35]

    Towards Deep Learning Models Resistant to Adversarial Attacks

    Towards deep learning models resistant to adversarial attacks , author=. arXiv preprint arXiv:1706.06083 , year=

    work page internal anchor Pith review arXiv

  36. [36]

    Conference on Robot Learning , pages=

    Safe control under input limits with neural control barrier functions , author=. Conference on Robot Learning , pages=. 2023 , organization=

    work page 2023

  37. [37]

    arXiv preprint arXiv:2212.11429 , year=

    Automatically bounding the Taylor remainder series: Tighter bounds and new applications , author=. arXiv preprint arXiv:2212.11429 , year=

    work page arXiv

  38. [38]

    2011 , school=

    Rigorous polynomial approximations and applications , author=. 2011 , school=

    work page 2011

  39. [39]

    1998 , publisher=

    Rigorous analysis of nonlinear motion in particle accelerators , author=. 1998 , publisher=

    work page 1998

  40. [40]

    6th Annual Learning for Dynamics & Control Conference , year=

    Real-Time Safe Control of Neural Network Dynamic Models with Sound Approximation , author=. 6th Annual Learning for Dynamics & Control Conference , year=

    work page

  41. [41]

    Advances in neural information processing systems , volume=

    Efficient neural network robustness certification with general activation functions , author=. Advances in neural information processing systems , volume=

    work page

  42. [42]

    Proceedings of the IEEE/CVF International Conference on Computer Vision , pages=

    Scalable verified training for provably robust image classification , author=. Proceedings of the IEEE/CVF International Conference on Computer Vision , pages=

    work page

  43. [43]

    arXiv preprint arXiv:1906.06316 , year=

    Towards stable and efficient training of verifiably robust neural networks , author=. arXiv preprint arXiv:1906.06316 , year=

    work page arXiv 1906

  44. [44]

    Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition , pages=

    Towards evaluating and training verifiably robust neural networks , author=. Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition , pages=

    work page

  45. [45]

    2019 IEEE 58th Conference on Decision and Control (CDC) , pages=

    Safety-critical control for non-affine nonlinear systems with application on autonomous vehicle , author=. 2019 IEEE 58th Conference on Decision and Control (CDC) , pages=. 2019 , organization=

    work page 2019

  46. [46]

    Proceedings of the AAAI conference on artificial intelligence , volume=

    End-to-end safe reinforcement learning through barrier functions for safety-critical continuous control tasks , author=. Proceedings of the AAAI conference on artificial intelligence , volume=

    work page

  47. [47]

    2024 IEEE International Conference on Robotics and Automation (ICRA) , pages=

    How to train your neural control barrier function: Learning safety filters for complex input-constrained systems , author=. 2024 IEEE International Conference on Robotics and Automation (ICRA) , pages=. 2024 , organization=

    work page 2024

  48. [48]

    Annual Reviews in Control , volume=

    Safety-critical control for autonomous systems: Control barrier functions via reduced-order models , author=. Annual Reviews in Control , volume=. 2024 , publisher=

    work page 2024

  49. [49]

    IEEE Transactions on Automatic Control , year=

    A semi-algebraic framework for verification and synthesis of control barrier functions , author=. IEEE Transactions on Automatic Control , year=

    work page

  50. [50]

    Advances in Neural Information Processing Systems , volume=

    Automatic perturbation analysis for scalable certified robustness and beyond , author=. Advances in Neural Information Processing Systems , volume=

    work page

  51. [51]

    Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation

    Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation , author=. arXiv preprint arXiv:2511.06341 , year=

    work page internal anchor Pith review Pith/arXiv arXiv

  52. [52]

    IEEE Transactions on Control Systems Technology , year=

    Dynamic collision avoidance using velocity obstacle-based control barrier functions , author=. IEEE Transactions on Control Systems Technology , year=

    work page

  53. [53]

    arXiv preprint arXiv:2502.16293 , year=

    Optimization-free Smooth Control Barrier Function for Polygonal Collision Avoidance , author=. arXiv preprint arXiv:2502.16293 , year=

    work page arXiv

  54. [54]

    IEEE Transactions on Intelligent Vehicles , year=

    Safe reinforcement learning for autonomous driving by using disturbance-observer-based control barrier functions , author=. IEEE Transactions on Intelligent Vehicles , year=

    work page

  55. [55]

    IEEE Transactions on Aerospace and Electronic Systems , year=

    Onboard Mission Planning for Autonomous Avoidance of Spacecraft Subject to Various Orbital Threats: An SMT-Based Approach , author=. IEEE Transactions on Aerospace and Electronic Systems , year=

    work page

  56. [56]

    2022 American Control Conference (ACC) , pages=

    Duality-based convex optimization for real-time obstacle avoidance between polytopes with control barrier functions , author=. 2022 American Control Conference (ACC) , pages=. 2022 , organization=

    work page 2022

  57. [57]

    IEEE Robotics and Automation Letters , volume=

    Safety-critical manipulation for collision-free food preparation , author=. IEEE Robotics and Automation Letters , volume=. 2022 , publisher=

    work page 2022

  58. [58]

    IEEE Robotics and Automation Letters , volume=

    Diffocclusion: Differentiable optimization based control barrier functions for occlusion-free visual servoing , author=. IEEE Robotics and Automation Letters , volume=. 2024 , publisher=

    work page 2024

  59. [59]

    International conference on automated deduction , pages=

    dReal: An SMT solver for nonlinear theories over the reals , author=. International conference on automated deduction , pages=. 2013 , organization=

    work page 2013

  60. [60]

    International conference on tools and algorithms for the construction and analysis of systems , pages=

    Automated and formal synthesis of neural barrier certificates for dynamical models , author=. International conference on tools and algorithms for the construction and analysis of systems , pages=. 2021 , organization=

    work page 2021

  61. [61]

    Lyapunov-stable neural control for state and output feedback: A novel formulation for efficient synthesis and verification,

    Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation for Efficient Synthesis and Verification , author=. arXiv preprint arXiv:2404.07956 , year=

    work page arXiv

  62. [62]

    ROBOT , volume =

    Chen, Mou and Ma, Haoxiang and Yong, Kenan and Wu Ying , title =. ROBOT , volume =

    work page

  63. [63]

    ROBOT , volume =

    Fu, Junjie and Lin, Xiaokun and Wen, Guanghui , title =. ROBOT , volume =

    work page