Logit-Bound Report Checker

Reusable consistency checker for exported per-example logit bounds (robust_margin_cert_v0_1).

The checker reads exported output bounds and recomputes the strict top-label margin:

$\mathrm{logits}_{\mathrm{hi}}[j]<\mathrm{logits}_{\mathrm{lo}}[\mathrm{label}]$ for every $j\neq\mathrm{label}$.

This module does not establish that the bounds enclose a model on an input region. That requires a separate verifier or a TorchLean propagation theorem. The checker validates only the internal arithmetic and summary fields of the supplied report.

def NN.Verification.Robustness.MarginCert.formatTag : String

Format tag expected at the top level of exported logit-bound reports.

structure NN.Verification.Robustness.MarginCert.Counters : Type

Running counters for nominal accuracy and margin outcomes.

• total : ℕ

  Number of examples checked.

• nominalOk : ℕ

  Number of examples whose optional nominal prediction equals the label.

• certifiedOk : ℕ

  Number of examples certified by the margin predicate.

def NN.Verification.Robustness.MarginCert.instReprCounters.repr : Counters → ℕ → Std.Format

@[instance_reducible]

instance NN.Verification.Robustness.MarginCert.instReprCounters : Repr Counters

def NN.Verification.Robustness.MarginCert.Counters.push (counts : Counters) (nominalOk cert : Bool) : Counters

Add one (nominalOk, certifiedOk) outcome to the report counters.

def NN.Verification.Robustness.MarginCert.checkOneExample (numClasses : ℕ) (ex : Lean.Json) : IO (Bool × Bool)

Check one report entry and return (nominalOk, positiveMargin).

def NN.Verification.Robustness.MarginCert.checkWithTiming (path : String) (timing : Bool) (timingEvery : ℕ) : IO Unit

Check the internal consistency of a robust_margin_cert_v0_1 JSON report.

If timing = true, prints per-example timings every timingEvery examples.

def NN.Verification.Robustness.MarginCert.check (path : String) : IO Unit

Check a logit-bound report with timing disabled.

structure NN.Verification.Robustness.MarginCert.RunArgs : Type

Parsed CLI flags for a logit-bound report run.

• path : String

  Report JSON path.

• timing : Bool

  Print per-example checker timings.

• timingEvery : ℕ

  Print every timingEvery examples when timing is enabled; 0 disables periodic lines.

def NN.Verification.Robustness.MarginCert.parseRunArgs (defaultPath : String) (args : List String) : Except String RunArgs

Parse shared margin-report CLI flags.

def NN.Verification.Robustness.MarginCert.runWithDefault (defaultPath : String) (args : List String) : IO Unit

Run the checker with a caller-provided default report path.