What Makes a Hull Approximation Useful

The obvious way to judge a hull approximation is to ask how close it is. That question has a good answer and a bad question hidden inside it, and the bad one is the one that decides whether a verifier is useful.

The good question is about geometry: how much of the gap between the approximation and the true convex hull is left over. The bad question assumes that closing it is always worth doing. It is not, for two independent reasons — and both of them are about what the approximation keeps rather than how tight it is.

This note is about that, using WraLU and WraAct as the worked examples. The WraLU note explains the construction and the WraAct note covers the soundness contract; what sits between them is the part that generalises to any relaxation.

A tight description of one piece says nothing about their combination

Bound propagation works neuron by neuron. For each activation you compute a region that contains every value that activation can take, given the input region. Every neuron gets one, and the network’s behaviour is then bounded through them.

Here is the problem, and it is not a subtlety — it is the reason the whole area exists. Each of those per-neuron regions is correct, and their composition can still be far too loose, because a set of individually valid statements about separate variables does not determine which combinations are actually reachable. The variables are not independent: they are outputs of the same input.

The natural example is a pair of ReLUs whose pre-activations are correlated. If one is large positive the other cannot be independently large negative, and a relaxation that treats them separately permits a combination that no input produces. Nothing is wrong with either per-neuron bound. What is missing is the relationship between them.

So there are two different things to preserve. What each neuron is allowed to do, which is what per-neuron bounds describe. And which combinations of those behaviours can occur together, which is a strictly larger amount of information and the part a loose relaxation throws away.

This gives the useful way to talk about tightness. A relaxation can be locally exact on every neuron and still describe a set of joint behaviours that no input reaches. The soundness and completeness chapter works through what that costs: the method finds a point that looks reachable and is not, and reports UNKNOWN on a property that is actually true. The precision was not the problem. The missing relation was.

More information is available, and it is not free

If relations are what a relaxation is short of, the obvious response is to add them, and there are more ways to do that than a practitioner has time to implement. Some of them are worth understanding on their own terms, because each fails in a way that is instructive.

The exact hull. For ReLU over an interval, the convex hull is exactly describable, so an exact over-approximation exists and is cheap. That case is unusually friendly, and it is worth naming why: the function is piecewise linear, so the hull is a polytope with finitely many facets and can be written down. For a smooth activation it is not, and computing it is a hard geometric problem that is intractable in many cases. So the interesting case is not ReLU, where the tightest available answer is also the cheap one, but the S-shaped and saturating functions where those two come apart.

Worth being precise about what makes a description the hull, because it is easy to get this wrong in the direction of over-confidence. A polytope can touch the function at every one of its facets and still strictly contain it, since containment is an interior property: the curve can run through the middle without meeting a face at all. Take the unit circle and circumscribe a square — every facet is tangent, the square is convex, it contains the circle, and it is still not the convex hull, which is the disc. So the condition that characterises the hull is not tangency, and not convexity-plus-containment either, since the square satisfies both. It is minimality: the smallest convex set containing the graph. A relaxation that contains the graph and is convex is a valid outer approximation, which is a weaker thing than being the hull, and every construction below is aiming at the weaker thing on purpose.

A hull of sampled points. Compute the convex hull of a fine grid of points on the graph. This is tighter than a coarse construction and it is not sound: the graph bulges between the samples, and the sampled polytope does not contain those bulges. This is worth dwelling on because sampling is exactly the kind of method that looks rigorous in a plot and fails in a way no plot reveals. Validating on a sample does not discharge the problem either — the sample is the wrong kind of object, and the WraAct note works through why.

Every facet you can afford. Once you have a valid outer approximation you may keep adding facets to shrink the gap; each is sound if it lies above the graph, and each costs a constraint. The stopping point here is a budget decision dressed up as a geometric one.

A more expensive bound can save search

What makes the choice hard is that the price of adding information is not well described by counting constraints. Three quantities move, and only one of them is the constraint count.

Tightness is what a facet sitting adjacent to the true hull buys. Constraint count is what it costs at every LP in the search tree, which compounds with depth rather than adding linearly. Construction time is paid once, before the search begins, and whether that matters depends entirely on whether the tool runs offline or interactively.

A design that ignores one of the three has not avoided the trade — it has moved it somewhere less visible. An approximation that is tighter and cheap to build but triples the constraints has not improved the verifier; it has moved the cost into the loop that matters more, because each constraint is paid again at every node.

And the direction of the effect is not fixed. A richer representation can also reduce downstream work, if the extra information lets the search prune whole regions earlier. “More information is more expensive” is true of the construction and false of the run, and treating it as true of both is why it is worth separating.

Two constructions that spend accuracy on purpose

The pattern appears twice here, and it is worth naming rather than illustrating twice.

WraLU reuses ReLU’s own linear pieces as the lower faces of the polytope and constructs upper faces adjacent to them, so the construction becomes bookkeeping over the function’s existing edges and vertices rather than a geometry search. On the paper’s benchmarks it reduced constraint count by up to half at comparable or better precision, and moved single-neuron verification from under ten verified samples to over forty. The WraLU note has the construction, and the scope condition that comes with it.

WraAct takes the S-shaped case directly, replacing the graph on $[l,u]$ with a double-linear-piece function: two affine pieces combined by a maximum or a minimum. “A lower line and an upper line” is a different object — the pieces meet at a kink, and which side of the target each one sits on follows from the max/min rather than from the pieces being ordered. Reported against SBLM+PDDM on Sigmoid, Tanh and MaxPool, it is more precise and much faster to construct, with about half the constraints. The WraAct note works through the definition, the tangent that licenses each piece, and what the library’s containment contract has to establish.

The shared move is not that tightness is bad. Each takes a construction whose cost is predictable and whose validity is checkable over a whole interval, and spends accuracy to get it. The accuracy given up is chosen rather than incidental, which is what makes it a design decision rather than a limitation — and it is also why the useful question is what an approximation keeps rather than how close it is.

The three questions

Whether a relaxation is worth using is not a property of the polytope. It is a property of the polytope composed with the solver, the network and the budget — and the three questions that decide it are answerable separately.

1. Is it sound? Every emitted constraint is justified over the whole domain rather than at sampled points. This one is not negotiable, and it is the only one of the three that can make a verifier unsound rather than merely unhelpful.
2. Does it preserve the relations that decide this property? A relaxation can be locally exact on every neuron and describe joint behaviours no input reaches.
3. Does the constructed system finish?

A construction can answer 1 and 3 while failing 2, and be right. One answering all three can be too expensive to build, or to finish inside its budget — practicality, not soundness. What is not available is answering 3 while ignoring 1: that is how unsound verifiers ship.

Further Reading

• Ma, Li, Bai. ReLU Hull Approximation (POPL’24) — reusing the function’s own linear pieces as lower faces.
• Ma, Wang, Bai. Convex Hull Approximation for Activation Functions (OOPSLA’25) — the double-linear-piece framework for S-shaped and saturating functions.
• Why Reusing ReLU’s Own Pieces Makes Hull Approximation Cheap — the WraLU construction in detail.
• Activation Hulls: What Makes an Approximation Sound? — the containment contract, and what validation actually has to establish.
• Soundness, Completeness, and UNKNOWN — why a tighter bound that cannot be computed in budget buys nothing.