Soundness, Completeness, and UNKNOWN

A verification tool can be wrong in two independent ways, and only one of them is a bug. This chapter separates them, and gives each of the three possible outputs an implication that can be checked on paper.

Two independent properties

Soundness is a property of the conclusions. A sound tool never reports SAFE unless it holds a valid argument that the property holds on the whole input set, and never reports UNSAFE without an input that actually violates it.

Completeness is a property of the termination. A complete tool reaches one of those two conclusions for every input set, in finite time.

Neither implies the other, and the four combinations are all real. A complete and unsound method returns a definite answer that may be false. A sound and incomplete method returns UNKNOWN rather than guessing, which is why every deployed verifier is sound. A complete and sound method is the goal, and its cost is the subject of the rest of this series.

It is common to describe complete methods as slow and incomplete methods as fast, and as a description of deployed tooling that is roughly accurate. As a definition it is wrong in both directions: a complete method on a small network finishes in milliseconds, and an incomplete method can be arbitrarily slow if its bound computation is expensive. Completeness describes what a method guarantees about reaching an answer, not how long the answer takes, so a complete method that is too slow to run is not thereby incomplete — it simply has not been given a chance.

A run that stopped because of a time limit or a memory limit is a third thing. It is a property of one execution, not of the method, and a method that would have finished given more time is still complete. This is worth separating because a benchmark that reports timeouts as a separate column is reporting something a method’s definition does not contain.

What each output licenses

Write the outputs as implications, so each one can be checked against what the tool actually returned.

Output	The claim it licenses
SAFE	$\forall x \in \mathcal{X}:\ Q(f(x))$ , established by a valid argument
UNSAFE	$\exists x^\ast \in \mathcal{X}:\ \neg Q(f(x^\ast))$ , with $x^\ast$ returned
UNKNOWN	neither, and the tool says so

The first two are the only two that assert anything about the network. The third asserts something about the method: the search was exhausted, or the budget ran out, without either argument.

The asymmetry in what a witness costs is worth noticing. A SAFE answer is a universal claim and needs an argument covering every input. An UNSAFE answer is existential, and one evaluable point discharges it — you can check it by running the network forward. This is why an unsound tool errs mostly in the SAFE direction, and why “no counterexample was found” is not a statement about the network at all.

A true property with an inconclusive relaxation

An incomplete method returns UNKNOWN when its bound is too loose to settle the question. It is worth seeing that once on an example where the property is genuinely true, because the tempting example — one where the property is false — teaches the wrong lesson.

Take the two-ReLU network from the bound-propagation chapter and ask about an objective rather than an output:

x\in[-1,1],\qquad h_1=\operatorname{ReLU}(x),\qquad h_2=\operatorname{ReLU}(-x),\qquad g=h_1-h_2-x+\tfrac14.

The identity $\operatorname{ReLU}(x)-\operatorname{ReLU}(-x)=x$ makes $g=1/4$ everywhere on the interval, so $g\ge 0$ is true. The complete triangle constraints are

\begin{aligned} h_1&\geq0,& h_1&\geq x,& h_1&\leq \tfrac{x+1}{2},\\ h_2&\geq0,& h_2&\geq -x,& h_2&\leq \tfrac{1-x}{2}. \end{aligned}

Minimising $g$ over that relaxation gives exactly $-1/4$ . It is reached at $x=0$ , and it is worth seeing the two cases rather than taking the number on trust: for $x\ge0$ the binding lower bound is $h_1\ge x$ , giving $g\ge x/2-1/4$ ; for $x\le0$ it is $h_2\le\tfrac{1-x}{2}$ , giving $g\ge -x/2-1/4$ . Both meet at $-1/4$ when $x=0$ .

So the relaxation cannot establish $g\ge0$ , and the relaxed minimiser $(0,0,\tfrac12)$ is not a counterexample: evaluating the actual network at $x=0$ gives $g=1/4$ . This is a genuine relaxation gap on a true property.

