Baum–Welch algorithm

TheoremPath weight as a product#✓fully proved

Let \(h\) be an HMM with weights in a commutative semiring, with initial weights \(\pi\), transition weights \(a\) and emission weights \(b\), and let \(x_0, x_1, \dots\) be observations. For every \(T\) and every state path \(z = (z_0, \dots, z_T)\), the path weight of \(z\) and \(x_0, \dots, x_T\) is

\[\pi(z_0) \prod_{t=0}^{T-1} a(z_t, z_{t+1}) \prod_{t=0}^{T} b(z_t, x_t).\]

theorem pathProb_eq_prod [CommSemiring R] (h : HMM S O R) (x : ℕ → O) :
    ∀ (T : ℕ) (z : Fin (T + 1) → S), pathProb h x T z =
      h.init (z 0) * (∏ t : Fin T, h.trans (z t.castSucc) (z t.succ)) *
        ∏ t : Fin (T + 1), h.emit (z t) (x t)

Uses 2 · Used by 8

Statement usesHidden Markov model · Joint weight of a state path and the observations

Used byThe ChromHMM update maximizes Q(· | θ) · Positivity of the ChromHMM joint weight · The ChromHMM update is a valid parameter · The Baum-Welch update maximizes the EM objective · One Baum-Welch step · The log path weight is linear in the path's counts · The log-likelihood is monotone along the Baum-Welch iterates · Each Baum-Welch step does not decrease the log-likelihood

StructureValid hidden Markov model parameters#✓fully proved

