Formal Verification of Neural Certificates Done Dynamically
This provides an incremental improvement for cyber-physical systems control by offering a more scalable alternative to static verification of neural certificates.
The paper tackles the scalability challenge of formally verifying neural certificates in cyber-physical systems by proposing a lightweight runtime monitoring framework that performs on-the-fly verification over a lookahead region, demonstrating practical effectiveness in a case study with minimal overhead.
Neural certificates have emerged as a powerful tool in cyber-physical systems control, providing witnesses of correctness. These certificates, such as barrier functions, often learned alongside control policies, once verified, serve as mathematical proofs of system safety. However, traditional formal verification of their defining conditions typically faces scalability challenges due to exhaustive state-space exploration. To address this challenge, we propose a lightweight runtime monitoring framework that integrates real-time verification and does not require access to the underlying control policy. Our monitor observes the system during deployment and performs on-the-fly verification of the certificate over a lookahead region to ensure safety within a finite prediction horizon. We instantiate this framework for ReLU-based control barrier functions and demonstrate its practical effectiveness in a case study. Our approach enables timely detection of safety violations and incorrect certificates with minimal overhead, providing an effective but lightweight alternative to the static verification of the certificates.