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): lake 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.

• crownObjAlpha : Mode

  Backward CROWN objective pass with imported ReLU slopes.

@[implicit_reducible]

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

@[implicit_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.

@[implicit_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.MnistFCOpts : 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
  • crownobj-alpha: objective pass with precomputed ReLU slopes (--alphas)
• alphas : String

  Path to exported alpha slopes JSON (required for mode = crownobj-alpha).

def NN.Verification.VNNComp.MnistFC.instReprMnistFCOpts.repr : MnistFCOpts → ℕ → Std.Format

@[implicit_reducible]

instance NN.Verification.VNNComp.MnistFC.instReprMnistFCOpts : Repr MnistFCOpts

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 MnistFCOpts

Parse CLI flags into MnistFCOpts.

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

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

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

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

This is the lightest data structure we need to rebuild a CROWN Graph for MNIST-FC.

• inDim : ℕ

  Input dimension for this layer.

• outDim : ℕ

  Output dimension for this layer.

• w : Spec.Tensor Float (Spec.Shape.dim self.outDim (Spec.Shape.dim self.inDim Spec.Shape.scalar))

  Weight matrix, shape (outDim × inDim).

• b : Spec.Tensor Float (Spec.Shape.dim self.outDim Spec.Shape.scalar)

  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.dedupSortedNat (xs : Array ℕ) : Array ℕ

Deduplicate a sorted list of natural numbers (used to normalize layer indices discovered from JSON keys).

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.loadWeights.checkChain : List LayerWB → IO Unit

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

One set of precomputed ReLU alpha slopes for crownobj-alpha mode.

This checker assumes the MNIST-FC graph has ReLU nodes at fixed ids (2 and 4), so we store the alpha vectors in a format that can be mapped back to those nodes.

• id : ℕ

  Instance id this alpha payload applies to.

• alpha2 : Array (Array Float)

  Alpha vectors for ReLU node 2, indexed by disjunct term.

• alpha4 : Array (Array Float)

  Alpha vectors for ReLU node 4, indexed by disjunct term.

def NN.Verification.VNNComp.MnistFC.loadAlphas (path : String) : IO (Array AlphaEntry)

Load the exported alpha slopes database (for mode = crownobj-alpha).

This expects the mnist_fc_crownobj_alpha_v0_1 format produced by the Python export script.

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.

For MNIST-FC we build: input -> linear -> relu -> linear -> relu -> linear and return the graph plus the inferred inDim, outDim, and output node id.

def NN.Verification.VNNComp.MnistFC.buildGraphAndParams.go (parentId : ℕ) (nodes : Array MLTheory.CROWN.Graph.Node) (ps : MLTheory.CROWN.Graph.ParamStore Float) (rem : List LayerWB) : Array MLTheory.CROWN.Graph.Node × MLTheory.CROWN.Graph.ParamStore Float × ℕ

def NN.Verification.VNNComp.MnistFC.outputBoxIBP (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (outId : ℕ) : IO (Array Float × Array 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 (Array Float × Array 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 _inDim outDim : ℕ) (row : Array Float) (rhs : Float) : IO Bool

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

We build an objective obj = row and lower-bound rowᵀ 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.refutesRowByCROWNObjectiveWithReluAlpha (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (xB : MLTheory.CROWN.FlatBox Float) (ibp : Array (Option (MLTheory.CROWN.FlatBox Float))) (inId outId inDim outDim : ℕ) (row : Array Float) (rhs : Float) (reluAlpha : Array (Option (MLTheory.CROWN.Graph.FlatVec Float))) : IO Bool

Like refutesRowByCROWNObjective, but use precomputed ReLU alpha slopes.

This is a workflow hook for comparing against "fixed alpha" CROWN objective bounds exported from a reference implementation.

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.

This is strictly stronger than checking an output interval box, but it is also slower.

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

Refute a VNNLIB spec using CROWN objectives with externally-provided ReLU alphas.

This mode is meant for apples-to-apples comparisons against alpha-CROWN style tools where the alphas are optimized elsewhere and then imported into TorchLean for checking.

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

CLI entry point.

This is wired into lake exe verify -- vnncomp-mnistfc.