Three questions meet at that point, and a reader who runs them together will misdiagnose the failure:

Does the relaxed region admit states the network cannot reach? Yes. $(0,0,\tfrac12)$ is one, and so is $(0,\tfrac12,\tfrac12)$ .
Is the property true? Yes. It holds everywhere, which is why a complete method settles it.
Is the bound tight? No. The true minimum is $1/4$ and the relaxed minimum is $-1/4$ , so the relaxed value is the negative of the true one and the gap between them is $1/2$ .

UNKNOWN is therefore the honest report of a method that reached an inconclusive configuration on a property that is in fact true. The network’s answer and the method’s answer are not in conflict; the method cannot see the difference.

What closes the gap, and what does not. For this objective the joint equality $h_1-h_2=x$ is sufficient: it makes $g=1/4$ throughout the strengthened relaxation, so a method holding it settles the property. It does not make the relaxed set exact — $(0,\tfrac12,\tfrac12)$ satisfies $h_1-h_2=x$ and still lies off the graph. A bound can be exact for one objective while the feasible set still contains spurious points, so “the bound is now tight” and “the relaxation is now exact” are different claims. Splitting on the sign of $x$ is the other route, and it makes each unit’s bound exact on each part.

A trap worth naming, because it is easy to walk into. These bounds belong to the interval they were derived for. On $x\in[-1,1]$ the upper line is $\tfrac{x+1}{2}$ ; on $x\in[-1/2,1/2]$ it is $x/2+1/4$ . Narrowing the domain does not invalidate the wider interval’s bounds — they remain sound, and they remain valid — but they stop being the triangle for the domain at hand, and the extra looseness now belongs to the interval rather than to the network. A relaxation can look entirely reasonable, contain no false statement, and settle less than its author believes, because the bounds on the page were computed for a different page. The check is to derive the secant the stated domain requires and compare it against the bounds on display, which is the only way this gets caught rather than shipped.

Probabilistic certificates are a different kind of object

Some certificates are not universal claims at all. Randomized smoothing replaces the network $f_\theta$ with a smoothed classifier

g(x) = \mathbb{E}_{\text{noise}}\bigl[f_\theta(x + \text{noise})\bigr]

and certifies that, with probability at least $1-\alpha$ over the noise draw, $g$ keeps its prediction within radius $\epsilon$ . Cohen, Rosenfeld and Kolter (2019) give the construction and the soundness argument.

Two things make this a different object from a deterministic certificate rather than a weaker one. The claim is about $g$ , not about $f_\theta$ — a guarantee on the smoothed classifier does not transfer to the raw network without an argument about the smoothing. And the guarantee is an implication guarded by a probability: it holds with probability at least $1-\alpha$ , not for every draw, and $\alpha$ is a parameter of the result rather than an error bar.

The sound/complete axis and the deterministic/probabilistic axis are orthogonal, and conflating them is how a probabilistic certificate ends up described as merely a weaker empirical test. It is a theorem about a specific classifier with a stated failure probability, which is a stronger object than a measured robustness rate and a different one from a deterministic certificate.

Key Takeaways

Soundness and completeness are independent, and neither implies the other. Soundness governs conclusions, completeness governs termination, and a complete unsound method is more dangerous than a sound incomplete one because it does not say UNKNOWN.

Only two of the three outputs make a claim about the network. SAFE is a universal statement with an argument; UNSAFE is existential with a point you can check by evaluating the network; UNKNOWN is a statement about the method.

UNKNOWN means the relaxation was too loose, not that the network is fragile. A spurious point in the relaxed region is the usual cause, and it is a point the network cannot reach, which is why more compute on the same relaxation does not help.

Completeness is a guarantee, not a cost. Whether a complete method finishes quickly depends on the instance and the budget, and a run that stopped early has not become a different kind of method.

A probabilistic certificate is about a different object. It constrains a smoothed classifier, and it holds with probability at least $1-\alpha$ rather than universally. It is not an empirical robustness rate, and it is not a weaker version of a deterministic certificate.