Safe AI Control

Control barrier functions (CBFs) define conditions under which a controller keeps a dynamical system inside a specified safe set. Neural CBFs can represent complex safety geometries, but a learned candidate is useful only when its safety conditions can be checked.

Exact verification

For rectified linear unit (ReLU) neural CBFs, smooth-function conditions do not apply at nondifferentiable boundaries. Ignoring those boundaries can accept a candidate that does not establish safety. Our NeurIPS 2023 work derived necessary and sufficient conditions for the studied class and an exact verification method that checks the activation regions intersecting the barrier boundary.

Synthesis with verification

SEEV integrates synthesis with exact verification. Training shapes the activation regions near the safety boundary so that the final verification problem is smaller, while counterexamples from verification guide subsequent synthesis.

Stochastic systems

This line also addresses stochastic dynamics. Our CDC 2024 work learns a formally verified CBF in a stochastic environment. Stochastic Neural Control Barrier Functions, to appear in IEEE Transactions on Automatic Control in March 2027, develops probabilistic forward-invariance guarantees under its stated stochastic-system assumptions.

Papers and code

• Exact Verification of ReLU Neural Control Barrier Functions · code
• SEEV: Synthesis with Efficient Exact Verification for ReLU Neural Barrier Functions · code
• Stochastic Neural Control Barrier Functions · code