28 Mar 2024 | Manan Tayal¹, Hongchao Zhang², Pushpak Jagtap¹, Andrew Clark², Shishir Kolathaya¹
This paper presents an algorithm for synthesizing formally verified continuous-time neural Control Barrier Functions (CBFs) in stochastic environments in a single step. The proposed method constructs a sample-based learning framework for Stochastic Neural CBFs (SNCBFs) to ensure efficacy across the entire state space with only a finite number of data points. By enforcing Lipschitz bounds on the neural network, its Jacobian, and Hessian terms, the methodology eliminates the need for post hoc verification. The approach is demonstrated through case studies on the inverted pendulum system and obstacle avoidance in autonomous driving, showcasing larger safe regions compared to baseline methods. The algorithm trains a neural network to synthesize SNCBFs that satisfy safety constraints, ensuring the system remains safe under stochastic conditions. The method guarantees safety by leveraging Lipschitz bounds and formal verification, making it suitable for real-time safety-critical control applications. The effectiveness of the proposed approach is validated through simulations, demonstrating its ability to handle continuous-time stochastic systems with formal guarantees.This paper presents an algorithm for synthesizing formally verified continuous-time neural Control Barrier Functions (CBFs) in stochastic environments in a single step. The proposed method constructs a sample-based learning framework for Stochastic Neural CBFs (SNCBFs) to ensure efficacy across the entire state space with only a finite number of data points. By enforcing Lipschitz bounds on the neural network, its Jacobian, and Hessian terms, the methodology eliminates the need for post hoc verification. The approach is demonstrated through case studies on the inverted pendulum system and obstacle avoidance in autonomous driving, showcasing larger safe regions compared to baseline methods. The algorithm trains a neural network to synthesize SNCBFs that satisfy safety constraints, ensuring the system remains safe under stochastic conditions. The method guarantees safety by leveraging Lipschitz bounds and formal verification, making it suitable for real-time safety-critical control applications. The effectiveness of the proposed approach is validated through simulations, demonstrating its ability to handle continuous-time stochastic systems with formal guarantees.