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验证器中，与现有边界收紧方法相比获得了有利结果。实验表明，我们的技术在神经网络验证中具有潜力。