VNN-COMP MNIST-FC Checker

VNN-COMP-style mini-suite checker for the MNIST-FC benchmark.

The command consumes exported ONNX/VNNLIB JSON artifacts, runs TorchLean IBP or CROWN bounds on the imported MLP, and checks the VNNLIB disjunction-of-conjunctions constraints using a sufficient condition on the output box.

The checker expects exported JSON artifacts. Keep large VNN-COMP snapshots outside git, for example under _external/vnncomp/mnist_fc/, and pass explicit paths when needed.

Run (Lean): scripts/lake.sh exe verify -- vnncomp-mnistfc

inductive NN.Verification.VNNComp.MnistFC.Mode : Type

Bound propagation/checking mode for the MNIST-FC mini-suite.

• ibp : Mode

  IBP only: fast but loose.

• crown : Mode

  Forward CROWN output box.

• crownObj : Mode

  Backward CROWN objective pass for each VNNLIB row.

@[instance_reducible]

instance NN.Verification.VNNComp.MnistFC.instDecidableEqMode : DecidableEq Mode

@[instance_reducible]

instance NN.Verification.VNNComp.MnistFC.instReprMode : Repr Mode

def NN.Verification.VNNComp.MnistFC.instReprMode.repr : Mode → ℕ → Std.Format

def NN.Verification.VNNComp.MnistFC.Mode.toString : Mode → String

CLI spelling for a VNN-COMP checker mode.

@[instance_reducible]

instance NN.Verification.VNNComp.MnistFC.Mode.instToString : ToString Mode

def NN.Verification.VNNComp.MnistFC.Mode.parse (s : String) : Except String Mode

Parse the --mode value accepted by the MNIST-FC checker.

def NN.Verification.VNNComp.MnistFC.defaultWeightsPath : String

Default ignored-local MNIST-FC weights export.

def NN.Verification.VNNComp.MnistFC.defaultSuitePath : String

Default ignored-local MNIST-FC suite export.

structure NN.Verification.VNNComp.MnistFC.Options : Type

Command-line options for the MNIST-FC VNN-COMP mini-suite verifier.

The defaults point at ignored local artifact paths under _external/vnncomp/mnist_fc/.

• weights : String

  Path to exported weights (model_weights.json).

• suite : String

  Path to exported instance suite (suite.json).

• max : ℕ

  Maximum number of instances to check (useful for local checks).

• mode : Mode

  Bound propagation mode:

  • ibp: IBP only (fast, loose)
  • crown: forward CROWN (still produces just an output box)
  • crownobj: backward objective pass for each spec row

@[instance_reducible]

instance NN.Verification.VNNComp.MnistFC.instReprOptions : Repr Options

def NN.Verification.VNNComp.MnistFC.instReprOptions.repr : Options → ℕ → Std.Format

def NN.Verification.VNNComp.MnistFC.usage : String

Usage text printed by this tool (returned as an error message on --help).

def NN.Verification.VNNComp.MnistFC.parseArgs (args : List String) : Except String Options

Parse CLI flags into Options.

def NN.Verification.VNNComp.MnistFC.requireArtifact (label path : String) : IO Unit

Fail early with a helpful message when an external artifact is missing.

Unlike Data.requireFile, this appends the full usage text, since a missing VNN-COMP snapshot usually means the artifacts were never exported. It also keeps NN.API.Data.Sources and its CSV/.npy loader stack off this checker's import path.

structure NN.Verification.VNNComp.MnistFC.LayerWB : Type

Weights for one exported fully-connected layer ($y=Wx+b$).

Each layer stores PyTorch's row-major weights and bias with their checked dimensions.

• inDim : ℕ

  Input dimension for this layer.

• outDim : ℕ

  Output dimension for this layer.

• w : TorchLean.Tensor Float [self.outDim, self.inDim]

  Weight matrix, shape (outDim × inDim).

• b : TorchLean.Tensor Float [self.outDim]

  Bias vector, shape (outDim).

def NN.Verification.VNNComp.MnistFC.keysForLayer (i : ℕ) : String × String

State-dict keys for the i-th linear layer exported by the Python script.

def NN.Verification.VNNComp.MnistFC.loadWeights (path : String) : IO (Array LayerWB)

Load an exported MNIST-FC model from JSON weights.

This expects keys like layers.0.weight, layers.0.bias, etc, and checks that the linear layer dimensions form a consistent chain.

def NN.Verification.VNNComp.MnistFC.buildGraphAndParams (layers : Array LayerWB) : IO (MLTheory.CROWN.Graph × MLTheory.CROWN.Graph.ParamStore Float × ℕ × ℕ × ℕ)

Lower the loaded weights into a CROWN Graph + ParamStore.

The graph alternates linear layers and ReLUs, ending with a linear layer. The number of layers comes from the export. Return its parameters, input/output dimensions, and output node id.

def NN.Verification.VNNComp.MnistFC.outputBoxIBP (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (outId : ℕ) : IO (MLTheory.CROWN.FlatBox Float)

Compute an output interval box using IBP (fast, loose).

def NN.Verification.VNNComp.MnistFC.outputBoxCROWN (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (xB : MLTheory.CROWN.FlatBox Float) (inId outId inDim : ℕ) : IO (MLTheory.CROWN.FlatBox Float)

Compute an output interval box by running forward CROWN and evaluating the affine bounds on the input box.

def NN.Verification.VNNComp.MnistFC.boxesForObjective (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (xB : MLTheory.CROWN.FlatBox Float) (inId inDim : ℕ) : IO (Array (Option (MLTheory.CROWN.FlatBox Float)))

Compute per-node interval boxes to be used by the backward objective pass.

We start from IBP boxes and (when the input dimension is small) refine a small set of parent-node intervals by evaluating forward CROWN affines on the input box. This makes objective bounds tighter without paying the full cost of "evaluate every affine on the input box".

def NN.Verification.VNNComp.MnistFC.refutesRowByCROWNObjective (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (xB : MLTheory.CROWN.FlatBox Float) (ibp : Array (Option (MLTheory.CROWN.FlatBox Float))) (ctx : MLTheory.CROWN.Graph.AffineCtx) (outId outDim : ℕ) (row : TorchLean.Tensor Float [outDim]) (rhs : Float) : IO Bool

Try to refute a single spec row using a backward CROWN objective bound.

We build an objective $\mathrm{obj}=\mathrm{row}$ and lower-bound $\mathrm{row}^{\mathsf{T}}y$ over the input box. If the lower bound is strictly greater than rhs, then the constraint rowᵀ y <= rhs cannot hold.

def NN.Verification.VNNComp.MnistFC.vnnlibRefutedByCROWNObjectives (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (xB : MLTheory.CROWN.FlatBox Float) (inId outId inDim outDim : ℕ) (spec : VNNLib.Spec) : IO Bool

Refute a VNNLIB disjunction-of-conjunctions spec using per-row CROWN objective bounds.

Each row is bounded directly, avoiding some correlations lost when evaluating a row over an output interval box. This implementation does not guarantee that every resulting bound is tighter.

def NN.Verification.VNNComp.MnistFC.main (args : List String) : IO Unit

CLI entry point.

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