VerifyMarginCert

Lean checker for per-example logit-margin certificates (robust_margin_cert_v0_1).

This checker is intentionally lightweight: it does not re-run bound propagation. Instead, it verifies that the exported logit bounds imply the certified margin predicate:

logits_lo[label] > max_{j≠label} logits_hi[j]

Run: python3 scripts/verification/robustness/export_margin_cert.py lake exe verify -- margin-cert

def NN.Examples.Verification.Robustness.VerifyMarginCert.ltBool (x y : Float) : Bool

Boolean < on Float.

def NN.Examples.Verification.Robustness.VerifyMarginCert.leBool (x y : Float) : Bool

Boolean ≤ on Float.

def NN.Examples.Verification.Robustness.VerifyMarginCert.certifiedTop1 (lo hi : Array Float) (label : Nat) : Bool

Check the logit-margin predicate from exported bounds.

Returns true if lo[label] > max_{j≠label} hi[j].

structure NN.Examples.Verification.Robustness.VerifyMarginCert.Counters : Type

Running counters for reporting nominal vs certified accuracy.

• total : Nat

  total.

• nominalOk : Nat

  nominal Ok.

• certifiedOk : Nat

  certified Ok.

def NN.Examples.Verification.Robustness.VerifyMarginCert.instReprCounters.repr : Counters → Nat → Std.Format

@[implicit_reducible]

instance NN.Examples.Verification.Robustness.VerifyMarginCert.instReprCounters : Repr Counters

Internal helpers.

def NN.Examples.Verification.Robustness.VerifyMarginCert.checkOneExample (numClasses : Nat) (ex : Lean.Json) : IO (Bool × Bool)

def NN.Examples.Verification.Robustness.VerifyMarginCert.checkWithTiming (path : String) (timing : Bool) (timingEvery : Nat) : IO Unit

Check a robust_margin_cert_v0_1 JSON certificate file.

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

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

Check a margin cert file with timing disabled (thin wrapper around checkWithTiming).

def NN.Examples.Verification.Robustness.VerifyMarginCert.run (args : List String) : IO Unit

CLI entry point: lake exe verify -- margin-cert [cert.json].

If --timing is passed, prints timing information (optionally controlled by --timing-every=N).