神经网络可达性分析的二次特性

二次约束 (QCs) 广泛用于特征非线性和不确定性，但通用的解析特性在有界域上可能保守。本文发展了一个框架，用于构造标量关系在二维实平面上的经验证二次特性。候选二次不等式通过求解针对关系样本和外部样本点的凸二次规划问题来局部生成。然后通过 sum-of-squares 证书在精确半代数描述下（或对于非多项式关系，在松弛多项式描述下）对其进行全局验证。 resulting 经验证约束定义了标量关系在所考虑域上的 sound overapproximation。这些约束直接兼容基于 QCs 和 pointwise integral quadratic constraints (IQCs) 的现有分析框架，用于静态非线性和不确定性，还可以嵌入 QC 基于的半正定规划，用于 feedforward 神经网络的可达性和安全性分析。对于 smooth 激活函数如 $\tanh$，该方法产生与通用 sector- 或 slope-based 描述相比的 domain-dependent 二次特性。对于 ReLU 网络，我们提供方法利用神经元之间的依赖性和更紧致的局部界限来降低 QC 基于可达性分析的保守性。数值示例展示了对于 smooth 激活函数改进的可达性结果、对于 ReLU 网络降低保守性，以及通过涉及饱和的例子超出神经网络的适用性。