发表机构
University of Colorado Boulder（科罗拉多大学博尔德分校）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出一种数据驱动的组合式安全验证方法，利用单调性构建局部区间障碍证书并组合验证互联单调系统，无需显式模型，实验证明其有效且可扩展。
AI 中文摘要
本文提出了一种样本高效的组合式方法，用于对互联单调系统进行形式化安全验证，且无需局部子系统的显式模型。现有的数据驱动方法要么缺乏形式化安全保证，要么依赖基于Lipschitz的稠密状态空间离散化来提供此类保证，这导致了显著的计算开销并限制了可扩展性。相比之下，我们利用局部子系统的单调性，仅通过对每个子系统进行边界评估，以分散方式构造易于处理的局部区间障碍证书，并结合一个全局条件来保证整个互联系统的安全性。在局部层面，我们的框架利用单调神经网络，从由局部状态和内部输入空间划分所诱导的边界样本中学习区间障碍证书。在全局层面，它利用互联结构组合这些局部神经区间障碍证书，以验证整体系统的安全性。此外，在适当的结构假设下，我们将全局安全条件重新表述为可扩展的形式，该形式可直接纳入神经网络损失函数中。这使得在局部训练期间能够强制执行整体系统安全性。实验结果表明了所提方法的有效性和可扩展性。
英文摘要
This paper introduces a sample-efficient compositional method for formal safety verification of interconnected monotone systems without requiring explicit models of the local subsystems. Existing data-driven approaches either lack formal safety guarantees or rely on dense Lipschitz-based discretizations of the state space to provide such guarantees, which leads to significant computational overhead and limits scalability. In contrast, we leverage the monotonicity of local subsystems to construct tractable local interval-barrier certificates using only boundary evaluations of each subsystem in a decentralized manner, together with a global condition that guarantees the safety of the overall interconnected system. At the local level, our framework learns interval-barrier certificates using monotone neural networks from boundary samples induced by partitions of the local state and internal-input spaces. At the global level, it composes these local neural interval-barrier certificates using the interconnection structure to certify the safety of the overall system. Furthermore, under appropriate structural assumptions, we reformulate the global safety condition into a scalable form that can be directly incorporated into the neural network loss. This enables the enforcement of overall system safety during local training. The experimental results demonstrate the effectiveness and scalability of the proposed method.
