MnistFcVerify

VNN-COMP-style mini-suite checker (MNIST-FC, VNN-COMP 2022 benchmark).

This tool is intentionally compact:

• it consumes ONNX+VNNLIB instances via JSON artifacts, and
• it runs TorchLean's IBP / (basic) CROWN bounds on the imported MLP, then 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

structure NN.Examples.Verification.VNNComp.MnistFcVerify.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 quick local checks).

• mode : String

  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.Examples.Verification.VNNComp.MnistFcVerify.instReprMnistFCOpts.repr : MnistFCOpts → ℕ → Std.Format

@[implicit_reducible]

instance NN.Examples.Verification.VNNComp.MnistFcVerify.instReprMnistFCOpts : Repr MnistFCOpts

def NN.Examples.Verification.VNNComp.MnistFcVerify.usage : String

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

def NN.Examples.Verification.VNNComp.MnistFcVerify.parseArgs : List String → Except String MnistFCOpts

Parse CLI flags into MnistFCOpts.

On --help / -h this returns usage as the error message (so callers can print it and exit).

structure NN.Examples.Verification.VNNComp.MnistFcVerify.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.Examples.Verification.VNNComp.MnistFcVerify.keysForLayer (i : ℕ) : String × String

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

def NN.Examples.Verification.VNNComp.MnistFcVerify.tensorVecOfArray (n : ℕ) (arr : Array Float) : Option (Spec.Tensor Float (Spec.Shape.dim n Spec.Shape.scalar))

Convert a JSON float array into a length-n TorchLean vector tensor (returns none if sizes mismatch).

def NN.Examples.Verification.VNNComp.MnistFcVerify.parseFloatMatrixArray (j : Lean.Json) : Option (Array (Array Float))

Parse a JSON matrix payload (array-of-array-of-floats) into Array (Array Float).

def NN.Examples.Verification.VNNComp.MnistFcVerify.tensorMatOfArray (rows cols : ℕ) (m : Array (Array Float)) : Option (Spec.Tensor Float (Spec.Shape.dim rows (Spec.Shape.dim cols Spec.Shape.scalar)))

Convert a rows × cols float matrix payload into a TorchLean matrix tensor (checks both dimensions).

def NN.Examples.Verification.VNNComp.MnistFcVerify.dedupSortedNat (xs : Array ℕ) : Array ℕ

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

def NN.Examples.Verification.VNNComp.MnistFcVerify.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.Examples.Verification.VNNComp.MnistFcVerify.loadWeights.checkChain : List LayerWB → IO Unit

structure NN.Examples.Verification.VNNComp.MnistFcVerify.Instance : Type

One exported VNN-COMP instance.

spec is a disjunction-of-conjunctions: each term is a conjunction mat * y <= rhs over the network output vector y.

• id : ℕ

  Instance id (copied from the exported suite JSON).

• inputLo : Array Float

  Lower bound for the input box (x_lo).

• inputHi : Array Float

  Upper bound for the input box (x_hi).

• spec : Array (Array (Array Float) × Array Float)

  Disjunction terms, each a conjunction mat * y <= rhs.

def NN.Examples.Verification.VNNComp.MnistFcVerify.parseMat (j : Lean.Json) : IO (Array (Array Float))

Parse a matrix payload (Array (Array Float)) from JSON, throwing if the shape is not right.

def NN.Examples.Verification.VNNComp.MnistFcVerify.loadSuite (path : String) : IO (Array Instance)

Load the exported VNN-COMP suite JSON.

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

structure NN.Examples.Verification.VNNComp.MnistFcVerify.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.Examples.Verification.VNNComp.MnistFcVerify.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.Examples.Verification.VNNComp.MnistFcVerify.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.Examples.Verification.VNNComp.MnistFcVerify.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.Examples.Verification.VNNComp.MnistFcVerify.vnnlibRefutedByOutputBox (yLo yHi : Array Float) (spec : Array (Array (Array Float) × Array Float)) : Bool

Check whether an unsafe VNNLIB spec is refuted by an output interval box.

Given an output box y ∈ [yLo, yHi], we conservatively lower-bound each linear constraint row aᵀ y and check if some constraint in each disjunct term is violated (lb > rhs).

If every disjunct term is refuted this way, the unsafe spec is unsatisfiable for this output box, so the instance is certified safe (a sufficient condition).

def NN.Examples.Verification.VNNComp.MnistFcVerify.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.Examples.Verification.VNNComp.MnistFcVerify.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.Examples.Verification.VNNComp.MnistFcVerify.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.Examples.Verification.VNNComp.MnistFcVerify.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.Examples.Verification.VNNComp.MnistFcVerify.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.Examples.Verification.VNNComp.MnistFcVerify.vnnlibRefutedByCROWNObjectives (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (xB : MLTheory.CROWN.FlatBox Float) (inId outId inDim outDim : ℕ) (spec : Array (Array (Array Float) × Array Float)) : 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.Examples.Verification.VNNComp.MnistFcVerify.vnnlibRefutedByCROWNObjectivesAlpha (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (xB : MLTheory.CROWN.FlatBox Float) (inId outId inDim outDim : ℕ) (spec : Array (Array (Array Float) × Array Float)) (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.Examples.Verification.VNNComp.MnistFcVerify.main (args : List String) : IO Unit

CLI entry point.

This is wired into lake exe verify -- vnncomp-mnistfc (see NN/Examples/README.md).