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.

@[instance_reducible]

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

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

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.checkEntry (numClasses : ℕ) (ex : Lean.Json) : IO (Bool × Bool)

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

def NN.Verification.Robustness.MarginCert.check (path : String) (timing : Bool := false) (timingEvery : ℕ := 0) : IO Unit

Check the internal consistency of a robust_margin_cert_v0_1 JSON report.

With timing := true, print a timing summary. A positive timingEvery also prints per-entry timings at that interval; zero leaves only the summary.

structure NN.Verification.Robustness.MarginCert.Options : 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.Options.parse (args : List String) (defaultPath : String) : Except String Options

Parse report-checker flags, using defaultPath when no report path is supplied.

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

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