TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Spec.Module.Hmm

HMM adapters as Spec.Modules #

The HMM spec model (NN/Spec/Models/Hmm.lean) uses discrete observations (Fin nObservations).

For composition and examples, it is sometimes convenient to accept a tensor of scores/probabilities over the observation alphabet and decode each timestep via argmax. The wrappers in this file provide that bridge and package the resulting behavior as Spec.Modules.

source
def Spec.Module.decodeObservation {α : Type} [TorchLean.Storage α] [Context α] {nObservations : ℕ} (hObservations : nObservations > 0) (scores : TorchLean.Tensor α [nObservations]) :
Fin nObservations

Decode a single observation vector into a discrete symbol by taking argmax.

Instances For
    source
    def Spec.Module.decodeObservations {α : Type} [TorchLean.Storage α] [Context α] {seqLen nObservations : ℕ} (hObservations : nObservations > 0) (scores : TorchLean.Tensor α [seqLen, nObservations]) :
    TorchLean.Tensor (Fin nObservations) [seqLen]

    Convert a tensor of per-symbol scores/probabilities into a discrete observation sequence by decoding each timestep with argmax.

    Instances For
      source
      def Spec.Module.hmm {α : Type} [TorchLean.Storage α] [Context α] {nStates nObservations : ℕ} (hObservations : nObservations > 0) (m : HMMSpec α nStates nObservations) :
      Module α [nObservations] [nStates]

      A one-step HMM module: map an observation distribution to a filtered state distribution.

      Instances For
        source
        def Spec.Module.forwardMessages {α : Type} [TorchLean.Storage α] [Context α] {nStates nObservations length : ℕ} (m : HMMSpec α nStates nObservations) (observations : ObservationSeq nObservations length) :
        TorchLean.Tensor (TorchLean.Tensor α [nStates]) [length]

        Forward messages α_t for each timestep (scaled).

        Instances For
          source
          def Spec.Module.hmmSequence {α : Type} [TorchLean.Storage α] [Context α] {seqLen nStates nObservations : ℕ} (hObservations : nObservations > 0) (m : HMMSpec α nStates nObservations) :
          Module α [seqLen, nObservations] [seqLen, nStates]

          Sequence module: compute forward messages α_t for each timestep.

          Instances For
            source
            def Spec.Module.hmmPrefixLikelihoods {α : Type} [TorchLean.Storage α] [Context α] {seqLen nStates nObservations : ℕ} (hObservations : nObservations > 0) (m : HMMSpec α nStates nObservations) :
            Module α [seqLen, nObservations] [seqLen]

            Sequence module: compute prefix likelihoods p(o₀:t) for each timestep t.

            The scaled forward trace is computed once. Each prefix multiplies its scale factors in sequence order, starting from 1, as in hmmForwardSpec for a nonempty sequence.

            Instances For
              source
              def Spec.Module.hmmStateProbabilities {α : Type} [TorchLean.Storage α] [Context α] {seqLen nStates nObservations : ℕ} (hObservations : nObservations > 0) (m : HMMSpec α nStates nObservations) :
              Module α [seqLen, nObservations] [seqLen, nStates]

              Sequence module: normalize each scaled forward message again by its computed total.

              Rounded messages need not sum to exactly 1. This second pass divides each entry by that total; hmmSequence exposes the original messages without this extra division.

              Instances For
                source
                def Spec.Module.hmmIndependent {α : Type} [TorchLean.Storage α] [Context α] {seqLen nStates nObservations : ℕ} (hObservations : nObservations > 0) (m : HMMSpec α nStates nObservations) :
                Module α [seqLen, nObservations] [seqLen, nStates]

                Apply hmm independently at each timestep, using the initial distribution for every row.

                Each row is decoded with argmax, as in the one-step module. The output contains filtered state probabilities, with the same totalization for impossible observations as hmm.

                Instances For