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)
  • CROWN (outputBoxCROWN?), which takes each lower endpoint from the lower affine form and each upper endpoint from the upper form

Run: scripts/lake.sh exe verify -- digits scripts/lake.sh exe verify -- digits --eps=0.02 --max=360 scripts/lake.sh exe verify -- digits --arithmetic ieee --eps=0.02 scripts/lake.sh 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.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.Options : 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.instReprOptions.repr : Options → ℕ → Std.Format

@[instance_reducible]

instance NN.Verification.Robustness.Digits.instReprOptions : Repr Options

structure NN.Verification.Robustness.Digits.Training.Options : Type

Options for the train → lower → certify report command.

• certify : Digits.Options

  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.Training.instReprOptions.repr : Options → ℕ → Std.Format

@[instance_reducible]

instance NN.Verification.Robustness.Digits.Training.instReprOptions : Repr Options

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

Usage string printed on --help / -h.

def NN.Verification.Robustness.Digits.Options.parseRest (args : List String) : Except String (Options × List String)

Consume the certification flags shared by both digits commands (after -- stripping and the --help check), returning the remaining arguments. Flags are extracted by key, so the caller may consume its own flags from the remainder in any order.

def NN.Verification.Robustness.Digits.Options.parse (args : List String) : Except String Options

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

def NN.Verification.Robustness.Digits.Training.parse (args : List String) : Except String Options

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

def NN.Verification.Robustness.Digits.Training.args (options : Options) : Array String

Python trainer arguments, including the artifact destinations checked by Lean afterward.

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

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

def NN.Verification.Robustness.Digits.loadDataset (path : String) : IO (Array (TorchLean.Tensor Float [64] × ℕ))

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

structure NN.Verification.Robustness.Digits.Report : 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.

@[instance_reducible]

instance NN.Verification.Robustness.Digits.instReprReport : Repr Report

def NN.Verification.Robustness.Digits.instReprReport.repr : Report → ℕ → Std.Format

def NN.Verification.Robustness.Digits.inputBox {α : Type} [TorchLean.Storage α] [Context α] [TorchLean.Runtime.FromFloat α] {shape : Spec.Shape} (x : TorchLean.Tensor Float shape) (eps : Float) : MLTheory.CROWN.FlatBox α

The certified input box: the binary64 ℓ∞ ball around x, rounded outward by FlatBox.lInfBall, clipped to the pixel range [0, 1], and converted to α with the directed rounding of TorchLean.Runtime.ofFloatDirected. It contains every real input within eps of the binary64 center that lies in [0, 1].

def NN.Verification.Robustness.Digits.run {α : Type} [TorchLean.Storage α] [Context α] [MLTheory.CROWN.BoundOps α] [MLTheory.CROWN.NonlinearBoundOps α] [ToString α] [TorchLean.Runtime.FromFloat α] (options : Options) : IO Report

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

This lowers the linear classifier to the verifier IR, then checks each example's $L^\infty$ box using IBP and two-sided CROWN output bounds.

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

CLI entry point for the digits certified-robustness workflow.

This is wired into scripts/lake.sh exe verify -- digits.

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

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

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