The non-linearity of activation functions presents a major challenge in the verification of neural networks. Due to the computational complexity in the (complete) reasoning over exact activation functions, various studies have been dedicated to efficiently and tightly over-approximating them (sound but often incomplete). One commonly used approach is to employ convex hulls, which reduces the activation functions into linear constraints. However, computing the exact convex hull \emph{per se} is costly, and striking a balance between efficiency and precision in its approximation remains a challenging task.

In this work, we propose a fast and precise over-approximation approach for the convex hull of the ReLU function (referred to as the \emph{ReLU hull}), one of the most used activation functions. Our key insight is to formulate a \emph{convex polyhedron} that “wraps” the ReLU hull, by reusing the linear pieces of the ReLU function as the \emph{lower faces} and constructing \emph{upper faces} that are adjacent to the lower faces. Relying on the edges and vertices of the lower faces, the upper faces can be efficiently constructed, given that an $n$-dimensional (or simply $n$d hereafter) hyperplane can be determined by an $(n-1)$d hyperplane and a point outside of it. This approximation method takes full advantage of the uniqueness of the ReLU hull in sharing linear pieces of the original ReLU function as its lower faces, enabling efficient determination of the forms of the adjacent faces and vertices. Additionally, the adjacency of the newly-generated upper faces to the exact lower faces and the inclusion of the exact vertices contribute to a tight approximation.

We have implemented our method as WraLU, and evaluated its performance in terms of precision, efficiency, constraint complexity, and scalability in approximating ReLU hulls. WraLU outperforms existing advanced methods by generating fewer constraints to achieve tighter approximation in less time. It exhibits versatility by effectively addressing arbitrary input polyhedra and higher-dimensional cases, which are beyond the capabilities of existing methods. We integrate WraLU into PRIMA, a state-of-the-art neural network verifier based on ReLU hull approximation and apply it to verify large-scale ReLU-based neural networks. Our experimental results demonstrate that WraLU achieves a high efficiency without compromising precision. It reduces the number of constraints that need to be solved by the linear programming solver by up to half, while delivering comparable or even superior results compared to the state-of-the-art verifiers.