一句话：提出 WraAct，利用双线性分段函数简化局部几何，高效构造通用激活函数的紧凸包过近似。
神经网络形式化验证受激活函数非线性制约；精确凸包计算昂贵甚至不可行，已有方法多针对 ReLU、Sigmoid 等特定函数。本文提出 WraAct，通过线性约束平滑目标函数波动，并用双线性分段（DLP）函数简化局部几何，将通用激活函数凸包过近似归约为可高效处理的 DLP 过近似。与 SOTA 方法 SBLM+PDDM 相比，WraAct 在 Sigmoid、Tanh、MaxPool 上平均快 400 倍、精度高 150 倍，约束数减少约 50%，10 秒可处理 8 个输入维度；集成到验证器后，单神经元验证数从不足 10 提升至 40 以上，较 PRIMA 多验证最多 20 个样本，并可在 1 分钟内验证 22k 神经元 ResNet。
The wide adoption of deep learning in safety-critical domains has driven the need for formally verifying the robustness of neural networks. A critical challenge in this endeavor lies in addressing the inherent non-linearity of activation functions. The convex hull of the activation function has emerged as a promising solution, as it effectively tightens variable ranges and provides multi-neuron constraints, which together enhance verification precision. Given that constructing exact convex hulls is computationally expensive and even infeasible in most cases, existing research has focused on over-approximating them. Several ad-hoc methods have been devised for specific functions such as ReLU and Sigmoid. Nonetheless, there remains a substantial gap in developing broadly applicable approaches for general activation functions. In this work, we propose WraAct , an approach to efficiently constructing tight over-approximations for activation function hulls. Its core idea is to introduce linear constraints to smooth out the fluctuations in the target function, by leveraging double-linear-piece (DLP) functions to simplify the local geometry. In this way, the problem is reduced to over-approximating DLP functions, which can be efficiently handled. We evaluate WraAct against SBLM+PDDM, the state-of-the-art (SOTA) multi-neuron over-approximation method based on decomposing functions into segments. WraAct outperforms it on commonly-used functions like Sigmoid, Tanh, and MaxPool, offering superior efficiency (average 400X faster) and precision (average 150X) while constructing fewer constraints (average 50% reduction). It can complete the computation of up to 8 input dimensions in 10 seconds. We also integrate WraAct into a neural network verifier to evaluate its capability in verification tasks. On 100 benchmark samples, it significantly enhances the single-neuron verification from under 10 to over 40, and outperforms the multi-neuron verifier PRIMA with up to additional 20 verified samples. On large networks like ResNets with 22k neurons, it can complete the verification of one sample within one minute.
@article{paperbot2888,
title = {Convex Hull Approximation for Activation Functions},
author = {Zhongkui Ma and Zihan Wang and Guangdong Bai},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763086}
}