Certified label checks #
Shared predicates for certified classification from output bounds.
The checker uses one rule: the claimed label's lower bound must be strictly above every other class upper bound. Bounds use equally shaped tensors, including after JSON decoding.
def
NN.Verification.Robustness.TopLabel.check
{α : Type}
[TorchLean.Storage α]
[Context α]
{n : ℕ}
(lo hi : TorchLean.Tensor α [n])
(label : ℕ)
:
Check that the label's lower bound strictly exceeds every competing upper bound. An out-of-range label or unordered comparison returns false.