TorchLean API

Docs HomeGuideExamplesGraphs

NN.API.Models.Resnet

ResNet Model Helpers (API) #

This module provides a ResNet-style classifier constructor used by runnable examples.

The architecture is small enough to keep the Lean shape arguments readable while still following the standard ResNet pattern:

The positivity proofs below are Lean's way of recording that pooling axes are nonempty. The public constructor is nn.models.resnet cfg; executable examples can decide separately whether this heavier residual path belongs in their runtime budget.

source
structure NN.API.nn.models.ResnetConfig :
Type

Configuration for a ResNet-style image classifier.

Instances For
    source
    def NN.API.nn.models.instReprResnetConfig.repr :
    ResnetConfig → ℕ → Std.Format
    Instances For
      source
      @[implicit_reducible]
      instance NN.API.nn.models.instReprResnetConfig :
      Repr ResnetConfig
      source
      def NN.API.nn.models.ResnetConfig.stage2C (cfg : ResnetConfig) :
      ℕ

      Channel count of the second ResNet stage.

      Instances For
        source
        def NN.API.nn.models.ResnetConfig.h2 (cfg : ResnetConfig) :
        ℕ

        Spatial height after the downsampling block.

        Instances For
          source
          def NN.API.nn.models.ResnetConfig.w2 (cfg : ResnetConfig) :
          ℕ

          Spatial width after the downsampling block.

          Instances For
            source
            @[reducible, inline]
            abbrev NN.API.nn.models.resnetInShape (cfg : ResnetConfig) :
            Shape

            Batched image input shape for the ResNet helper.

            Instances For
              source
              @[reducible, inline]
              abbrev NN.API.nn.models.resnetOutShape (cfg : ResnetConfig) :
              Shape

              Batched classifier-logit output shape for the ResNet helper.

              Instances For
                source
                def NN.API.nn.models.resnet (cfg : ResnetConfig) (h_batch : cfg.batch ≠ 0 := by decide) (h_inC : cfg.inC ≠ 0 := by decide) (h_inH : cfg.inH ≠ 0 := by decide) (h_inW : cfg.inW ≠ 0 := by decide) (h_stemC : cfg.stemC ≠ 0 := by decide) (h_stage2C : cfg.stage2C ≠ 0 := by decide) :
                M (Sequential (resnetInShape cfg) (resnetOutShape cfg))

                Build a ResNet-style image classifier.

                Architecture: conv3x3 stem -> batch norm -> ReLU -> basic block -> downsampling basic block -> basic block -> global average pool -> linear head.

                The explicit proof arguments are optional defaults. For concrete model configs they are solved by by decide; keeping them here hides the proof arguments from runnable examples.

                Instances For