Skip to main content
ReLUConvex HullVerificationPOPL

WraLU: Fast and Precise ReLU Hull Approximation

A fast and precise approach to over-approximating the convex hull of the ReLU function, reporting 10x-10^6x runtime improvements and up to 50% fewer constraints in the evaluated benchmarks.

Overview

WraLU is a fast and precise approach to over-approximating the convex hull of the ReLU function (referred to as the ReLU hull), one of the most used activation functions. Published at POPL’24 (the 51st ACM SIGPLAN Symposium on Principles of Programming Languages).

The Verification Problem

Neural network verification requires encoding activation functions as linear constraints. For ReLU networks, the convex hull of the ReLU function over a bounded input region provides the tightest possible linear approximation.

The challenge: Computing the exact convex hull is computationally expensive, and existing over-approximations are either too loose (box bounds) or too slow to construct (general-purpose polytope methods).

Key Insight

Our key insight is to formulate a convex polytope that “wraps” the ReLU hull, by reusing the linear pieces of the ReLU function as the lower faces and constructing upper faces that are adjacent to the lower faces.

The upper faces can be efficiently constructed based on the edges and vertices of the lower faces, given that an n-dimensional hyperplane can be determined by an (n-1)-dimensional hyperplane and a point outside of it.

How It Works

  1. Lower Faces: Reuse the linear pieces of the ReLU function directly
  2. Upper Face Construction: Build upper faces adjacent to lower faces using edge and vertex information
  3. Wrapping Polytope: The resulting convex polytope tightly wraps the ReLU hull
  4. Integration: Feed the constraints to LP solvers for neural network verification

Performance Highlights

  • 10x to 10^6x runtime improvement over the compared baselines in the reported evaluation
  • Up to 50% fewer constraints while maintaining or improving precision
  • Handles arbitrary input polytopes and higher-dimensional cases
  • Used in verification experiments on CNNs and ResNet-style models with tens of thousands of neurons
  • Designed for LP-based neural network verification pipelines that benefit from tighter ReLU relaxations

Comparison with Other Methods

MethodTightnessSpeedConstraints
Box boundsVery looseFastest4
Triangle boundsLooseFast3
General polytopeTightSlowVariable
WraLUTightFastUp to 50% fewer

Verification Impact

On the paper’s benchmark:

  • Enhances single-neuron verification from under 10 to over 40 verified samples
  • Outperforms multi-neuron verifier PRIMA with up to 20 additional verified samples
  • WraAct: Extension to general activation functions (Sigmoid, Tanh, MaxPool) — OOPSLA’25
  • wraact (library): Unified Python library for hull approximation

Citation

@article{ma2024relu,
  title={ReLU Hull Approximation},
  author={Ma, Zhongkui and Li, Jiaying and Bai, Guangdong},
  journal={Proceedings of the ACM on Programming Languages},
  volume={8},
  number={POPL},
  pages={2260--2287},
  year={2024},
  publisher={ACM New York, NY, USA}
}

Lessons Learned

1. Structure matters: ReLU’s piecewise linear structure allows exact polytope representation. Exploiting this structure is key to both tightness and speed.

2. Tightness enables verification: Loose approximations make verification impossible. Tighter bounds mean faster solver convergence and more verified properties.

3. Practical impact: Sub-millisecond polytope generation enables verification of 1000+ neuron networks, making formal verification practical for real-world models.

Conclusion

WraLU demonstrates that tight, fast activation approximation is achievable by exploiting the geometric structure of the ReLU function. The wrapping polytope approach balances soundness, tightness, and computational efficiency — a foundation for scaling neural network verification to larger models.

Sound. Tight. Fast. That’s what WraLU delivers.

← Back to Blogs