A hidden Markov model with finite state set \(S\), finite observation set \(O\) and real initial weights \(\pi\), transition weights \(a\) and emission weights \(b\) is valid when all its weights are strictly positive and form probability distributions: \(\pi(s) > 0\) for every \(s\) and \(\sum_{s} \pi(s) = 1\); \(a(s, s') > 0\) for all \(s, s'\) and \(\sum_{s'} a(s, s') = 1\) for every \(s\); and \(b(s, o) > 0\) for all \(s, o\) and \(\sum_{o} b(s, o) = 1\) for every \(s\).

structure Valid (h : HMM S O ℝ) : Prop where
  init_pos : ∀ s, 0 < h.init s
  init_sum : ∑ s, h.init s = 1
  trans_pos : ∀ s s', 0 < h.trans s s'
  trans_sum : ∀ s, ∑ s', h.trans s s' = 1
  emit_pos : ∀ s o, 0 < h.emit s o
  emit_sum : ∀ s, ∑ o, h.emit s o = 1

Uses 1 · Used by 20

Statement usesHidden Markov model

Used byThe ChromHMM update maximizes Q(· | θ) · Positivity of the ChromHMM joint weight · The log-likelihood is monotone along the ChromHMM iterates · Each ChromHMM step does not decrease the log-likelihood · The ChromHMM update is a valid parameter · Valid ChromHMM parameters give a valid HMM · Valid HMM built from a valid ChromHMM parameter · The Baum-Welch objective in terms of expected counts · The Baum-Welch update maximizes the EM objective · One Baum-Welch step · The expected emissions from forward-backward · The expected starts from forward-backward · The EM model of a hidden Markov model · The log path weight is linear in the path's counts · The Baum-Welch log-likelihood is the HMM log-likelihood · The log-likelihood is monotone along the Baum-Welch iterates · Each Baum-Welch step does not decrease the log-likelihood · The EM marginal of an HMM is its likelihood · The expected transitions from forward-backward · Valid HMMs

AbbreviationValid HMMs#✓fully proved

For finite sets \(S\) of states and \(O\) of observations, the valid HMMs are the HMMs with states \(S\), observations \(O\) and real weights whose initial weights are positive and sum to \(1\), whose transition weights out of each state are positive and sum to \(1\), and whose emission weights from each state are positive and sum to \(1\). They form the parameter space of Baum-Welch.

abbrev ValidHMM (S O : Type*) [Fintype S] [Fintype O] := {h : HMM S O ℝ // Valid h}

Uses 2 · Used by 23

Statement usesValid hidden Markov model parameters · Hidden Markov model

Used byThe ChromHMM update maximizes Q(· | θ) · Positivity of the ChromHMM joint weight · The log-likelihood is monotone along the ChromHMM iterates · Each ChromHMM step does not decrease the log-likelihood · The ChromHMM update is a valid parameter · Valid HMM built from a valid ChromHMM parameter · The Baum-Welch objective in terms of expected counts · The Baum-Welch update maximizes the EM objective · One Baum-Welch step · Expected emission counts · The expected emissions from forward-backward · Expected initial-state counts · The expected starts from forward-backward · The EM model of a hidden Markov model · The log path weight is linear in the path's counts · The Baum-Welch log-likelihood is the HMM log-likelihood · The log-likelihood is monotone along the Baum-Welch iterates · Each Baum-Welch step does not decrease the log-likelihood · The Baum-Welch M-step · The EM marginal of an HMM is its likelihood · Posterior weight of a state path · Expected transition count · The expected transitions from forward-backward

DefinitionThe EM model of a hidden Markov model#✓fully proved

Let \(S\) and \(O\) be finite sets and let \(T\) be a natural number. Let \(h\) be a valid hidden Markov model on states \(S\) and observations \(O\), with positive initial probabilities \(\pi_s\), transition probabilities \(a_{ss'}\) and emission probabilities \(b_{so}\), each distribution summing to one. The joint of its EM model at an observation sequence \(x = (x_0, x_1, \dots)\) in \(O\) and a state path \(z = (z_0, \dots, z_T)\) in \(S\) is the path weight \(p_h(x, z) = \pi_{z_0} b_{z_0 x_0} \prod_{t=1}^{T} a_{z_{t-1} z_t} b_{z_t x_t}\).

noncomputable def joint (h : ValidHMM S O) (x : ℕ → O) (z : Fin (T + 1) → S) : ℝ :=
  pathProb h.1 x T z

Uses 4 · Used by 13

Statement usesValid hidden Markov model parameters · Valid HMMs · Hidden Markov model · Joint weight of a state path and the observations

Used byThe ChromHMM update maximizes Q(· | θ) · ChromHMM joint weight of a state path and mark vectors · Positivity of the ChromHMM joint weight · The ChromHMM update is a valid parameter · The Baum-Welch objective in terms of expected counts · The Baum-Welch update maximizes the EM objective · One Baum-Welch step · The log path weight is linear in the path's counts · The Baum-Welch log-likelihood is the HMM log-likelihood · The log-likelihood is monotone along the Baum-Welch iterates · Each Baum-Welch step does not decrease the log-likelihood · The EM marginal of an HMM is its likelihood · Posterior weight of a state path

TheoremThe EM marginal of an HMM is its likelihood#✓fully proved

For every \(T\), every valid HMM \(h\) and every observation sequence \(x\), the marginal at \(h\) and \(x\) of the EM model of HMMs with state paths \((z_0, \dots, z_T)\), that is the sum over all such paths of the path weight of \(z\) and \(x\), equals the likelihood under \(h\) of the observations \(x_0, \dots, x_T\).

theorem marginal_joint (h : ValidHMM S O) (x : ℕ → O) :
    marginal (joint T) h x = likelihood h.1 x T

Uses 6

Statement usesMarginal of a latent-variable model · Valid hidden Markov model parameters · Valid HMMs · The EM model of a hidden Markov model · Hidden Markov model · Likelihood of the observations

DefinitionInitial-state indicator of a state path#✓fully proved

For a state path \(z = (z_0, \dots, z_T)\) and a state \(s\), the initial-state indicator is the real number \(1\) if \(z_0 = s\) and \(0\) otherwise.

def pInit (z : Fin (T + 1) → S) (s : S) : ℝ := if z 0 = s then 1 else 0

Used by 8

Used byThe ChromHMM update maximizes Q(· | θ) · The ChromHMM update is a valid parameter · The Baum-Welch objective in terms of expected counts · The Baum-Welch update maximizes the EM objective · One Baum-Welch step · Expected initial-state counts · The expected starts from forward-backward · The log path weight is linear in the path's counts

DefinitionTransition count of a state path#✓fully proved

For a state path \(z = (z_0, \dots, z_T)\) and states \(s, s'\), the transition count is the number of \(t \in \{0, \dots, T - 1\}\) with \(z_t = s\) and \(z_{t+1} = s'\), as a real number.

def pTrans (z : Fin (T + 1) → S) (s s' : S) : ℝ :=
  ∑ t : Fin T, if z t.castSucc = s ∧ z t.succ = s' then 1 else 0

Used by 8

Used byThe ChromHMM update maximizes Q(· | θ) · The ChromHMM update is a valid parameter · The Baum-Welch objective in terms of expected counts · The Baum-Welch update maximizes the EM objective · One Baum-Welch step · The log path weight is linear in the path's counts · Expected transition count · The expected transitions from forward-backward

DefinitionEmission count of a state path#✓fully proved

For a state path \(z = (z_0, \dots, z_T)\), observations \(x_0, x_1, \dots\), a state \(s\) and a symbol \(o\), the emission count is the number of times \(t \in \{0, \dots, T\}\) with \(z_t = s\) and \(x_t = o\), as a real number.

def pEmit (x : ℕ → O) (z : Fin (T + 1) → S) (s : S) (o : O) : ℝ :=
  ∑ t : Fin (T + 1), if z t = s ∧ x t = o then 1 else 0

Used by 9

Used byThe ChromHMM update maximizes Q(· | θ) · The ChromHMM update is a valid parameter · The factored update in posterior form · The Baum-Welch objective in terms of expected counts · The Baum-Welch update maximizes the EM objective · One Baum-Welch step · Expected emission counts · The expected emissions from forward-backward · The log path weight is linear in the path's counts

TheoremThe log path weight is linear in the path's counts#✓fully proved

Let \(S\) and \(O\) be finite sets, let \(T\) be a natural number, and let \(h\) be a valid hidden Markov model on states \(S\) and observations \(O\), with positive initial probabilities \(\pi_s\), transition probabilities \(a_{ss'}\) and emission probabilities \(b_{so}\), each distribution summing to one. For every observation sequence \(x = (x_0, x_1, \dots)\) in \(O\) and every state path \(z = (z_0, \dots, z_T)\) in \(S\), the path weight \(p_h(x, z) = \pi_{z_0} b_{z_0 x_0} \prod_{t=1}^{T} a_{z_{t-1} z_t} b_{z_t x_t}\) satisfies \(\log p_h(x, z) = \sum_{s} [z_0 = s] \log \pi_s + \sum_{s, s'} n_{ss'} \log a_{ss'} + \sum_{s, o} m_{so} \log b_{so}\), where \([z_0 = s]\) is \(1\) if \(z_0 = s\) and \(0\) otherwise, \(n_{ss'} = \#\{t < T : z_t = s,\ z_{t+1} = s'\}\) and \(m_{so} = \#\{t \le T : z_t = s,\ x_t = o\}\).

theorem log_joint (h : ValidHMM S O) (x : ℕ → O) (z : Fin (T + 1) → S) :
    log (joint T h x z) = ∑ s, pInit T z s * log (h.1.init s) +
      ∑ s, ∑ s', pTrans T z s s' * log (h.1.trans s s') +
      ∑ s, ∑ o, pEmit T x z s o * log (h.1.emit s o)

Uses 9 · Used by 1

Statement usesValid hidden Markov model parameters · Valid HMMs · The EM model of a hidden Markov model · Emission count of a state path · Initial-state indicator of a state path · Transition count of a state path · Hidden Markov model

Proof usesPath weight as a product · Joint weight of a state path and the observations

Used byThe Baum-Welch objective in terms of expected counts

DefinitionPosterior weight of a state path#✓fully proved

For a valid HMM \(h\), observation sequences \(x_0, \dots, x_{N-1}\), an index \(n < N\) and a state path \(z = (z_0, \dots, z_T)\), the posterior weight of \(z\) is the posterior of \(z\) given \(x_n\) at \(h\) in the EM model of HMMs: the path weight of \(z\) and \(x_n\) divided by the sum of the path weights of \(z'\) and \(x_n\) over all state paths \(z' = (z'_0, \dots, z'_T)\).

noncomputable def post (h : ValidHMM S O) (n : Fin N) (z : Fin (T + 1) → S) : ℝ :=
  posterior (joint T) h (xs n) z

Uses 3 · Used by 11

Statement usesPosterior of a latent-variable model · Valid HMMs · The EM model of a hidden Markov model

Used byThe ChromHMM update maximizes Q(· | θ) · The ChromHMM update is a valid parameter · The factored update in posterior form · The Baum-Welch update maximizes the EM objective · One Baum-Welch step · Expected emission counts · The expected emissions from forward-backward · Expected initial-state counts · The expected starts from forward-backward · Expected transition count · The expected transitions from forward-backward

DefinitionExpected initial-state counts#✓fully proved

Let \(S\) and \(O\) be finite sets, let \(T\) be a natural number, and let \(x_1, \dots, x_N\) be sequences of observations in \(O\). For a valid hidden Markov model \(h\) on states \(S\) and observations \(O\) and a state \(s\), the expected number of sequences starting in \(s\) is

\[I_s = \sum_{n=1}^{N} \sum_{z \,:\, z_0 = s} p_h(z \mid x_n),\]

where \(z\) ranges over the state paths \((z_0, \dots, z_T)\) in \(S\) and \(p_h(z \mid x_n)\) is the posterior of \(z\) given \(x_n\): the path weight of \(z\) and \(x_n\) under \(h\) divided by the total weight of all such paths.

noncomputable def initCount (h : ValidHMM S O) (s : S) : ℝ :=
  ∑ n, ∑ z, post T xs h n z * pInit T z s

Uses 3 · Used by 7

Statement usesValid HMMs · Initial-state indicator of a state path · Posterior weight of a state path

Used byThe ChromHMM update maximizes Q(· | θ) · The ChromHMM update is a valid parameter · The Baum-Welch objective in terms of expected counts · The Baum-Welch update maximizes the EM objective · One Baum-Welch step · The expected starts from forward-backward · The Baum-Welch M-step

DefinitionExpected transition count#✓fully proved

For a valid HMM \(h\), observation sequences \(x_0, \dots, x_{N-1}\) and states \(s, s'\), the expected transition count is \(\sum_{n < N} \sum_{z} p_h(z \mid x_n) \, c_{s s'}(z)\), where \(z\) ranges over the state paths \((z_0, \dots, z_T)\), \(p_h(z \mid x_n)\) is the posterior weight of \(z\) for \(x_n\), and \(c_{s s'}(z)\) is the number of \(t < T\) with \(z_t = s\) and \(z_{t+1} = s'\).

noncomputable def transCount (h : ValidHMM S O) (s s' : S) : ℝ :=
  ∑ n, ∑ z, post T xs h n z * pTrans T z s s'

Uses 3 · Used by 7

Statement usesValid HMMs · Transition count of a state path · Posterior weight of a state path

Used byThe ChromHMM update maximizes Q(· | θ) · The ChromHMM update is a valid parameter · The Baum-Welch objective in terms of expected counts · The Baum-Welch update maximizes the EM objective · One Baum-Welch step · The Baum-Welch M-step · The expected transitions from forward-backward

DefinitionExpected emission counts#✓fully proved

Let \(S\) and \(O\) be finite sets, let \(T\) be a natural number, and let \(x_1, \dots, x_N\) be sequences \(x_n = (x_{n,0}, x_{n,1}, \dots)\) of observations in \(O\). For a valid hidden Markov model \(h\) on states \(S\) and observations \(O\), a state \(s\) and an observation \(o\), the expected number of emissions of \(o\) from \(s\) is

\[E_{so} = \sum_{n=1}^{N} \sum_{z} p_h(z \mid x_n) \, \#\{t \le T : z_t = s,\ x_{n,t} = o\},\]

where \(z\) ranges over the state paths \((z_0, \dots, z_T)\) in \(S\) and \(p_h(z \mid x_n)\) is the posterior of \(z\) given \(x_n\): the path weight of \(z\) and \(x_n\) under \(h\) divided by the total weight of all such paths.

noncomputable def emitCount (h : ValidHMM S O) (s : S) (o : O) : ℝ :=
  ∑ n, ∑ z, post T xs h n z * pEmit T (xs n) z s o

Uses 3 · Used by 11

Statement usesValid HMMs · Emission count of a state path · Posterior weight of a state path

Used byThe ChromHMM update maximizes Q(· | θ) · The ChromHMM M-step · The ChromHMM update is a valid parameter · Expected number of bins in a state with a mark present · The factored update in posterior form · Expected number of bins in a state with a mark absent · The Baum-Welch objective in terms of expected counts · The Baum-Welch update maximizes the EM objective · One Baum-Welch step · The expected emissions from forward-backward · The Baum-Welch M-step

DefinitionThe Baum-Welch M-step#✓fully proved

Let \(h\) be a valid HMM with finite state set \(S\) and finite observation set \(O\), let \(x_0, \dots, x_{N-1}\) be observation sequences, and consider state paths \((z_0, \dots, z_T)\). Write \(I(s)\), \(A(s, s')\) and \(E(s, o)\) for the expected numbers, under the posterior of \(h\) and summed over the sequences, of sequences starting in \(s\), of transitions \(s \to s'\) and of emissions of \(o\) from \(s\). The M-step is the HMM with real weights whose initial weight of \(s\) is \(I(s) / N\), whose transition weight from \(s\) to \(s'\) is \(A(s, s') / \sum_{s''} A(s, s'')\), and whose emission weight of \(o\) from \(s\) is \(E(s, o) / \sum_{o'} E(s, o')\) (a quotient by \(0\) is read as \(0\)).

noncomputable def mStep (h : ValidHMM S O) : HMM S O ℝ where
  init s := initCount T xs h s / N
  trans s s' := transCount T xs h s s' / ∑ s'', transCount T xs h s s''
  emit s o := emitCount T xs h s o / ∑ o', emitCount T xs h s o'

Uses 5 · Used by 2

Statement usesValid HMMs · Expected emission counts · Expected initial-state counts · Expected transition count · Hidden Markov model

Used byThe ChromHMM M-step · One Baum-Welch step

TheoremThe Baum-Welch objective in terms of expected counts#✓fully proved

Let \(S\) and \(O\) be finite sets, let \(T\) be a natural number, and let \(x_1, \dots, x_N\) be sequences \(x_n = (x_{n,0}, x_{n,1}, \dots)\) of observations in \(O\). For a valid hidden Markov model \(h\) on states \(S\) and observations \(O\) (positive initial, transition and emission probabilities, each distribution summing to one), write \(p_h(x, z)\) for the path weight of the observations \(x\) and a state path \(z = (z_0, \dots, z_T)\) (the joint of the EM model of \(h\)) and \(p_h(z \mid x) = p_h(x, z) / \sum_{z'} p_h(x, z')\) for the posterior of the path, the sums ranging over all paths \(z : \{0, \dots, T\} \to S\). Let \(I_s = \sum_n \sum_{z \,:\, z_0 = s} p_h(z \mid x_n)\), \(A_{ss'} = \sum_n \sum_z p_h(z \mid x_n) \, \#\{t < T : z_t = s,\ z_{t+1} = s'\}\) and \(E_{so} = \sum_n \sum_z p_h(z \mid x_n) \, \#\{t \le T : z_t = s,\ x_{n,t} = o\}\) be the expected counts of initial states, transitions and emissions. Then for every valid hidden Markov model \(h'\) with initial probabilities \(\pi'_s\), transition probabilities \(a'_{ss'}\) and emission probabilities \(b'_{so}\), the EM objective \(Q(h' \mid h) = \sum_n \sum_z p_h(z \mid x_n) \log p_{h'}(x_n, z)\) equals \(\sum_{s} I_s \log \pi'_s + \sum_{s, s'} A_{ss'} \log a'_{ss'} + \sum_{s, o} E_{so} \log b'_{so}\).

theorem emQ_eq (h' h : ValidHMM S O) :
    emQ (joint T) xs h' h = ∑ s, initCount T xs h s * log (h'.1.init s) +
      ∑ s, ∑ s', transCount T xs h s s' * log (h'.1.trans s s') +
      ∑ s, ∑ o, emitCount T xs h s o * log (h'.1.emit s o)

Uses 13 · Used by 2

Statement usesThe EM objective · Valid hidden Markov model parameters · Valid HMMs · Expected emission counts · Expected initial-state counts · The EM model of a hidden Markov model · Expected transition count · Hidden Markov model

Proof usesPosterior of a latent-variable model · The log path weight is linear in the path's counts · Emission count of a state path · Initial-state indicator of a state path · Transition count of a state path

Used byThe ChromHMM update maximizes Q(· | θ) · The Baum-Welch update maximizes the EM objective

StructureData rich enough for the Baum-Welch M-step#✓fully proved

Observation sequences \(x_0, \dots, x_{N-1}\) over a symbol set \(O\) are rich for state paths \((z_0, \dots, z_T)\) when \(N > 0\), \(T > 0\), and every symbol \(o \in O\) is observed, that is \(x_n(t) = o\) for some \(n < N\) and some \(t \le T\).

These are the data on which the M-step gives a valid HMM.

structure Rich (xs : Fin N → ℕ → O) : Prop where
  pos : 0 < N
  len : 0 < T
  covers : ∀ o, ∃ n, ∃ t : Fin (T + 1), xs n t = o

Used by 4

Used byThe Baum-Welch update maximizes the EM objective · One Baum-Welch step · The log-likelihood is monotone along the Baum-Welch iterates · Each Baum-Welch step does not decrease the log-likelihood

DefinitionOne Baum-Welch step#✓fully proved

Let \(S\) and \(O\) be finite sets, let \(T \ge 1\), and let \(x_1, \dots, x_N\) with \(N \ge 1\) be sequences \(x_n = (x_{n,0}, x_{n,1}, \dots)\) of observations in \(O\) such that every \(o \in O\) equals \(x_{n,t}\) for some \(n\) and some \(t \le T\). For a valid hidden Markov model \(h\) on states \(S\) and observations \(O\) (positive initial, transition and emission probabilities, each distribution summing to one), the Baum-Welch step maps \(h\) to the hidden Markov model with initial probabilities \(I_s / N\), transition probabilities \(A_{ss'} / \sum_{s''} A_{ss''}\) and emission probabilities \(E_{so} / \sum_{o'} E_{so'}\). Here \(I_s\), \(A_{ss'}\) and \(E_{so}\) are the expected numbers of initial states equal to \(s\), of transitions from \(s\) to \(s'\) at times \(t < T\), and of emissions of \(o\) from \(s\) at times \(t \le T\), summed over \(n\) under the posterior of \(h\) over state paths \((z_0, \dots, z_T)\) given \(x_n\). On such data this hidden Markov model is again valid.

noncomputable def emStep (hx : Rich T xs) (h : ValidHMM S O) : ValidHMM S O :=
  ⟨mStep T xs h, mStep_valid hx h⟩

Uses 18 · Used by 3

Statement usesPosteriors are probability distributions · Marginal of a latent-variable model · Posterior of a latent-variable model · Data rich enough for the Baum-Welch M-step · Valid hidden Markov model parameters · Valid HMMs · Expected emission counts · Expected initial-state counts · The EM model of a hidden Markov model · The Baum-Welch M-step · Emission count of a state path · Initial-state indicator of a state path · Transition count of a state path · Path weight as a product · Posterior weight of a state path · Expected transition count · Hidden Markov model · Joint weight of a state path and the observations

Used byThe Baum-Welch update maximizes the EM objective · The log-likelihood is monotone along the Baum-Welch iterates · Each Baum-Welch step does not decrease the log-likelihood

TheoremThe Baum-Welch update maximizes the EM objective#✓fully proved

Let \(S\) and \(O\) be finite sets, let \(T \ge 1\), and let \(x_1, \dots, x_N\) with \(N \ge 1\) be sequences \(x_n = (x_{n,0}, x_{n,1}, \dots)\) of observations in \(O\) such that every \(o \in O\) equals \(x_{n,t}\) for some \(n\) and some \(t \le T\). Consider the EM model of a hidden Markov model on states \(S\) and observations \(O\) whose latent variable is the state path \(z = (z_0, \dots, z_T)\) and whose joint \(p_h(x, z)\) is the path weight, with EM objective \(Q(h' \mid h) = \sum_n \sum_z p_h(z \mid x_n) \log p_{h'}(x_n, z)\), where \(p_h(z \mid x) = p_h(x, z) / \sum_{z'} p_h(x, z')\) is the posterior of the path. Then for all valid hidden Markov models \(h\) and \(h'\) (positive initial, transition and emission probabilities, each distribution summing to one), \(Q(h' \mid h) \le Q(\bar h \mid h)\), where \(\bar h\) is the Baum-Welch step applied to \(h\) on these data.

theorem emQ_le_emStep (hx : Rich T xs) (h' h : ValidHMM S O) :
    emQ (joint T) xs h' h ≤ emQ (joint T) xs (emStep T xs hx h) h

Uses 21 · Used by 2

Statement usesThe EM objective · Data rich enough for the Baum-Welch M-step · Valid HMMs · One Baum-Welch step · The EM model of a hidden Markov model

Proof usesThe weighted log-likelihood is bounded by its value at the normalized counts · Posteriors are probability distributions · Marginal of a latent-variable model · Posterior of a latent-variable model · Valid hidden Markov model parameters · The Baum-Welch objective in terms of expected counts · Expected emission counts · Expected initial-state counts · Emission count of a state path · Initial-state indicator of a state path · Transition count of a state path · Path weight as a product · Posterior weight of a state path · Expected transition count · Hidden Markov model · Joint weight of a state path and the observations

Used byThe log-likelihood is monotone along the Baum-Welch iterates · Each Baum-Welch step does not decrease the log-likelihood

TheoremEach Baum-Welch step does not decrease the log-likelihood#✓fully proved

Let \(S\) and \(O\) be finite sets, let \(T \ge 1\), and let \(x_1, \dots, x_N\) with \(N \ge 1\) be sequences \(x_n = (x_{n,0}, x_{n,1}, \dots)\) of observations in \(O\) such that every \(o \in O\) equals \(x_{n,t}\) for some \(n\) and some \(t \le T\). For every valid hidden Markov model \(h\) on states \(S\) and observations \(O\), \(\ell(h) \le \ell(\bar h)\), where \(\bar h\) is the Baum-Welch step applied to \(h\) on these data and \(\ell(h) = \sum_{n=1}^{N} \log \sum_z p_h(x_n, z)\) is the log-likelihood of the EM model of \(h\), the sum ranging over state paths \(z = (z_0, \dots, z_T)\) and \(p_h(x, z)\) being the path weight.

theorem logLik_le_emStep (hx : Rich T xs) (h : ValidHMM S O) :
    logLik (joint T) xs h ≤ logLik (joint T) xs (emStep T xs hx h)

Uses 11

Statement usesLog-likelihood of a latent-variable model · Data rich enough for the Baum-Welch M-step · Valid HMMs · One Baum-Welch step · The EM model of a hidden Markov model

Proof usesThe EM theorem · Valid hidden Markov model parameters · The Baum-Welch update maximizes the EM objective · Path weight as a product · Hidden Markov model · Joint weight of a state path and the observations

TheoremThe log-likelihood is monotone along the Baum-Welch iterates#✓fully proved

Let \(S\) and \(O\) be finite sets, let \(T \ge 1\), and let \(x_1, \dots, x_N\) with \(N \ge 1\) be sequences \(x_n = (x_{n,0}, x_{n,1}, \dots)\) of observations in \(O\) such that every \(o \in O\) equals \(x_{n,t}\) for some \(n\) and some \(t \le T\). Let \(h_0\) be a valid hidden Markov model on states \(S\) and observations \(O\) and let \(h_t\) be the result of \(t\) Baum-Welch steps from \(h_0\) on these data. Then \(t \mapsto \ell(h_t)\) is monotone (nondecreasing in \(t \in \mathbb{N}\)), where \(\ell(h) = \sum_{n=1}^{N} \log \sum_z p_h(x_n, z)\) is the log-likelihood of the EM model of \(h\), the sum ranging over state paths \(z = (z_0, \dots, z_T)\) and \(p_h(x, z)\) being the path weight.

theorem logLik_iterate_emStep_monotone (hx : Rich T xs) (h₀ : ValidHMM S O) :
    Monotone fun t => logLik (joint T) xs ((emStep T xs hx)^[t] h₀)

Uses 11

Statement usesLog-likelihood of a latent-variable model · Data rich enough for the Baum-Welch M-step · Valid HMMs · One Baum-Welch step · The EM model of a hidden Markov model

Proof usesEM iterates have monotone likelihood · Valid hidden Markov model parameters · The Baum-Welch update maximizes the EM objective · Path weight as a product · Hidden Markov model · Joint weight of a state path and the observations

TheoremThe Baum-Welch log-likelihood is the HMM log-likelihood#✓fully proved

Let \(S\) and \(O\) be finite sets, let \(T\) be a natural number, and let \(x_1, \dots, x_N\) be sequences \(x_n = (x_{n,0}, x_{n,1}, \dots)\) of observations in \(O\). For every valid hidden Markov model \(h\) on states \(S\) and observations \(O\), the log-likelihood of its EM model (latent state paths \((z_0, \dots, z_T)\), joint the path weight) on these data equals \(\sum_{n=1}^{N} \log L_h(x_n)\), where \(L_h(x_n)\) is the likelihood of the observations \(x_{n,0}, \dots, x_{n,T}\) under \(h\): the total path weight over all state paths \((z_0, \dots, z_T)\).

theorem logLik_eq (h : ValidHMM S O) :
    logLik (joint T) xs h = ∑ n, log (likelihood h.1 (xs n) T)

Uses 6

Statement usesLog-likelihood of a latent-variable model · Valid hidden Markov model parameters · Valid HMMs · The EM model of a hidden Markov model · Hidden Markov model · Likelihood of the observations

TheoremPairwise path sums with a fixed endpoint#✓fully proved

Let \(h\) be a hidden Markov model with finite state set \(S\), transition weights \(a\) and emission weights \(b\) in a semiring, and let \(x\) be an observation sequence. For all \(k, t \in \mathbb{N}\) and states \(s, s', u\), the sum of the path weights of the state paths \(z_0, \dots, z_{t + 1 + k}\) with \(z_t = s\), \(z_{t + 1} = s'\) and \(z_{t + 1 + k} = u\) equals \(\alpha_t(s)\, a(s, s')\, b(s', x(t + 1))\, B_{k, t + 1}(s', u)\), where \(\alpha_t(s)\) is the forward variable and \(B_{k, t + 1}(s', u)\) is the bridge weight of the paths from the state \(s'\) at time \(t + 1\) to the state \(u\) at time \(t + 1 + k\).

theorem sum_pathProb_ite_pair : ∀ (k t : ℕ) (s s' u : S),
    ∑ z : Fin (t + 1 + k + 1) → S,
      (if z ⟨t, by omega⟩ = s ∧ z ⟨t + 1, by omega⟩ = s' ∧ z (Fin.last (t + 1 + k)) = u then
        pathProb h x (t + 1 + k) z else 0) =
      forward h x t s * h.trans s s' * h.emit s' (x (t + 1)) * bridge h x k (t + 1) s' u

Uses 5 · Used by 1

Statement usesHidden Markov model · Bridge weights of a hidden Markov model · Forward variables of a hidden Markov model · Joint weight of a state path and the observations

Proof usesThe forward variables are path sums

Used byPairwise forward-backward

DefinitionPairwise state marginal of a hidden Markov model#✓fully proved

For a hidden Markov model with finite state set \(S\), an observation sequence \(x\), times \(t, k \in \mathbb{N}\) and states \(s, s'\), the pairwise marginal is the joint weight of the observations \(x(0), \dots, x(t + 1 + k)\) and the transition \(s \to s'\) from time \(t\) to time \(t + 1\): the sum of the path weights of all state paths \(z_0, \dots, z_{t + 1 + k}\) with \(z_t = s\) and \(z_{t + 1} = s'\).

def pairMarg (t k : ℕ) (s s' : S) : R :=
  ∑ z : Fin (t + 1 + k + 1) → S,
    if z ⟨t, by omega⟩ = s ∧ z ⟨t + 1, by omega⟩ = s' then pathProb h x (t + 1 + k) z else 0

Uses 2 · Used by 2

Statement usesHidden Markov model · Joint weight of a state path and the observations

Used byPairwise forward-backward · The expected transitions from forward-backward

TheoremPairwise forward-backward#✓fully proved

Let \(h\) be a hidden Markov model with finite state set \(S\), transition weights \(a\) and emission weights \(b\) in a semiring, and let \(x\) be an observation sequence. For all \(t, k \in \mathbb{N}\) and states \(s, s'\), the joint weight of the observations \(x(0), \dots, x(t + 1 + k)\) and the transition \(s \to s'\) from time \(t\) to time \(t + 1\) equals \(\alpha_t(s)\, a(s, s')\, b(s', x(t + 1))\, \beta_{k, t + 1}(s')\), where \(\alpha_t(s)\) is the forward variable and \(\beta_{k, t + 1}(s')\) is the backward variable, the weight of the observations \(x(t + 2), \dots, x(t + 1 + k)\) given the state \(s'\) at time \(t + 1\).

theorem pairMarg_eq (t k : ℕ) (s s' : S) :
    pairMarg h x t k s s' =
      forward h x t s * h.trans s s' * h.emit s' (x (t + 1)) * backward h x k (t + 1) s'

Uses 8 · Used by 1

Statement usesHidden Markov model · Backward variables of a hidden Markov model · Forward variables of a hidden Markov model · Pairwise state marginal of a hidden Markov model

Proof usesBridge weights of a hidden Markov model · Joint weight of a state path and the observations · Bridge weights sum to the backward variable · Pairwise path sums with a fixed endpoint

Used byThe expected transitions from forward-backward

TheoremThe expected starts from forward-backward#✓fully proved

Let \(h\) be a valid hidden Markov model with finite state set \(S\) and finite observation set \(O\), let \(T \in \mathbb{N}\), and let \(x_0, \dots, x_{N-1}\) be observation sequences. For a sequence \(x_n\) write \(\alpha^n_0(s)\) for its forward variable at time \(0\) and state \(s\), \(\beta^n_{T,0}(s)\) for its backward variable from time \(0\) with \(T\) remaining steps (the weight of the observations \(x_n(1), \dots, x_n(T)\) given the state \(s\) at time \(0\)), and \(L_n\) for the likelihood of \(x_n(0), \dots, x_n(T)\). Then for every state \(s\), the expected number of sequences whose state path of length \(T + 1\) starts in \(s\), under the posterior of \(h\), is \(\sum_{n < N} \alpha^n_0(s)\, \beta^n_{T,0}(s) / L_n\).

theorem initCount_eq (h : ValidHMM S O) (s : S) :
    initCount T xs h s =
      ∑ n, forward h.1 (xs n) 0 s * backward h.1 (xs n) T 0 s / likelihood h.1 (xs n) T

Uses 12

Statement usesValid hidden Markov model parameters · Valid HMMs · Expected initial-state counts · Hidden Markov model · Backward variables of a hidden Markov model · Forward variables of a hidden Markov model · Likelihood of the observations

Proof usesInitial-state indicator of a state path · Posterior weight of a state path · Joint weight of a state path and the observations · Joint weight of the observations and a state · Forward-backward identity

TheoremThe expected emissions from forward-backward#✓fully proved

Let \(h\) be a valid hidden Markov model with finite state set \(S\) and finite observation set \(O\), let \(T \in \mathbb{N}\), and let \(x_0, \dots, x_{N-1}\) be observation sequences. For a sequence \(x_n\) write \(\alpha^n_t(s)\) for its forward variable at time \(t\) and state \(s\), \(\beta^n_{k,t}(s)\) for its backward variable (the weight of the observations \(x_n(t + 1), \dots, x_n(t + k)\) given the state \(s\) at time \(t\)), and \(L_n\) for the likelihood of \(x_n(0), \dots, x_n(T)\). Then for every state \(s\) and observation \(o\), the expected number of emissions of \(o\) from \(s\) along state paths of length \(T + 1\), summed over the sequences under the posterior of \(h\), is \(\sum_{n < N} \sum_{t \le T,\ x_n(t) = o} \alpha^n_t(s)\, \beta^n_{T - t, t}(s) / L_n\).

theorem emitCount_eq (h : ValidHMM S O) (s : S) (o : O) :
    emitCount T xs h s o = ∑ n, ∑ t : Fin (T + 1), if xs n t = o then
      forward h.1 (xs n) t s * backward h.1 (xs n) (T - t) t s / likelihood h.1 (xs n) T
      else 0

Uses 12

Statement usesValid hidden Markov model parameters · Valid HMMs · Expected emission counts · Hidden Markov model · Backward variables of a hidden Markov model · Forward variables of a hidden Markov model · Likelihood of the observations

Proof usesEmission count of a state path · Posterior weight of a state path · Joint weight of a state path and the observations · Joint weight of the observations and a state · Forward-backward identity

TheoremThe expected transitions from forward-backward#✓fully proved

Let \(h\) be a valid hidden Markov model with finite state set \(S\), finite observation set \(O\), transition weights \(a\) and emission weights \(b\), let \(T \in \mathbb{N}\), and let \(x_0, \dots, x_{N-1}\) be observation sequences. For a sequence \(x_n\) write \(\alpha^n_t(s)\) for its forward variable at time \(t\) and state \(s\), \(\beta^n_{k,t}(s)\) for its backward variable (the weight of the observations \(x_n(t + 1), \dots, x_n(t + k)\) given the state \(s\) at time \(t\)), and \(L_n\) for the likelihood of \(x_n(0), \dots, x_n(T)\). Then for all states \(s, s'\), the expected number of transitions \(s \to s'\) along state paths of length \(T + 1\), summed over the sequences under the posterior of \(h\), is \(\sum_{n < N} \sum_{t < T} \alpha^n_t(s)\, a(s, s')\, b(s', x_n(t + 1))\, \beta^n_{T - t - 1, t + 1}(s') / L_n\).

Each summand is Rabiner's \(\xi_t(s, s')\) for the sequence \(x_n\).

theorem transCount_eq (h : ValidHMM S O) (s s' : S) :
    transCount T xs h s s' = ∑ n, ∑ t : Fin T,
      forward h.1 (xs n) t s * h.1.trans s s' * h.1.emit s' (xs n (t + 1)) *
        backward h.1 (xs n) (T - t - 1) (t + 1) s' / likelihood h.1 (xs n) T

Uses 12

Statement usesValid hidden Markov model parameters · Valid HMMs · Expected transition count · Hidden Markov model · Backward variables of a hidden Markov model · Forward variables of a hidden Markov model · Likelihood of the observations

Proof usesTransition count of a state path · Posterior weight of a state path · Pairwise state marginal of a hidden Markov model · Pairwise forward-backward · Joint weight of a state path and the observations

27 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.