On Choice of Loss Functions for Neural Control Barrier Certificates
摘要
The design of controllers with correctness guarantees is a primary concern for safety-critical control systems. A Control Barrier Certificate (CBC) is a real-valued function over the state space of the system that provides an inductive proof of the existence of a safe controller. Recently, neural networks have been successfully deployed for data-driven learning of control barrier certificates. These approaches encode the conditions for the existence of a CBC using a rectified linear unit ( \(\textsf{ReLU} \) ) loss function. The resulting encoding, while sound, tends to be conservative, which results in slower training and limits scalability to large, complex systems. Can altering the loss function alleviate some of the problems associated with \(\textsf{ReLU} \) loss and lead to faster learning? This paper proposes a novel encoding with a Mean Squared Error loss function, which allows for more scalable and efficient training, while addressing some of the theoretical limitations of previous methods. We also encode one of the main conditions of CBC in a non-conservative way, enabling us to derive CBC where existing methods have failed. The proposed approach derives a validity condition based on Lipschitz continuity to formally characterize safety guarantees, eliminating the need for a post-hoc verification. The effectiveness of the proposed loss functions is demonstrated through six case studies curated from the existing literature. Our results provide a strong argument for exploring alternative loss function choices as a novel approach to optimizing the design of CBCs.