Conditional random fields

StructureLinear-chain conditional random field#✓fully proved

Let \(S\) be a type of states, \(O\) a type of inputs and \(R\) a type of weights with a zero and a relation \(\le\). A linear-chain conditional random field consists of a unary potential \(\phi(x, t, s) \in R\) and a transition potential \(\psi(x, t, s, s') \in R\) from \(s\) to \(s'\), given for every observation sequence \(x \colon \mathbb{N} \to O\), every position \(t \in \mathbb{N}\) and all states \(s, s' \in S\), such that \(0 \le \phi(x, t, s)\) and \(0 \le \psi(x, t, s, s')\) always hold.

Both potentials see the whole, possibly infinite, observation sequence \(x\), so path weights condition on all of \(x\), as the conditional probability \(p(y \mid x)\) of a label sequence \(y\) does in the standard definition. Nonnegativity makes the potentials unnormalized probabilities.

structure ChainCRF (S O R : Type*) [Zero R] [LE R] where
  /-- The unary potential of a state at a position, as a function of the whole
  observation sequence. -/
  unary : (ℕ → O) → ℕ → S → R
  /-- The transition potential from the first state to the second at a step, as a function
  of the whole observation sequence (so edge features may depend jointly on the two
  states, the full input, and the position). -/
  trans : (ℕ → O) → ℕ → S → S → R
  /-- Unary potentials are nonnegative. -/
  unary_nonneg : ∀ (x : ℕ → O) (t : ℕ) (s : S), 0 ≤ unary x t s
  /-- Transition potentials are nonnegative. -/
  trans_nonneg : ∀ (x : ℕ → O) (t : ℕ) (s s' : S), 0 ≤ trans x t s s'

Used by 24

Used byBackpointer of the tabulated CRF Viterbi algorithm · Backtracked path of the tabulated CRF Viterbi algorithm · Conditional probability of a label path in a chain CRF · Conditional probabilities of a chain CRF are nonnegative · The Viterbi path of a chain CRF · The Viterbi variables of a chain CRF are attained · Forward variables of a chain CRF · The forward variables are path weights · One step of the tabulated CRF forward algorithm · Tabulated CRF forward algorithm · The chain CRF of a hidden Markov model · The chain CRF of a hidden Markov model has the same path weights · Partition function of a chain CRF · The forward algorithm computes the partition function · The tabulated forward algorithm for chain CRFs · Weight of a label path in a chain CRF · The backtracked path of a chain CRF attains the Viterbi variable · The Viterbi path of a chain CRF has maximal weight · Path weights of a chain CRF are bounded by the Viterbi variables · The conditional probabilities sum to \(1\) · Viterbi computes the MAP value of a chain CRF · The Viterbi variables of a chain CRF · One step of the tabulated Viterbi recursion for a chain CRF · The tabulated Viterbi variables of a chain CRF

DefinitionWeight of a label path in a chain CRF#✓fully proved

For a chain conditional random field with weights in a semiring, unary potentials \(u_t(s)\) and transition potentials \(\tau_t(s, s')\) given the observation stream \(x\), the unnormalized weight of a label path \(z = (z_0, \dots, z_t)\) is

\[w_t(z) = u_0(z_0) \prod_{i=1}^{t} \tau_{i-1}(z_{i-1}, z_i)\, u_i(z_i),\]

with the factors multiplied from left to right in increasing order of \(i\).

def pathWeight : (t : ℕ) → (Fin (t + 1) → S) → R
  | 0, z => c.unary x 0 (z 0)
  | t + 1, z => pathWeight t (Fin.init z) * c.trans x t (z (Fin.last t).castSucc)
      (z (Fin.last (t + 1))) * c.unary x (t + 1) (z (Fin.last (t + 1)))

Uses 1 · Used by 12

Statement usesLinear-chain conditional random field

Used byConditional probability of a label path in a chain CRF · Conditional probabilities of a chain CRF are nonnegative · The Viterbi variables of a chain CRF are attained · The forward variables are path weights · The chain CRF of a hidden Markov model has the same path weights · Partition function of a chain CRF · The forward algorithm computes the partition function · The backtracked path of a chain CRF attains the Viterbi variable · The Viterbi path of a chain CRF has maximal weight · Path weights of a chain CRF are bounded by the Viterbi variables · The conditional probabilities sum to \(1\) · Viterbi computes the MAP value of a chain CRF

DefinitionPartition function of a chain CRF#✓fully proved

For a chain conditional random field with a finite set of states and weights in a semiring, and an observation stream \(x\), the partition function at time \(t\) is \(Z_t = \sum_z w_t(z)\), the total weight of all label paths \(z\) of length \(t + 1\), where \(w_t(z)\) is the unnormalized weight of \(z\) given \(x\).

def partition (t : ℕ) : R := ∑ z : Fin (t + 1) → S, pathWeight c x t z

Uses 2 · Used by 4

Statement usesLinear-chain conditional random field · Weight of a label path in a chain CRF

Used byConditional probability of a label path in a chain CRF · Conditional probabilities of a chain CRF are nonnegative · The forward algorithm computes the partition function · The conditional probabilities sum to \(1\)

DefinitionForward variables of a chain CRF#✓fully proved

For a chain conditional random field with a finite set of states, weights in a semiring, unary potentials \(u_t(s)\) and transition potentials \(\tau_t(s', s)\) given the observation stream \(x\), the forward variables are defined by \(\alpha_0(s) = u_0(s)\) and \(\alpha_{t+1}(s) = \left(\sum_{s'} \alpha_t(s')\, \tau_t(s', s)\right) u_{t+1}(s)\), the sum running over all states \(s'\).

The forward variable \(\alpha_t(s)\) is the total weight of the label paths of length \(t + 1\) ending in \(s\).

def forward : ℕ → S → R
  | 0, s => c.unary x 0 s
  | t + 1, s => (∑ s', forward t s' * c.trans x t s' s) * c.unary x (t + 1) s

Uses 1 · Used by 2

Statement usesLinear-chain conditional random field

Used byThe forward variables are path weights · The forward algorithm computes the partition function

TheoremThe forward variables are path weights#✓fully proved

Let \(c\) be a chain CRF with a finite set of states \(S\) and weights in a semiring \(R\) carrying a relation \(\le\), and let \(x\) be an observation sequence. For every \(t \in \mathbb{N}\) and every state \(s \in S\), the forward variable \(\alpha_t(s)\) equals the total path weight of the label paths \(z = (z_0, \dots, z_t) \in S^{t+1}\) that end in \(z_t = s\):

\[\alpha_t(s) = \sum_{z \in S^{t+1},\ z_t = s} w_t(z),\]

where \(w_t(z)\) is the path weight of \(z\).

theorem forward_eq [DecidableEq S] : ∀ (t : ℕ) (s : S),
    forward c x t s = ∑ z : Fin (t + 1) → S,
      if z (Fin.last t) = s then pathWeight c x t z else 0

Uses 3 · Used by 1

Statement usesLinear-chain conditional random field · Forward variables of a chain CRF · Weight of a label path in a chain CRF

Used byThe forward algorithm computes the partition function

TheoremThe forward algorithm computes the partition function#✓fully proved

For a chain conditional random field with a finite set of states and weights in a semiring, and an observation stream \(x\), for every \(t\) the partition function at time \(t\) equals \(\sum_s \alpha_t(s)\), the sum over all states \(s\) of the forward variables \(\alpha_t(s)\).

theorem partition_eq_sum_forward (t : ℕ) :
    partition c x t = ∑ s, forward c x t s

Uses 5

Statement usesLinear-chain conditional random field · Forward variables of a chain CRF · Partition function of a chain CRF

Proof usesThe forward variables are path weights · Weight of a label path in a chain CRF

25 fully proved

Viterbi

DefinitionThe Viterbi variables of a chain CRF#✓fully proved

Let \(c\) be a chain conditional random field with a finite nonempty set of states \(S\) and weights in a linearly ordered commutative semiring \(R\), and let \(x\) be an observation sequence. Write \(\phi_t(s)\) for the unary potential of \(c\) at \(x\) of state \(s\) at position \(t\), and \(\psi_t(s', s)\) for its transition potential from \(s'\) to \(s\) at step \(t\). The Viterbi variables \(V_t(s)\), for \(t \in \mathbb{N}\) and \(s \in S\), are defined by \(V_0(s) = \phi_0(s)\) and

\[V_{t+1}(s) = \Big(\max_{s' \in S} V_t(s') \, \psi_t(s', s)\Big) \, \phi_{t+1}(s).\]

Thus \(V_t(s)\) is the largest weight of a label path of length \(t + 1\) ending in \(s\).

def viterbi : ℕ → S → R
  | 0, s => c.unary x 0 s
  | t + 1, s => Finset.univ.sup' Finset.univ_nonempty
      (fun s' => viterbi t s' * c.trans x t s' s) * c.unary x (t + 1) s

Uses 1 · Used by 5

Statement usesLinear-chain conditional random field

Used byThe Viterbi variables of a chain CRF are attained · The backtracked path of a chain CRF attains the Viterbi variable · The Viterbi path of a chain CRF has maximal weight · Path weights of a chain CRF are bounded by the Viterbi variables · Viterbi computes the MAP value of a chain CRF

TheoremPath weights of a chain CRF are bounded by the Viterbi variables#✓fully proved

For a chain conditional random field with a nonempty finite set of states, weights in a linearly ordered commutative semiring, and an observation stream \(x\), for every \(t\) and every label path \(z = (z_0, \dots, z_t)\), the weight of \(z\) is at most the Viterbi variable at time \(t\) of its last state \(z_t\).

theorem pathWeight_le_viterbi :
    ∀ (t : ℕ) (z : Fin (t + 1) → S),
      pathWeight c x t z ≤ viterbi c x t (z (Fin.last t))

Uses 3 · Used by 2

Statement usesLinear-chain conditional random field · Weight of a label path in a chain CRF · The Viterbi variables of a chain CRF

Used byThe Viterbi path of a chain CRF has maximal weight · Viterbi computes the MAP value of a chain CRF

TheoremThe Viterbi variables of a chain CRF are attained#✓fully proved

Let \(c\) be a chain CRF with a finite nonempty set of states \(S\) and weights in a linearly ordered commutative semiring, and let \(x\) be an observation sequence. For every \(t \in \mathbb{N}\) and every state \(s \in S\) there is a label path \(z = (z_0, \dots, z_t) \in S^{t+1}\) with \(z_t = s\) whose path weight equals the Viterbi variable of \(s\) at time \(t\).

theorem exists_pathWeight_eq_viterbi :
    ∀ (t : ℕ) (s : S),
      ∃ z : Fin (t + 1) → S, z (Fin.last t) = s ∧ pathWeight c x t z = viterbi c x t s

Uses 3 · Used by 1

Statement usesLinear-chain conditional random field · Weight of a label path in a chain CRF · The Viterbi variables of a chain CRF

Used byViterbi computes the MAP value of a chain CRF

TheoremViterbi computes the MAP value of a chain CRF#✓fully proved

Let \(c\) be a chain conditional random field with a finite nonempty set of states \(S\) and weights in a linearly ordered commutative semiring \(R\), and let \(x\) be an observation sequence. For every \(t \in \mathbb{N}\), the maximum over \(s \in S\) of the Viterbi variable \(V_t(s)\) of \(c\) at \(x\) equals the maximum, over all label paths \(z : \{0, \dots, t\} \to S\), of the weight of \(z\).

theorem sup'_viterbi_eq (t : ℕ) :
    (Finset.univ : Finset S).sup' Finset.univ_nonempty (viterbi c x t) =
      (Finset.univ : Finset (Fin (t + 1) → S)).sup' Finset.univ_nonempty (pathWeight c x t)

Uses 5

Statement usesLinear-chain conditional random field · Weight of a label path in a chain CRF · The Viterbi variables of a chain CRF

Proof usesThe Viterbi variables of a chain CRF are attained · Path weights of a chain CRF are bounded by the Viterbi variables

Conditional probabilities

DefinitionConditional probability of a label path in a chain CRF#✓fully proved

Let \(c\) be a chain CRF with a finite set of states \(S\) and weights in a semifield \(R\) carrying a partial order \(\le\), and let \(x\) be an observation sequence. For \(t \in \mathbb{N}\), the conditional probability of a label path \(z \in S^{t+1}\) given \(x\) is \(w_t(z) / Z_t\), where \(w_t(z)\) is the path weight of \(z\) and \(Z_t\) is the partition function, the total path weight of all label paths in \(S^{t+1}\); the quotient is \(0\) when \(Z_t = 0\).

def condProb (t : ℕ) (z : Fin (t + 1) → S) : R := pathWeight c x t z / partition c x t

Uses 3 · Used by 2

Statement usesLinear-chain conditional random field · Partition function of a chain CRF · Weight of a label path in a chain CRF

Used byConditional probabilities of a chain CRF are nonnegative · The conditional probabilities sum to \(1\)

TheoremThe conditional probabilities sum to \(1\)#✓fully proved

Let \(c\) be a chain conditional random field with finitely many states \(S\) and weights in a semifield \(R\) equipped with a partial order (not assumed compatible with the operations), let \(x\) be an observation sequence, and let \(t \in \mathbb{N}\). If the partition function of \(c\) at \(x\) and time \(t\) is positive, then the conditional probabilities \(p(z \mid x)\) of all label paths \(z : \{0, \dots, t\} \to S\) of length \(t + 1\) sum to \(1\).

theorem sum_condProb_eq_one (t : ℕ) (hpos : 0 < partition c x t) :
    ∑ z : Fin (t + 1) → S, condProb c x t z = 1

Uses 4

Statement usesLinear-chain conditional random field · Conditional probability of a label path in a chain CRF · Partition function of a chain CRF

Proof usesWeight of a label path in a chain CRF

TheoremConditional probabilities of a chain CRF are nonnegative#✓fully proved

Let \(c\) be a chain CRF with a finite set of states \(S\) and weights in a linearly ordered field \(R\), and let \(x\) be an observation sequence. For every \(t \in \mathbb{N}\) and every label path \(z = (z_0, \dots, z_t) \in S^{t+1}\), the conditional probability of \(z\) given \(x\) is nonnegative.

No positivity of the partition function is assumed; nonnegativity comes from the nonnegativity of the potentials.

theorem condProb_nonneg (t : ℕ) (z : Fin (t + 1) → S) :
    0 ≤ condProb c x t z

Uses 4

Statement usesLinear-chain conditional random field · Conditional probability of a label path in a chain CRF

Proof usesPartition function of a chain CRF · Weight of a label path in a chain CRF

Every HMM embeds as a CRF

DefinitionThe chain CRF of a hidden Markov model#✓fully proved

Let \(h\) be a hidden Markov model with initial weights \(\pi(s)\), transition weights \(a(s, s')\) and emission weights \(b(s, o)\) in a linearly ordered commutative semiring, all nonnegative. Its chain CRF has, for every observation stream \(x\), unary potentials \(u_0(s) = \pi(s)\, b(s, x_0)\) and \(u_t(s) = b(s, x_t)\) for \(t \ge 1\), and transition potentials \(\tau_t(s, s') = a(s, s')\) at every step \(t\).

def hmmToCRF (hn : h.Nonneg) : ChainCRF S O R where
  unary x t s := if t = 0 then h.init s * h.emit s (x t) else h.emit s (x t)
  trans _x _t s s' := h.trans s s'
  unary_nonneg x t s := by
    by_cases ht : t = 0
    · subst ht
      simp only [ite_true]
      exact mul_nonneg (hn.init _) (hn.emit _ _)
    · simp only [ht, ite_false]
      exact hn.emit _ _
  trans_nonneg _x _t s s' := hn.trans _ _

Uses 3 · Used by 1

Statement usesLinear-chain conditional random field · Hidden Markov model · Hidden Markov models with nonnegative weights

Used byThe chain CRF of a hidden Markov model has the same path weights

TheoremThe chain CRF of a hidden Markov model has the same path weights#✓fully proved

Let \(h\) be a hidden Markov model with nonnegative weights in a linearly ordered commutative semiring, and let \(x\) be an observation stream. For every \(t\) and every state path \(z = (z_0, \dots, z_t)\), the weight of \(z\) in the chain CRF of \(h\) given \(x\) equals the joint weight in \(h\) of the state path \(z\) and the observations \(x_0, \dots, x_t\).

theorem hmmToCRF_pathWeight (hn : h.Nonneg) :
    ∀ (t : ℕ) (z : Fin (t + 1) → S),
      pathWeight (hmmToCRF h hn) x t z =
        Cslib.MachineLearning.Sequence.HiddenMarkov.pathProb h x t z

Uses 6

Statement usesThe chain CRF of a hidden Markov model · Weight of a label path in a chain CRF · Hidden Markov model · Hidden Markov models with nonnegative weights · Joint weight of a state path and the observations

Proof usesLinear-chain conditional random field

Tabulated algorithms on Fin n

DefinitionOne step of the tabulated CRF forward algorithm#✓fully proved

Let \(c\) be a chain CRF with states \(\{0, \dots, n-1\}\) and weights in a semiring \(R\) carrying a relation \(\le\), with unary potential \(\phi_t(s)\) at position \(t\) and transition potential \(\psi_t(s', s)\) from \(s'\) to \(s\) at step \(t\), given the observation sequence \(x\). For a table \(v \in R^n\) and a step \(t\), the forward step returns the table whose entry at a state \(s\) is

\[\Bigl(\sum_{s'=0}^{n-1} v_{s'} \, \psi_t(s', s)\Bigr) \, \phi_{t+1}(s).\]

def forwardStep (v : Vector R n) (t : ℕ) : Vector R n :=
  Vector.ofFn fun s => (∑ s', v[s'] * c.trans x t s' s) * c.unary x (t + 1) s

Uses 1 · Used by 1

Statement usesLinear-chain conditional random field

Used byTabulated CRF forward algorithm

DefinitionTabulated CRF forward algorithm#✓fully proved

Let \(c\) be a chain CRF with states \(\{0, \dots, n-1\}\) and weights in a semiring \(R\) carrying a relation \(\le\), with unary potential \(\phi_t(s)\) at position \(t\) given the observation sequence \(x\). The forward table is the sequence of vectors in \(R^n\) defined by recursion on time: at time \(0\) its entry at \(s\) is \(\phi_0(s)\), and the table at time \(t + 1\) is the forward step at step \(t\) applied to the table at time \(t\).

Each step takes \(O(n^2)\) operations.

def forwardTab : ℕ → Vector R n
  | 0 => Vector.ofFn fun s => c.unary x 0 s
  | t + 1 => forwardStep x c (forwardTab t) t

Uses 2 · Used by 1

Statement usesLinear-chain conditional random field · One step of the tabulated CRF forward algorithm

Used byThe tabulated forward algorithm for chain CRFs

DefinitionThe tabulated forward algorithm for chain CRFs#✓fully proved

For a chain conditional random field with states \(0, \dots, n - 1\) and weights in a semiring, and an observation stream \(x\), the tabulated partition function at time \(t\) is the sum of the entries of the forward table at time \(t\), the vector \((\alpha_t(0), \dots, \alpha_t(n - 1))\) of forward variables computed step by step from time \(0\).

It equals the partition function at time \(t\) and takes \(O(t n^2)\) operations.

def partitionTab (t : ℕ) : R :=
  Cslib.MachineLearning.Sequence.HiddenMarkov.sumVec (forwardTab x c t)

Uses 3

Statement usesLinear-chain conditional random field · Tabulated CRF forward algorithm · Sum of the entries of a vector

DefinitionOne step of the tabulated Viterbi recursion for a chain CRF#✓fully proved

Let \(c\) be a chain conditional random field with states \(\{0, \dots, n - 1\}\), where \(n \ge 1\), and weights in a linearly ordered commutative semiring \(R\), and let \(x\) be an observation sequence. Write \(\phi_t(s)\) for the unary potential of \(c\) at \(x\) of state \(s\) at position \(t\), and \(\psi_t(s', s)\) for its transition potential from \(s'\) to \(s\) at step \(t\). Given a vector \(v \in R^n\) and \(t \in \mathbb{N}\), the Viterbi step returns the vector in \(R^n\) whose entry at state \(s\) is

\[\Big(\max_{s'} v_{s'} \, \psi_t(s', s)\Big) \, \phi_{t+1}(s).\]

def viterbiStep (v : Vector R n) (t : ℕ) : Vector R n :=
  Vector.ofFn fun s => Finset.univ.sup' Finset.univ_nonempty
    (fun s' => v[s'] * c.trans x t s' s) * c.unary x (t + 1) s

Uses 1 · Used by 1

Statement usesLinear-chain conditional random field

Used byThe tabulated Viterbi variables of a chain CRF

DefinitionThe tabulated Viterbi variables of a chain CRF#✓fully proved

Let \(c\) be a chain conditional random field with states \(\{0, \dots, n - 1\}\), where \(n \ge 1\), and weights in a linearly ordered commutative semiring \(R\), and let \(x\) be an observation sequence. Write \(\phi_0(s)\) for the unary potential of \(c\) at \(x\) of state \(s\) at position \(0\). The Viterbi table assigns to each \(t \in \mathbb{N}\) a vector \(T_t \in R^n\): the vector \(T_0\) has entry \(\phi_0(s)\) at each state \(s\), and \(T_{t+1}\) is the Viterbi step at time \(t\) applied to \(T_t\).

The entry of \(T_t\) at state \(s\) is the Viterbi variable \(V_t(s)\).

def viterbiTab : ℕ → Vector R n
  | 0 => Vector.ofFn fun s => c.unary x 0 s
  | t + 1 => viterbiStep x c (viterbiTab t) t

Uses 2 · Used by 4

Statement usesLinear-chain conditional random field · One step of the tabulated Viterbi recursion for a chain CRF

Used byBacktracked path of the tabulated CRF Viterbi algorithm · The Viterbi path of a chain CRF · The backtracked path of a chain CRF attains the Viterbi variable · The Viterbi path of a chain CRF has maximal weight

DefinitionBackpointer of the tabulated CRF Viterbi algorithm#✓fully proved

Let \(c\) be a chain CRF with states \(\{0, \dots, n-1\}\), where \(n \ge 1\), and weights in a linearly ordered commutative semiring \(R\), and let \(\psi_t(s', s)\) be its transition potential from \(s'\) to \(s\) at step \(t\) given the observation sequence \(x\). For a step \(t\), a table \(v \in R^n\) and a state \(s\), the backpointer of \(s\) is the first state \(s'\), in the order \(0, \dots, n-1\), that maximizes \(v_{s'} \, \psi_t(s', s)\).

def back (t : ℕ) (v : Vector R n) (s : Fin n) : Fin n :=
  Cslib.MachineLearning.Sequence.HiddenMarkov.argmaxFin fun s' => v[s'] * c.trans x t s' s

Uses 2 · Used by 2

Statement usesLinear-chain conditional random field · First maximizer of a function on a finite range

Used byBacktracked path of the tabulated CRF Viterbi algorithm · The backtracked path of a chain CRF attains the Viterbi variable

DefinitionBacktracked path of the tabulated CRF Viterbi algorithm#✓fully proved

Let \(c\) be a chain CRF with states \(\{0, \dots, n-1\}\), where \(n \ge 1\), and weights in a linearly ordered commutative semiring, and fix an observation sequence \(x\). For a state \(s\), the backtracked path \(b_t(s) = (b_t(s)_0, \dots, b_t(s)_t)\) of length \(t + 1\) is defined by recursion on \(t\): \(b_0(s)\) is the one-state path \((s)\), and \(b_{t+1}(s)\) is \(b_t(s')\) followed by \(s\), where \(s'\) is the backpointer of \(s\) at step \(t\) computed from the Viterbi table at time \(t\).

def bestPath : (t : ℕ) → Fin n → Fin (t + 1) → Fin n
  | 0, s => fun _ => s
  | t + 1, s => Fin.snoc (bestPath t (back x c t (viterbiTab x c t) s)) s

Uses 3 · Used by 3

Statement usesLinear-chain conditional random field · Backpointer of the tabulated CRF Viterbi algorithm · The tabulated Viterbi variables of a chain CRF

Used byThe Viterbi path of a chain CRF · The backtracked path of a chain CRF attains the Viterbi variable · The Viterbi path of a chain CRF has maximal weight

TheoremThe backtracked path of a chain CRF attains the Viterbi variable#✓fully proved

For a chain conditional random field with states \(0, \dots, n - 1\) where \(n \ge 1\), weights in a linearly ordered commutative semiring, and an observation stream \(x\), for every \(t\) and every state \(s\) the weight of the backtracked path of length \(t + 1\) ending in \(s\), obtained by following the backpointers, equals the Viterbi variable at time \(t\) of \(s\).

theorem pathWeight_bestPath : ∀ (t : ℕ) (s : Fin n),
    pathWeight c x t (bestPath x c t s) = viterbi c x t s

Uses 7 · Used by 1

Statement usesLinear-chain conditional random field · Backtracked path of the tabulated CRF Viterbi algorithm · Weight of a label path in a chain CRF · The Viterbi variables of a chain CRF

Proof usesBackpointer of the tabulated CRF Viterbi algorithm · The tabulated Viterbi variables of a chain CRF · First maximizer of a function on a finite range

Used byThe Viterbi path of a chain CRF has maximal weight

DefinitionThe Viterbi path of a chain CRF#✓fully proved

Let \(c\) be a chain CRF with states \(\{0, \dots, n-1\}\), where \(n \ge 1\), and weights in a linearly ordered commutative semiring, and let \(x\) be an observation sequence. For \(t \in \mathbb{N}\), the Viterbi path of length \(t + 1\) is the backtracked path ending in the first state, in the order \(0, \dots, n-1\), that maximizes the Viterbi table at time \(t\).

def crfPath (t : ℕ) : Fin (t + 1) → Fin n :=
  bestPath x c t
    (Cslib.MachineLearning.Sequence.HiddenMarkov.argmaxVec (viterbiTab x c t))

Uses 4 · Used by 1

Statement usesLinear-chain conditional random field · Backtracked path of the tabulated CRF Viterbi algorithm · The tabulated Viterbi variables of a chain CRF · Index of a largest entry of a table

Used byThe Viterbi path of a chain CRF has maximal weight

TheoremThe Viterbi path of a chain CRF has maximal weight#✓fully proved

For a chain conditional random field with states \(0, \dots, n - 1\) where \(n \ge 1\), weights in a linearly ordered commutative semiring, and an observation stream \(x\), for every \(t\) and every label path \(z\) of length \(t + 1\), the weight of \(z\) is at most the weight of Viterbi's MAP path of length \(t + 1\).

theorem pathWeight_le_crfPath (t : ℕ) (z : Fin (t + 1) → Fin n) :
    pathWeight c x t z ≤ pathWeight c x t (crfPath x c t)

Uses 10

Statement usesLinear-chain conditional random field · The Viterbi path of a chain CRF · Weight of a label path in a chain CRF

Proof usesBacktracked path of the tabulated CRF Viterbi algorithm · The backtracked path of a chain CRF attains the Viterbi variable · Path weights of a chain CRF are bounded by the Viterbi variables · The Viterbi variables of a chain CRF · The tabulated Viterbi variables of a chain CRF · First maximizer of a function on a finite range · Index of a largest entry of a table

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.