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 $\ell^\infty$ 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 lake exe verify -- digits-train-certify --epochs=50 --eps=0.02 --max=100

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 : Spec.Shape

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

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

Bias shape for a linear classifier (10).

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

Input shape (64).

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

Output/logit shape (10).

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

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

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

Bundled sklearn-digits linear classifier weights.

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

Bundled sklearn-digits test set.

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

Python exporter used by the train-then-certify command.

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^\infty$ perturbation radius around each input example.

• max : ℕ

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

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

@[implicit_reducible]

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

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

Options for the train → compile → certify report command.

• certify : DigitsOpts

  Lean side certification options after Python exports the model and dataset.

• script : String

  Python trainer script path.

• seed : ℕ

  Reproducibility seed forwarded to the trainer.

• epochs : ℕ

  Number of Python training epochs.

• batch : ℕ

  Python trainer batch size.

• lr : Float

  Python trainer learning rate.

• testSize : Float

  Test split fraction used by the trainer.

• maxTest : ℕ

  Number of test examples exported by the trainer.

def NN.Verification.Robustness.Digits.instReprTrainCertifyOpts.repr : TrainCertifyOpts → ℕ → Std.Format

@[implicit_reducible]

instance NN.Verification.Robustness.Digits.instReprTrainCertifyOpts : Repr TrainCertifyOpts

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

Usage string printed on --help / -h.

def NN.Verification.Robustness.Digits.parseArgs (args : List String) : Except String DigitsOpts

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

def NN.Verification.Robustness.Digits.parseTrainCertifyArgs (args : List String) : Except String TrainCertifyOpts

Parse the combined trainer/certifier CLI for digits-train-certify.

def NN.Verification.Robustness.Digits.trainerArgs (opts : TrainCertifyOpts) : Array String

Trainer command-line arguments generated from TrainCertifyOpts.

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

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

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} [Context α] [MLTheory.CROWN.BoundOps α] [DecidableEq Spec.Shape] [ToString α] [TorchLean.Runtime.FromFloat α] (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^\infty$ 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.

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

Train a fresh digits classifier, compile it through the TorchLean verifier path, and certify it.

The Python trainer is an artifact producer only. Lean still parses the exported JSON, compiles the TorchLean program to verifier IR, runs IBP and affine CROWN bounds, and prints the certification report from the checked artifacts.