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:

Our goal is to keep the runnable torchlean resnet example focused on data loading, optimizer choice, and reporting. The positivity proofs below are Lean's way of recording that pooling axes are nonempty; callers should normally just use nn.models.resnet cfg.

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) :
      ℕ
      Instances For
        source
        def NN.API.nn.models.ResnetConfig.h2 (cfg : ResnetConfig) :
        ℕ
        Instances For
          source
          def NN.API.nn.models.ResnetConfig.w2 (cfg : ResnetConfig) :
          ℕ
          Instances For
            source
            @[reducible, inline]
            abbrev NN.API.nn.models.resnetInShape (cfg : ResnetConfig) :
            Shape
            Instances For
              source
              @[reducible, inline]
              abbrev NN.API.nn.models.resnetOutShape (cfg : ResnetConfig) :
              Shape
              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