Current approaches to neural network verification focus on specifications that target small regions around known input data points, such as local robustness. Thus, using these approaches, we can not obtain guarantees for inputs that are not close to known inputs. Yet, it is highly likely that a neural network will encounter such truly unseen inputs during its application. We study global specifications that - when satisfied - provide guarantees for all potential inputs. We introduce a hyperproperty formalism that allows for expressing global specifications such as monotonicity, Lipschitz continuity, global robustness, and dependency fairness. Our formalism enables verifying global specifications using existing neural network verification approaches by leveraging capabilities for verifying general computational graphs. Thereby, we extend the scope of guarantees that can be provided using existing methods. Recent success in verifying specific global specifications shows that attaining strong guarantees for all potential data points is feasible.

翻译：当前神经网络验证方法主要针对已知输入数据点附近的小范围规约（如局部鲁棒性）进行验证。因此，采用这些方法无法为远离已知输入的输入提供保证。然而在应用过程中，神经网络极有可能遭遇此类真正未见过的输入。本文研究全局规约——当满足此类规约时，可为所有潜在输入提供保证。我们引入超性质形式化体系，可表达单调性、Lipschitz连续性、全局鲁棒性和依赖公平性等全局规约。该形式化体系通过利用验证通用计算图的能力，使现有神经网络验证方法能够验证全局规约。由此，我们扩展了现有方法可提供的保证范围。特定全局规约验证的最新成功表明，为所有潜在数据点提供强保证是可行的。