用更紧的约束提升神经网络验证效率，兼顾大模型与精度。
SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
- 基于SDP思想设计新线性约束，显式建模神经元间耦合关系。
- 在6.5万神经元、247万参数的大模型上逼近昂贵SDP方法的紧度。
- 仅增每层一个参数，可无缝集成到现有验证框架中。
基于线性边界传播的神经网络验证器能高效处理大规模模型，但在神经元耦合关键时表现松散；而半定规划（SDP）验证器虽能自然捕捉神经元间耦合，却因立方复杂度仅适用于小模型。本文提出SDP-CROWN，一种融合SDP紧度与边界传播可扩展性的新型混合验证框架。核心是一种基于SDP原理推导的新线性边界，显式建模以ℓ₂-范数为基础的神经元间耦合，每层仅增加一个额外参数。该边界可无缝集成至任意线性边界传播流程，保持原有可扩展性的同时显著提升紧度。理论上，该神经元间边界相比传统单神经元边界可最多紧约√n倍。实践中，将其嵌入最先进的α-CROWN验证器后，在包含高达6.5万神经元和247万参数的大模型上实现了显著提升的验证性能，其紧度接近昂贵的基于SDP的方法。
原文摘要 · Abstract (English)
Neural network verifiers based on linear bound propagation scale impressively to massive models but can be surprisingly loose when neuron coupling is crucial. Conversely, semidefinite programming (SDP) verifiers capture inter-neuron coupling naturally, but their cubic complexity restricts them to only small models. In this paper, we propose SDP-CROWN, a novel hybrid verification framework that combines the tightness of SDP relaxations with the scalability of bound-propagation verifiers. At the core of SDP-CROWN is a new linear bound, derived via SDP principles, that explicitly captures $\ell_{2}$-norm-based inter-neuron coupling while adding only one extra parameter per layer. This bound can be integrated seamlessly into any linear bound-propagation pipeline, preserving the inherent scalability of such methods yet significantly improving tightness. In theory, we prove that our inter-neuron bound can be up to a factor of $\sqrt{n}$ tighter than traditional per-neuron bounds. In practice, when incorporated into the state-of-the-art $α$-CROWN verifier, we observe markedly improved verification performance on large models with up to 65 thousand neurons and 2.47 million parameters, achieving tightness that approaches that of costly SDP-based methods.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。