The increasing integration of deep neural networks in critical systems has spawned a theoretical and practical interest in formally guaranteeing safety properties about their behavior. To achieve this, contemporary verification algorithms rely on computing linear relaxations for a network's non-linear activation functions. Existing approaches for linear relaxations typically fall into one of two categories: single-neuron relaxation, in which each activation neuron is bounded in terms of its sources; and multi-neuron relaxation, in which linear bounds involving multiple activation neurons and their sources are calculated. However, existing methods might fail to balance tightness and scalability, as single-neuron bounds might not derive sufficiently tight bounds necessary for verification to complete, whereas generating multi-neuron relaxation for all activation neurons is computationally expensive. In this paper, we present a middle-ground approach featuring partial multi-neuron relaxation, in which we generate multi-neuron bounds for only a small, heuristically selected subset of neurons. To achieve this, we build upon existing branching heuristics for selecting neurons and for optimizing bounding hyper-planes for multi-neuron bounds. We integrated our proposed method within the Marabou verifier, and obtained favorable results in comparison to existing bound tightening methods. Our experiments showcase the potential of our technique for neural network verification.

翻译：深度神经网络在关键系统中的日益集成，引发了对其行为进行形式化安全保障的理论与实践兴趣。为此，当代验证算法依赖于对网络非线性激活函数计算线性松弛。现有的线性松弛方法通常分为两类：单神经元松弛，其中每个激活神经元以其输入为界进行约束；以及多神经元松弛，其中计算涉及多个激活神经元及其输入的线性界限。然而，现有方法可能难以平衡严格性与可扩展性，因为单神经元界限可能无法推导出验证所需足够严格的边界，而为所有激活神经元生成多神经元松弛在计算上成本高昂。本文提出了一种折中方案——部分多神经元松弛，该方案仅对通过启发式选择的一小部分神经元生成多神经元界限。为此，我们基于现有的分支启发式方法选择神经元，并优化多神经元界限的超平面。我们将所提出的方法集成到Marabou验证器中，并与现有的边界收紧方法相比取得了显著效果。我们的实验展示了该技术在神经网络验证中的潜力。