基于半定规划的神经网络验证中的弦稀疏性
Chordal Sparsity for SDP-based Neural Network Verification
AI总结：
本文提出利用弦稀疏性将神经网络验证中的DeepSDP框架的大规模线性矩阵不等式分解为等效的小规模集合，提出Chordal-DeepSDP及其二级分解方法，显著提升了基于半定规划验证的计算效率。
摘要：
神经网络是许多新兴技术的核心，但验证其正确性仍是一项重大挑战。众所周知，网络输出对微小的输入扰动可能非常敏感且脆弱，从而增加了不可预测和不良行为的风险。因此，快速且准确的神经网络验证对其广泛采用至关重要，近年来，针对这一问题已开发出多种方法。本文重点改进基于半定规划（SDP）的神经网络验证技术。此类技术能够表达复杂的几何约束，同时保持凸问题的表述，但在实际应用中，可扩展性仍是一个主要问题。我们的出发点是 Fazlyab 等人提出的 DeepSDP 框架，该框架利用二次约束将验证问题抽象为大规模 SDP。然而，随着网络规模增长，求解该 SDP 很快变得难以处理。我们的关键观察是，通过利用弦稀疏性，可以将 DeepSDP 的主要计算瓶颈——一个大型线性矩阵不等式（LMI）——分解为等效的较小 LMI 集合。我们将这种弦稀疏优化程序称为 Chordal-DeepSDP，并证明其构造与 DeepSDP 具有完全相同的表达能力。此外，我们展示了对 Chordal-DeepSDP 的进一步分析，使我们能够在第二级分解中重写其 LMI 集合，我们将其称为 Chordal-DeepSDP-2，这带来了显著的计算增益。最后，我们在学习到的车摆动力学的真实网络上进行了数值实验，展示了 Chordal-DeepSDP 和 Chordal-DeepSDP-2 相较于 DeepSDP 的计算优势。
英文摘要：
Neural networks are central to many emerging technologies, but verifying their correctness remains a major challenge. It is known that network outputs can be sensitive and fragile to even small input perturbations, thereby increasing the risk of unpredictable and undesirable behavior. Fast and accurate verification of neural networks is therefore critical to their widespread adoption, and in recent years, various methods have been developed as a response to this problem. In this paper, we focus on improving semidefinite programming (SDP) based techniques for neural network verification. Such techniques offer the power of expressing complex geometric constraints while retaining a convex problem formulation, but scalability remains a major issue in practice. Our starting point is the DeepSDP framework proposed by Fazlyab et al., which uses quadratic constraints to abstract the verification problem into a large-scale SDP. However, solving this SDP quickly becomes intractable when the network grows. Our key observation is that by leveraging chordal sparsity, we can decompose the primary computational bottleneck of DeepSDP -- a large linear matrix inequality (LMI) -- into an equivalent collection of smaller LMIs. We call our chordally sparse optimization program Chordal-DeepSDP and prove that its construction is identically expressive as that of DeepSDP. Moreover, we show that additional analysis of Chordal-DeepSDP allows us to further rewrite its collection of LMIs in a second level of decomposition that we call Chordal-DeepSDP-2 -- which results in another significant computational gain. Finally, we provide numerical experiments on real networks of learned cart-pole dynamics, showcasing the computational advantage of Chordal-DeepSDP and Chordal-DeepSDP-2 over DeepSDP.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
