What Does a Neural Network Verifier Prove?

A neural network verifier is asked a question with three parts: a network, a set of inputs, and a property. What it returns is one of three answers, and the difference between them is the whole subject of this chapter.

Start from the three parts, because each one is a choice somebody made, and a claim without all three is not yet a claim.

What is being asked

Let $f$ be a fixed network. Let $\mathcal{X}$ be the set of inputs the question ranges over. Let $Q$ be the property the output has to satisfy. The question is

\forall x \in \mathcal{X}:\ Q\bigl(f(x)\bigr).

Change any one of the three and it is a different question. A different $\mathcal{X}$ — a larger perturbation budget, a different normal form, a set that is a union rather than a ball — admits different inputs and can change the answer. A different $Q$ — positivity of an output, or a margin against a class — is a different property on the same network. A different $f$ — the network, or its preprocessing — is a different model entirely, and a certificate about one says nothing about another.

This matters more than it first appears. “This network is robust” is not a statement. “This network is robust to $\ell_\infty$ perturbations of size $\epsilon=2/255$ around the specified normalised input, with the preprocessing pipeline applied exactly as specified” is a statement, and it is checkable. Most disagreements about robustness claims are really disagreements about which of the three parts was fixed.

Three answers, and they do not substitute for each other

Take one small network and hold it fixed. With $x \in [-1,1]$ , let

h_1=\operatorname{ReLU}(x),\qquad h_2=\operatorname{ReLU}(-x),\qquad s=h_1+h_2.

Since at most one of $x$ and $-x$ is positive, $s=|x|$ exactly, and $\max s = 1$ on this input set. Now ask two properties of the same network.

Property A: $s \le 1.5$ . Interval propagation gives $h_1 \in [0,1]$ and $h_2 \in [0,1]$ , so $s \in [0,2]$ , and the upper bound 2 does not settle 1.5. The triangle relaxation gives $h_1 \le \tfrac{x+1}{2}$ and $h_2 \le \tfrac{1-x}{2}$ , which sums to $s \le 1$ . That settles it. A tool reporting SAFE here has been given a valid argument: $s \le 1 \le 1.5$ holds for every $x \in [-1,1]$ .

Property B: $s \le 0.5$ . The same triangle relaxation gives the same upper bound 1, which again does not settle 0.5. A tool that can only produce bounds reports UNKNOWN — a statement about the tool, not about the network. Refuting the property needs no completeness at all: evaluate one input, $x=1$ , and $s=1>0.5$ . That is a complete and checkable refutation, and any search that tried that point first would have returned it without any completeness argument. What the two activation cases buy is the stronger statement, that the relaxation is tight rather than merely satisfied: for $x \ge 0$ the pair is $(x, 0)$ and $s=x$ ; for $x \le 0$ it is $(0, -x)$ and $s=-x$ , so the maximum really is 1. And they are what lets a method reach that verdict on its own, rather than only when it happens to try a decisive point first.

Neither result replaced the other. The first property needed the relaxation and would have been unprovable by brute force on anything larger. The second needed one input evaluation, so a bound-based tool reporting UNKNOWN was not missing a counterexample anyone could have handed it — it had failed to prove there wasn’t one, which is a different gap, and the one completeness is about.

So the three answers are:

SAFE — a valid argument exists that the property holds for every $x \in \mathcal{X}$ .
UNSAFE — a specific $x$ was produced, and evaluating $f$ at it violates the property.
UNKNOWN — neither argument was produced.

UNKNOWN is the one that is easy to misread. It is not a weak form of UNSAFE, and a sound tool will report it on robust networks. It is also not a claim that the question is undecidable: an incomplete method is a statement about the method.

What soundness and completeness each license

Each answer is licensed by a different property of the tool, and the two properties are independent of each other.

Soundness licenses both SAFE and UNSAFE. It means the tool never produces a conclusion it cannot justify: a bound really contains every reachable value, and a witness really violates the property. A sound tool that reports UNKNOWN has told the truth.

Completeness says the tool will always reach a conclusion. It does not say the tool is correct — a complete and unsound tool will happily return a false SAFE. Completeness is what turns “no answer yet” into an answer, and it is what lets a verdict be reached without depending on having guessed a decisive input. It is not what makes a counterexample valid — the witness above is checkable by anyone willing to evaluate one point — and property A was settled by an upper bound rather than by a search, so completeness was not what it needed either.

A tool can also stop for a reason that is neither: a time limit, a memory limit, a numerical difficulty. That is a property of the run, not of the method, and a harness that reports it as UNKNOWN has conflated two different things. This is why competition results record a third state, and why a timeout is not evidence of incompleteness in the theoretical sense.

The trade-off is real but it is not a definition. It is common to hear that complete methods are slow and incomplete methods are fast, and as a description of what gets deployed that is roughly right. As a definition it is wrong in both directions: a complete method on a small network finishes instantly, and an incomplete method can be arbitrarily slow if its bound computation is expensive. Nothing about the word “complete” tells you the running time, and nothing about “incomplete” tells you it is cheap.

Where the difficulty is

The question above is elementary. Verifying it for a network with millions of parameters, over a region defined simultaneously in all of them, is not.

The obstacle is not that the input set is infinite, in the sense of being uncountable — that is handled by working with bounds over a set rather than enumerating points. The obstacle is that the network’s behaviour is a composition of many non-linear operations, and each one multiplies the number of combinations that have to be considered consistent. Two ReLUs reading one input, one of them negated, give two cases. In general $n$ unstable ReLUs give at most $2^n$ naive candidate activation patterns, and the input domain together with the dependency structure between neurons rules many of them out before any is solved. What is left is not a number an enumeration finishes.

Verification is the study of how to answer a question like the one above without enumerating those cases, and what may be given up to do it. The next chapters take the three parts of the question in turn: the property and the input set in threat models, the formal statement in the verification problem, and why a general answer is not expected in theoretical barriers.

Key Takeaways

A robustness claim is only meaningful with all three parts. The network, the input set, and the property. Two claims that differ in one of them are two claims, and the difference can be the difference between robust and not.

SAFE, UNSAFE and UNKNOWN are three different statements. SAFE is an argument, UNSAFE comes with a witness you can check by evaluating the network, and UNKNOWN is a statement about the method rather than about the network.

Soundness and completeness license different things. Soundness makes every reported answer trustworthy and is what makes UNKNOWN honest. Completeness is what produces an answer at all, and it is orthogonal to whether the answer is right.

A timeout is not a property of the method. “Complete” and “incomplete” describe what a method is guaranteed to do; a run that stops early has not thereby become a different kind of method.

Empirical testing and verification answer different questions. A measured robustness rate is a reproducible number over a sample. A certificate is a statement over a region. Neither substitutes for the other, and the gap between them is where the difficulty lives.