标题： 动态神经证书的形式化验证 显示英文标题

标题： Formal Verification of Neural Certificates Done Dynamically

摘要： 神经证书已成为网络物理系统控制中的强大工具，提供了正确性的证明。 这些证书，如屏障函数，通常与控制策略一起学习，一旦经过验证，即可作为系统安全的数学证明。 然而，传统形式化验证其定义条件通常由于全面的状态空间探索而面临可扩展性挑战。 为解决这一挑战，我们提出了一种轻量级的运行时监控框架，该框架集成了实时验证，并不需要访问底层控制策略。 我们的监控器在部署期间观察系统，并对一个前瞻区域内的证书进行实时验证，以确保在有限预测时间范围内的安全性。 我们将此框架应用于基于ReLU的控制屏障函数，并在案例研究中展示了其实际有效性。 我们的方法能够在最小开销的情况下及时检测安全违规和错误的证书，为证书的静态验证提供了一种有效但轻量的替代方案。 显示英文摘要

摘要： 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.