TorchLean API

NN.API.SelfSupervised.MaskedPrediction

Masked-Prediction API #

Self-supervised learning is primarily a training objective and data-view interface, not a special kind of layer.

This module is the public, model-independent SSL surface:

Architecture constructors, when useful, live under NN.API.Models.*. For example, a compact vector autoencoder is convenient for CIFAR runs, but the MAE idea itself belongs here: create a masked view of a tensor and reconstruct the original content.

Compact MAE-style masked reconstruction #

The hidden-coordinate mask used by compact MAE training.

true means "this feature coordinate is hidden from the encoder." The type is the finite-mask type used in the ML-theory files, specialized to the feature axis of a batch × dataDim matrix.

Instances For

    Feature-level deterministic mask for MAE samples over a batch × dataDim matrix.

    Every coordinate whose index is congruent to offset modulo period is hidden by setting it to zero. The mask is deterministic so examples and tests are reproducible.

    Instances For
      theorem TorchLean.ssl.vectorMaeMask_get_eq_if_selected_hidden (batch dataDim period offset : ) (x : Spec.Tensor Float (Spec.Shape.dim batch (Spec.Shape.dim dataDim Shape.scalar))) (bi : Fin batch) (j : Fin dataDim) :
      (Spec.get (Spec.get (vectorMaeMask batch dataDim period offset x) bi) j).toScalar = if vectorMaeHiddenMask dataDim period offset j = true then 0.0 else (Spec.get (Spec.get x bi) j).toScalar

      Coordinate-level bridge from the executable tensor mask to the finite mask used in the self-supervised theory files.

      For every batch row and feature coordinate, vectorMaeMask returns exactly zero on hidden coordinates and the original tensor value on visible coordinates.

      theorem TorchLean.ssl.vectorMaeMask_hidden_get_eq_zero (batch dataDim period offset : ) (x : Spec.Tensor Float (Spec.Shape.dim batch (Spec.Shape.dim dataDim Shape.scalar))) (bi : Fin batch) (j : Fin dataDim) (h : NN.MLTheory.SelfSupervised.selected (vectorMaeHiddenMask dataDim period offset) j) :
      (Spec.get (Spec.get (vectorMaeMask batch dataDim period offset x) bi) j).toScalar = 0.0

      Hidden feature coordinates are exactly zero after applying vectorMaeMask.

      theorem TorchLean.ssl.vectorMaeMask_visible_get_eq_input (batch dataDim period offset : ) (x : Spec.Tensor Float (Spec.Shape.dim batch (Spec.Shape.dim dataDim Shape.scalar))) (bi : Fin batch) (j : Fin dataDim) (h : ¬NN.MLTheory.SelfSupervised.selected (vectorMaeHiddenMask dataDim period offset) j) :
      (Spec.get (Spec.get (vectorMaeMask batch dataDim period offset x) bi) j).toScalar = (Spec.get (Spec.get x bi) j).toScalar

      Visible feature coordinates are preserved by vectorMaeMask.

      Build a compact MAE training sample from a vector batch.

      The model sees the masked vector and reconstructs the original vector. This is represented using TorchLean's existing supervised sample type because the "label" is derived from the input.

      Instances For
        theorem TorchLean.ssl.vectorMaeSample_input_eq_mask (batch dataDim period offset : ) (x : Spec.Tensor Float (Spec.Shape.dim batch (Spec.Shape.dim dataDim Shape.scalar))) :
        Sample.x (vectorMaeSample batch dataDim period offset x) = vectorMaeMask batch dataDim period offset x

        The executable vector MAE training input is exactly the masked tensor.

        This is the whole-tensor statement behind the coordinate theorems below. When the runtime training loop calls TorchLean.Sample.x, it receives this tensor and no other preprocessing is hidden in the sample wrapper.

        theorem TorchLean.ssl.vectorMaeSample_target_eq_source (batch dataDim period offset : ) (x : Spec.Tensor Float (Spec.Shape.dim batch (Spec.Shape.dim dataDim Shape.scalar))) :
        Sample.y (vectorMaeSample batch dataDim period offset x) = x

        The executable vector MAE training target is exactly the original tensor.

        Together with vectorMaeSample_input_eq_mask, this says the fixed-sample training call compares a model output against the unmasked source tensor.

        Tensor-to-theory bridge for predictive-view SSL #

        def TorchLean.ssl.vectorMaeSelectedIdxs (dataDim period offset : ) :
        List (Fin dataDim)

        The finite hidden-index list induced by the executable vector MAE mask.

        This is the serialization of the masked coordinate set used by the finite MAE/predictive-view objective. The tensor API uses the Boolean mask directly; the theory objective sums over a list.

        Instances For

          Extract one runtime tensor row as the finite patch batch used by the SSL theory layer.

          Instances For

            Extract one runtime prediction row as a finite prediction function.

            Instances For
              theorem TorchLean.ssl.vectorMaeSample_target_row_eq_source_row (batch dataDim period offset : ) (x : Spec.Tensor Float (Spec.Shape.dim batch (Spec.Shape.dim dataDim Shape.scalar))) (bi : Fin batch) :
              matrixRowAsPatchBatch batch dataDim (Sample.y (vectorMaeSample batch dataDim period offset x)) bi = matrixRowAsPatchBatch batch dataDim x bi

              The tensor MAE sample keeps the original row as the finite theory target.

              The target row is exactly the patch batch appearing in the finite MAE/predictive-view objective.

              theorem TorchLean.ssl.vectorMaeSample_input_hidden_get_eq_zero (batch dataDim period offset : ) (x : Spec.Tensor Float (Spec.Shape.dim batch (Spec.Shape.dim dataDim Shape.scalar))) (bi : Fin batch) (j : Fin dataDim) (h : NN.MLTheory.SelfSupervised.selected (vectorMaeHiddenMask dataDim period offset) j) :
              (Spec.get (Spec.get (Sample.x (vectorMaeSample batch dataDim period offset x)) bi) j).toScalar = 0.0

              The tensor MAE sample input has zero at every finite hidden coordinate.

              This is the executable masking invariant seen by the model before the theory objective asks it to predict those original target coordinates back.

              A single row of the executable vector MAE path instantiates the finite predictive-view contract.

              yhat is the model output tensor. After extracting row bi, the finite objective is precisely the MAE masked reconstruction loss over the selected hidden coordinates. This is the key bridge from Spec.Tensor implementation data to the SSL objective algebra.

              Instances For
                theorem TorchLean.ssl.vectorMaeRow_predictive_objective_eq_maeLoss (batch dataDim period offset : ) (x yhat : Spec.Tensor Float (Spec.Shape.dim batch (Spec.Shape.dim dataDim Shape.scalar))) (bi : Fin batch) (patchLoss : FloatFloat) :
                NN.MLTheory.SelfSupervised.predictiveViewObjective (vectorMaeRowPredictiveContract batch dataDim period offset x yhat bi patchLoss) = NN.MLTheory.SelfSupervised.maeLoss (vectorMaeSelectedIdxs dataDim period offset) (matrixRowAsPatchBatch batch dataDim x bi) (matrixRowAsPrediction batch dataDim yhat bi) patchLoss

                The extracted tensor-row predictive-view objective is exactly the finite MAE loss.

                This is the formal version of the implementation diagram:

                Spec.Tensor batch row → hidden-coordinate mask → model prediction row → masked reconstruction objective.

                def TorchLean.ssl.tensorPrefixMaeSample {source : Shape} (batch dataDim : ) (hData : dataDim source.size) (period offset : ) (x : Spec.Tensor Float (Spec.Shape.dim batch source)) :

                Build a compact MAE sample from any batched tensor source.

                The source can be an image tensor, spectrogram tensor, token-feature tensor, etc. This helper chooses a flattened prefix of each row, masks that prefix, and reconstructs the original prefix. A full ViT/patch MAE can replace this prefix projection with a patch embedding while keeping the same training idea.

                Instances For