The Verification Problem: Properties, Margins, and Counterexamples

A verification question has three ingredients: a fixed network $f$ , an input condition $P$ , and an output condition $Q$ . The statement to check is

\forall x:\ P(x)\Longrightarrow Q(f(x)).

The property is meaningful only relative to those ingredients. Changing preprocessing, the allowed input set or the meaning of the output changes the question.

The equivalent counterexample question

Negating the statement gives

\exists x:\ P(x)\land\neg Q(f(x)).

A solver may search for this bad input rather than directly manipulating a universal statement. If it finds one, we evaluate it in the intended network and check the input constraints. A candidate satisfying only a relaxation of the network is not yet a counterexample.

Use three outcomes for the semantic result: SAFE if the property is established, UNSAFE if a valid violating input is established, and UNKNOWN if neither has been established within the method or budget. A tool’s raw sat label must be interpreted according to the query it solves.

A network we can solve by hand

Throughout several chapters, use

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

The desired property is $g(x)>0$ . For $x\ge0$ , the activations are $(x,0)$ ; for $x\le0$ , they are $(0,-x)$ . In both cases $g(x)=1/4$ . The property therefore holds over the whole interval.

This is a proof by cases over two feasible regions, not a sample test. Later, a relaxation of the same network will allow a negative value. That will show failure of the relaxation to prove the property, not failure of the network.

Classification as a margin property

For output scores $f_c(x)$ and a chosen reference class $y$ , define

m_j(x)=f_y(x)-f_j(x),\qquad j\ne y.

One sufficient and unambiguous requirement is that every margin is strictly positive throughout $X$ . This requires the reference class to be the unique highest-scoring class. A property allowing ties needs an explicit tie-breaking convention instead.

The reference class can be a ground-truth label or the model’s nominal prediction. Those choices answer different questions. Robustly retaining an initially wrong prediction does not establish correctness.

Bounds and witnesses have opposite directions

For a continuous margin on a nonempty compact domain, let

m_j^*=\min_{x\in X}m_j(x).

Suppose a sound method returns a lower bound $L_j\le m_j^*$ . If every $L_j>0$ , the strict-margin property is proved. A lower bound at or below zero does not establish a violation: it may only reflect a loose relaxation.

An actual input $\hat x\in X$ gives the other direction: $m_j^*\le m_j(\hat x)$ . If $m_j(\hat x)\le0$ , it violates the strict property. Always verify that this value comes from the original network rather than from independent relaxed activation variables.

An exercise in reading a result

A verifier returns a sound lower bound of $-0.2$ . An attack finds an input with margin $0.1$ . What has been established?

Answer

Only that the minimum lies between $-0.2$ and $0.1$ . Neither result proves the property or exhibits a violation. The correct conclusion is UNKNOWN, unless another argument is available.

Key Takeaways

Write the property before choosing a tool. Fix the network semantics, input set and required output behaviour.

A negative relaxed bound is not a counterexample. It can mean that the method has not proved enough.

A witness must belong to the original problem. Check its input constraints and evaluate the actual network.