Digits certified robustness

Certified accuracy for a linear classifier on sklearn's digits dataset.

Workflow:

• Train a small linear classifier on sklearn's digits (8x8) in Python and export:
  • weights JSON (digits_linear_weights.json)
  • test dataset JSON (digits_test.json)
• In Lean, load the weights + dataset and compute certified accuracy under an ℓ∞ input box using:
  • IBP (runIBP)
  • a simple CROWN/affine pass (runAffine + AffineVec.eval_on_box)

Run: lake exe verify -- digits lake exe verify -- digits --eps=0.02 --max=360 lake exe verify -- digits --float32-mode ieee754exec --eps=0.02

Regenerate assets: python3 scripts/verification/robustness/train_digits_linear.py

def NN.Verification.Robustness.Digits.inDim : ℕ

Flattened input dimension for sklearn digits (8×8).

def NN.Verification.Robustness.Digits.outDim : ℕ

Number of classes (digits 0..9).

def NN.Verification.Robustness.Digits.WShape : Shape

Weight shape for a linear classifier y = Wx + b (10×64).

def NN.Verification.Robustness.Digits.bShape : Shape

Bias shape for a linear classifier (10).

def NN.Verification.Robustness.Digits.xShape : Shape

Input shape (64).

def NN.Verification.Robustness.Digits.yShape : Shape

Output/logit shape (10).

def NN.Verification.Robustness.Digits.paramShapes : List Shape

Parameter shapes list used by the compiled TorchLean program ([W, b]).

structure NN.Verification.Robustness.Digits.DigitsOpts : Type

CLI options for the digits certified-accuracy workflow.

• weights : String

  Weights JSON path (PyTorch export).

• dataset : String

  Dataset JSON path (PyTorch export).

• eps : Float

  L∞ perturbation radius around each input example.

• max : ℕ

  Max number of examples to evaluate (for quick local checks).

def NN.Verification.Robustness.Digits.instReprDigitsOpts.repr : DigitsOpts → ℕ → Std.Format

@[implicit_reducible]

instance NN.Verification.Robustness.Digits.instReprDigitsOpts : Repr DigitsOpts

def NN.Verification.Robustness.Digits.usage : String

Usage string printed on --help / -h.

def NN.Verification.Robustness.Digits.parseFloatLit (s : String) : Option Float

Parse a float literal written as JSON (e.g. 0.02).

def NN.Verification.Robustness.Digits.parseArgs : List String → Except String DigitsOpts

Parse CLI args into DigitsOpts (returns usage as the error message on --help).

def NN.Verification.Robustness.Digits.classifier {α : Type} [Context α] [DecidableEq Shape] : Runtime.Autograd.TorchLean.Program α (paramShapes ++ [xShape]) yShape

TorchLean program for the linear classifier y = Wx + b.

def NN.Verification.Robustness.Digits.clamp01 {α : Type} [Context α] {s : Shape} (t : Spec.Tensor α s) : Spec.Tensor α s

Clamp a tensor elementwise into [0,1] (used for input normalization).

def NN.Verification.Robustness.Digits.argmaxFloat {n : ℕ} (t : Spec.Tensor Float (Spec.Shape.dim n Spec.Shape.scalar)) : ℕ

Argmax for a Float vector tensor (returns 0 if n = 0).

def NN.Verification.Robustness.Digits.certifiedTop1 {α : Type} [Context α] (lo hi : Spec.Tensor α yShape) (label : ℕ) : Bool

Certify top-1 correctness from output bounds.

Given elementwise bounds lo <= y <= hi, this returns true if the lower bound on the true class logit exceeds the upper bounds of all other logits.

def NN.Verification.Robustness.Digits.loadWeights (path : String) : IO (Spec.LinearSpec Float inDim outDim)

Load linear classifier weights exported from PyTorch into a typed LinearSpec.

def NN.Verification.Robustness.Digits.loadDataset (path : String) : IO (Array (Spec.Tensor Float xShape × ℕ))

Load the digits test dataset exported from Python (JSON).

structure NN.Verification.Robustness.Digits.DigitsReport : Type

Running counters for the digits certified-accuracy workflow.

• total : ℕ

  Number of examples checked.

• nominalOk : ℕ

  Number of clean examples classified correctly by the exported model.

• ibpOk : ℕ

  Number of examples certified by interval bound propagation.

• crownOk : ℕ

  Number of examples certified by the affine CROWN pass.

@[implicit_reducible]

instance NN.Verification.Robustness.Digits.instReprDigitsReport : Repr DigitsReport

def NN.Verification.Robustness.Digits.instReprDigitsReport.repr : DigitsReport → ℕ → Std.Format

def NN.Verification.Robustness.Digits.runOnce {α : Type} [API.Semantics.Scalar α] [DecidableEq Shape] [ToString α] [API.Runtime.Scalar α] (opts : DigitsOpts) : IO DigitsReport

Run the certified-accuracy evaluation once, under a chosen scalar backend α.

This compiles the linear classifier to the verifier IR, then checks each example's L∞ box using IBP and a simple affine pass.

def NN.Verification.Robustness.Digits.main (args : List String) : IO Unit

CLI entry point for the digits certified-robustness workflow.

This is wired into lake exe verify -- digits.