新方法SLiR可自动构造激活函数的紧致线性松弛，提升神经网络验证效率。
Shifting-based Optimizable Linear Relaxations for General Activation Functions
- 基于斜率参数化与平移过程，自动生成适用于任意激活函数的线性松弛。
- 在多种实际激活函数上实现更紧的松弛，验证能力比现有方法提升7.8倍。
- 仅需提供利普希茨常数或关键点，适合需要高效验证的高安全场景。
神经网络在安全与安全关键领域应用日益广泛。为提供行为的严格保证，许多验证方法依赖于激活函数的可优化线性松弛。然而，现有技术对每个激活函数都需手动设计松弛，扩展到最新激活函数需大量人力。本文提出通用方法SLiR（基于平移的线性松弛），仅需利普希茨常数或一组关键点即可生成松弛。SLiR通过参数化斜率并利用平移过程确定偏移量，确保输入域上上下界的有效性，在保持正确性的前提下支持高效优化。实验表明，SLiR在多种实用激活函数上均能生成紧致松弛，使可验证性质数量相比当前最优方法提升最多7.8倍。
原文摘要 · Abstract (English)
The use of neural networks (NNs) is rapidly increasing, including in safety- and security-critical domains. To provide formal guarantees about NN behavior, many verification methods rely on optimizable linear relaxations of activation functions. However, existing techniques depend on hand-crafted relaxations for each activation function. Extension to state-of-the-art activation functions therefore requires substantial manual effort. In contrast, our approach SLiR (Shifting-based Linear Relaxations) is broadly applicable, requiring only a Lipschitz constant or a set of critical points. SLiR parameterizes relaxations by their slope and computes the corresponding offset via a shifting procedure that ensures sound upper and lower bounds over the input domain, enabling efficient optimization while maintaining correctness. Our experiments show that SLiR produces tight relaxations across a wide range of practical activation functions and enables verification of up to 7.8x more properties compared to state-of-the-art methods.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。