用集合损失函数一次性训练出可证明安全的神经屏障函数。
Set-Based Training of Neural Barrier Certificates for Safety Verification of Dynamical Systems
- 设计集合损失函数，将验证嵌入训练过程。
- 零损失即证明函数有效，无需迭代验证。
- 适合需要形式化安全保证的复杂系统设计者。
屏障证书是定义在动力系统状态空间上的标量函数，用于分离所有不安全状态与所有可达状态。其存在性可形式化验证系统的安全性。现有方法通过迭代训练神经网络合成屏障证书：每次训练后进行形式化验证，成功则找到证书。本文提出一种基于集合的训练方法，通过集合损失函数将验证过程紧密集成到训练中，该损失函数严格编码了屏障证书的所有性质。当损失值为零时，即可形式化证明证书的有效性，从而将原本迭代的训练与验证过程合并为单一训练流程。实验表明，该方法在系统维度增加时仍具有良好扩展性，并能自然处理复杂的非线性动态。
原文摘要 · Abstract (English)
Barrier certificates are scalar functions over the state space of dynamical systems that separate all unsafe states from all reachable states. The existence of a barrier certificate formally verifies the safety of the dynamical system. Recent approaches synthesize barrier certificates by iteratively training a neural network. In each iteration, the candidate is formally verified - if successful, the barrier certificate is found. Instead, we propose a set-based training approach that tightly integrates verification into training via a set-based loss function that soundly encodes all barrier certificate properties. A loss of zero formally proves the validity of the barrier certificate, collapsing the iterative training and verification into a single training procedure. Our experiments demonstrate that our set-based training approach scales well with the system dimension and naturally handles complex nonlinear dynamics.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。