Margin Certificate Checker

Reusable checker for per-example logit-margin certificates (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}$.

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

Certificate format tag expected at the top level of margin certificate JSON files.

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

Running counters for nominal and certified accuracy reports.

• 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

@[implicit_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 JSON example object and return (nominalOk, certifiedOk).

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

Check a robust_margin_cert_v0_1 JSON certificate file.

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

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

Check a margin certificate file with timing disabled.

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

Parsed CLI flags for a margin-certificate run.

• path : String

  Certificate 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-certificate CLI flags.

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

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