Activation Hulls: What Makes an Approximation Sound?

An activation-hull routine is useful to a verifier only if its constraints contain every behaviour they are supposed to represent. A neat polytope, a successful conversion from vertices to inequalities, and thousands of passing samples do not establish that containment by themselves.

This note separates three objects that are easy to confuse: the graph of an activation, its convex hull, and a polyhedral outer approximation.

Name the set before choosing its representation

For an input region $X$ and an activation map $\Phi$, define its graph over that region:

$$\mathcal G_X=\{(x,\Phi(x)):x\in X\}.$$

A sound outer approximation $P$ satisfies $\mathcal G_X\subseteq P$. If $P$ is convex, it also contains $\operatorname{conv}(\mathcal G_X)$. The task is not necessarily to construct that hull exactly; it is to obtain useful valid constraints at an acceptable cost.

For a bounded polytope, H-representation describes inequalities and V-representation describes a finite vertex set. Converting between representations preserves the represented polytope. It does not establish that this polytope contains the activation graph.

Why sampling points is not a soundness argument

Let $S$ be finitely many sampled points of $\mathcal G_X$. Then

$$S\subseteq\mathcal G_X \quad\Longrightarrow\quad \operatorname{conv}(S)\subseteq\operatorname{conv}(\mathcal G_X).$$

That inclusion is the opposite of the one an outer approximation needs. Equality can hold in special cases when all necessary extreme structure is captured, but it does not follow from using a dense grid.

A two-point counterexample is enough. Sample $q(x)=x^2$ at $x=-1$ and $x=1$. Both sampled graph points have height 1, so their convex hull is the horizontal segment $y=1$. The valid graph point $(0,0)$ is outside it. Converting that segment to halfspaces cannot recover the missing point.

Sampling remains useful for finding bugs or inspecting shapes. To turn it into a certified enclosure, an additional valid construction is needed, such as analytically justified envelopes or a proved remainder bound. This observation concerns the construction argument rather than the implementation: it is not a claim that the maintained library emits sampled hulls as certified constraints.

What a validated construction looks like

Sampling fails as a soundness argument because the points it uses are the wrong kind of object. A construction succeeds when every constraint it emits is justified over the whole domain, and the justification is a property of the function rather than of how many samples happened to be drawn.

Why the S-shaped case is harder. Two sources of complexity make S-shaped activations a different problem from ReLU. Joint dependency means we cannot consider isolated scalar triangles — the valid combinations of coordinates matter, so per-neuron exactness does not carry over to their composition. Function curvature means there are no flat regions to reuse, so each constraint has to be licensed analytically rather than inherited from the function’s own pieces. These two concerns affect every activation differently: ReLU’s joint dependency is the reason WraLU’s construction works, and S-shaped curvature is the reason WraAct needs a different approach.

For a S-shaped function on $[l,u]$, the DLP construction in WraAct replaces the graph with a double-linear-piece function: two affine pieces, combined by a maximum or a minimum. Worth being precise about that, because “a lower line and an upper line” is a different object. The max or min chooses the piecewise shape; it does not by itself prove that the result is above or below the target. The required enclosure inequality must still hold throughout $[l,u]$, and the usual way to license each piece is an analytically justified tangent. The tangent of $\sigma$ at $x_0$ is

$$y=\sigma(x_0)+\sigma'(x_0)(x-x_0),\qquad \sigma'(x)=\sigma(x)\bigl(1-\sigma(x)\bigr).$$

A point $x_0$ gives a valid upper bound exactly when $\sigma(x)\leq \sigma(x_0)+\sigma'(x_0)(x-x_0)$ holds for every $x\in[l,u]$, and the curvature of a S-shaped function is what lets an endpoint choice satisfy that. Two such pieces bound the graph in the plane, and the description extends to higher input dimensions because each constraint is a statement about the function rather than about a sampled point.

This is the contrast the previous section drew, stated positively. The graph hull is the right object to aim at; the question is what licenses each halfspace. An analytically justified tangent licenses itself, a ReLU’s own linear pieces license themselves exactly, and a grid of samples licenses nothing beyond the convex hull of the samples — which is why a sampled hull can be an inner approximation of the true hull and an outer approximation of nothing at all.

Where incremental construction helps, and what it does not

The full hull of an $n$-input, $m$-output activation lives in $n+m$ dimensions, and construction cost grows quickly with dimension. A verification query rarely needs all $m$ outputs at once: a property about one logit needs constraints for that logit.

The WithOneY idea is to extend the region one output at a time — solve in $n+1$ dimensions, then $n+2$, and stop once the query’s outputs are covered. What that buys is dimension and constraint count, which is a real saving.

What it does not buy is a guarantee. Each incremental step is a hull over a set of points, so the soundness of a step is whatever the underlying construction for that activation is; if the step samples, the result inherits exactly the problem above, one dimension at a time. And an early stop is sound only with respect to the outputs already added — a query about an output outside the constructed prefix has no constraints at all, which is a gap rather than a weakness.

Cost and obligation are separate claims, as they are everywhere else in this article. “Cheaper in dimension” is a measurement. “Contains every reachable point” is an argument, and the two do not stand in for each other.

The simplest correct reference case

For $y=\operatorname{ReLU}(z)$ with $l<0<u$, the graph hull over $[l,u]$ is described by

$$l\le z\le u,\qquad y\ge0,\qquad y\ge z,\qquad y\le\frac{u}{u-l}(z-l).$$

For $[-1,2]$, the upper facet is $y\le 2(z+1)/3$, not merely $y\le2$. The latter can be a looser bound, but calling it the exact triangle hull changes the claim.

This also shows what local exactness means. An exact hull for one ReLU does not automatically give the exact reachable set of an entire network. The multi-neuron chapter examines the missing joint relationships.

What the research and the library contribute

WraLU and WraAct study activation-hull approximation using the structure of the functions. The corresponding project pages connect the papers, full author lists and experimental artifacts. They should not be replaced by a generic story about sampling arbitrary nonlinear functions.

The maintained wraact library is a related software resource, not the same object as the archived paper artifact. Its README, checked on 2026-10-01, describes NumPy input constraints and a cal_hull interface. Older snippets using forward(input_bounds) and grid_density should not be carried forward as an unversioned public API.

The documented constraint convention is

$$b+A_xx+A_yy\ge0.$$

A caller must know the column order, input dimension, output dimension and sign convention. Misreading one of them can turn valid coefficients into the wrong property even when the hull-generation algorithm is correct.

Test different obligations separately

An integration test should first check the interface: accepted input shapes, output column count and variable order. A numerical example can then evaluate the constraints on actual graph points and compare against an analytically understood case.

Those are valuable tests, but a successful finite test set is still not a proof of global containment. The mathematical argument must cover every input in the specified domain. Floating-point computation creates another obligation: valid real-arithmetic inequalities can require a justified numerical treatment before they support a machine-level certificate.

Performance claims need the same separation. Hull-construction time, number of constraints and end-to-end verification time are different measurements. A faster geometric subroutine does not imply the same factor of speedup for the full verifier.

How to read these in sequence

Start with bound propagation for the role of sound bounds, then joint relaxations for the geometry they preserve. The WraLU explanation describes the structural idea behind one of the research methods. Consult the maintained repository for current installation and API details.