Why Reusing ReLU's Own Pieces Makes Hull Approximation Cheap

The problem with describing a hull

To verify a ReLU network with an LP-based relaxation, each neuron needs a polytope that contains the ReLU’s output over its input bounds. The tighter that polytope, the more properties the solver can prove; the smaller it is, the less work the solver does. The ideal choice is the exact convex hull, and for ReLU it is a known, simple shape — a triangle in two dimensions, a pyramid in three.

For one scalar ReLU, the familiar triangle is inexpensive. It describes the relationship between an input value and its activation over an interval that crosses zero. This remains true whether the neuron is near the input or deep inside a network.

The harder question appears when we retain more than one pair of values. Several pre-activations may depend on the same input, so their individual ranges do not tell us which values can occur together. One quantity may increase only when another decreases. Replacing that relationship with separate intervals allows combinations that the network cannot produce.

The change is therefore not from a first layer to a second layer. It is from a scalar description to a joint one. We now want constraints over an input region and the activation outputs together, with the relationships in that region still visible.

WraLU starts from the structure this object already has. For each coordinate, ReLU is either the identity or zero. The construction uses these known pieces, together with the input region, to build an enclosing polytope incrementally as output coordinates are added. It exploits specific geometry instead of treating every hull as an unrelated generic object.

This does not make all geometric work disappear, or make every constructed hull exact. It changes where the work is spent: known function structure supplies part of the description, and the remaining construction must still enclose all the relevant behaviour.

What ReLU already gives you

That means the lower faces of the hull do not have to be discovered. They are ReLU’s own pieces. A polytope can be described by its lower faces and its upper faces separately, so the expensive half of the description is free:

• Lower faces — reuse the linear pieces of ReLU directly
• Upper faces — construct faces adjacent to those lower faces

What remains is the second half, and it is construction rather than search. An n-dimensional hyperplane is determined by an (n-1)-dimensional hyperplane plus a point outside it, so each upper face can be built from the edge structure of the lower face it caps, using the vertices that edge already exposes. This avoids the full generic reconstruction of a convex hull output — not because all geometric work disappears, but because the function already supplies part of the description and the remaining construction only needs to enclose the relevant behaviour.

This is the whole idea behind WraLU: rather than describing the hull from outside, start from the pieces ReLU already has and add the minimum needed to close it.

The construction assumes what ReLU is — piecewise linear with two regions, one of them flat. That is the whole basis for the free lower faces, so it is also the boundary of the approach: S-shaped functions have a smooth region count and no flat piece to reuse, which makes them a different problem with different costs. That is what WraAct addresses, and treating the two as the same technique under different activation names is how a claim about one ends up with an implementation of the other.

What that buys

Wrapping the polytope this way, on the benchmarks in the paper:

• 10x to 10^6x faster construction than the compared baselines
• Up to 50% fewer constraints, while maintaining or improving precision
• Works on arbitrary input polytopes, not just boxes, and in higher dimensions

The constraint count is the part worth pausing on, but not for the reason the number invites. Fewer constraints is not only a smaller LP — it is less for the solver to chew, and for a fixed number of neurons it is one of the inputs to whether a run finishes at all. It is not the only input. Two relaxations of the same size can take very different times, because solver cost depends on the structure of the constraint matrix and not only on its dimensions: how much of it is shared between neurons, how dense each row is, how large the coefficients get. A description built out of ReLU’s own pieces tends to reuse rather than duplicate, which is the likelier reason the count drops without the added constraints being redundant copies of one another. So the honest reading of a constraint reduction is that it removed work, not that it settled the question. A richer constraint system may cost more per solve while eliminating later search. Whether it is worthwhile depends on the complete verification process, not on the constraint count alone.

Why it makes verification possible at all

A sound but incomplete method can still prove many properties. It returns UNKNOWN when it cannot establish a conclusion on an instance, not because it is forbidden from returning SAFE. Better approximation aims to make more useful conclusions available without excluding real behaviours.

Further Reading

• Ma, Li, Bai. ReLU Hull Approximation. Proceedings of the ACM on Programming Languages (POPL’24). doi:10.1145/3632917
• Singh, Ganvir, Puschel, Vechev. Beyond the Single Neuron Convex Barrier for Neural Network Certification. NeurIPS 2019. The paper that names the limit of bounding one ReLU at a time and moves past it by approximating several jointly, which is the other half of the space this one works in.
• The WraLU project page for the tool, the repository, and the full result tables.