Documentation

LeanMlir.ParamLayouts

The verified trainers' packed-parameter layouts #

One namespace per verified ImageNet-scale net (ResNet34Layout, MobileNetV2Layout, EfficientNetLayout, ConvNeXtLayout, ViTLayout): each net's (dims, initKind) list in the train step's argument order, plus the packed shape descriptors (packShapes, packXShape) the runtime passes to the FFI. Pure data — importing only LEBytes — so the spec side (Verified.NetsCore's #guard spec.toSpecs == XLayout.specs) can read the tables without importing the runtime.

References #

source
def packShapes (shapes : Array (Array Nat)) :
ByteArray

Pack param shape descriptors: [nParams, rank0, d0..., rank1, d1..., ...] as int32 LE.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def packXShape (dims : Array Nat) :
    ByteArray

    Pack a single shape: [rank, d0, d1, ...] as int32 LE (for x input).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def ResNet34Layout.specs :
      Array (Array Nat × Nat)

      (dims, initKind) for every param, in func-arg order.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def MobileNetV2Layout.specs :
        Array (Array Nat × Nat)

        (dims, initKind) for every param, in func-arg order.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def EfficientNetLayout.specs :
          Array (Array Nat × Nat)

          (dims, initKind) for every param, in func-arg order — generated from the B0 stage spec exactly as tests/TestEfficientNet*.lean blocks (stem out 32, prev threading).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def ConvNeXtLayout.specs :
            Array (Array Nat × Nat)

            (dims, initKind) for every param, in func-arg order.

            The head is GAP → LN(768) → dense, as in both the paper (self.norm(x.mean([-2,-1])), nn.LayerNorm(dims[-1], eps=1e-6)) and timm (NormMlpClassifierHead). 182 param tensors; the floats are 27,827,818 at K = 10, i.e. 28,589,128 at K = 1000 — timm's count. Without the head LN the count would be short by exactly 2×768 = 1,536, so a near-matching count is not evidence of the right architecture.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def ViTLayout.specs :
              Array (Array Nat × Nat)

              (dims, initKind) for every param, in @vit_train_step func-arg order.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For