6. Verification and Certificates🔗

Training tells us how a model behaves on the examples it sees. A verification claim can ask about every input in a region, including points never evaluated during training. For a classifier, a useful first property is that the predicted label stays fixed when each input coordinate changes by at most a stated amount. We can express this through the output scores: the chosen class must remain above every competitor.

For a graph g, parameter payload \theta, and input region B, a verification claim has the form

\forall x\in B,\qquad P(\operatorname{denote}(g,\theta,x)).

Here \operatorname{denote} is the chosen graph semantics and P is the property required of each output. Interval and affine bounds establish such properties over whole input regions. Lowering proofs and numerical error bounds justify transferring a claim between representations or arithmetic models. The same need to state what is preserved arises for derivatives and optimizer updates.

The quantifier ∀ x ∈ B is the demanding part. Sampling the box gives examples of behavior; an enclosure gives a bound that applies throughout it under the enclosure theorem's hypotheses. If the chosen score has lower bound L and its competitor has upper bound U, then L > U settles that comparison. A loose enclosure may fail to separate the scores even when the classifier is stable, which is why the choice of interval or affine propagation affects what can be established.

A certificate records evidence used in such an argument. Its contents determine what a checker can justify: a collection of claimed margins, a replayable trace of intermediate bounds, and a Lean value carrying enclosure proofs support different conclusions. The classifier chapter develops the score comparison first, then reads the relevant theorem signatures in terms of that example. The later certificate chapters examine the exported data and the precise conditions needed to turn local bounds into a claim about the whole region.