TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Finite-HMM Viterbi decoding is exact sequence MAP

Statement

Given a finite discrete HMM and an observation sequence of positive length, the sequence-decoding algorithm returns no conditional MAP path exactly when the observation evidence is zero. When the evidence is positive, it returns a hidden-state sequence maximizing the posterior probability of the entire sequence, including when there are ties.

Facts & Assumptions

Given: A finite discrete HMM $(S, Y, π, A, B)$ , a sequence $y = (y_{1}, \dots, y_{T}) \in Y^{T}$ with $T \geq 1$ , and the HMM decoding algorithm.

[F1]

Finite hidden Markov models for sequence decoding: The joint mass is $p (z, y) = π (z_{1}) B (z_{1}, y_{1}) \prod_{t = 2}^{T} A (z_{t - 1}, z_{t}) B (z_{t}, y_{t})$ ; the evidence is the finite sum $p (y) = \sum_{z \in S^{T}} p (z, y)$ , and for $p (y) > 0$ the posterior path mass is $p (z ∣ y) = p (z, y) / p (y)$ ; a sequence MAP path is any $z$ maximizing this conditional mass.

[F2]

Viterbi sequence decoding for a finite hidden Markov model: The algorithm creates initial weights $π (s) B (s, y_{1})$ , transition edges exactly for positive transition and emission factors, edge weights equal to their products, and terminal weights $1$ ; it then runs finite-trellis Viterbi.

[F3]

Finite-trellis Viterbi decoding returns a maximum-score path: Finite-trellis Viterbi returns no path exactly when no trellis path exists; otherwise it returns a path with maximum product score.

[F4]

The finite hidden Markov joint law is normalized: For each $T \geq 1$ , the joint masses $p (z, y)$ sum to $1$ over all $z \in S^{T}$ and $y \in Y^{T}$ .

Proof

1.1givenF1F2algebra

A hidden path $z$ has positive joint mass exactly when its initial factor, first emission factor, and every later transition and emission factor are positive. By [F2], this is exactly the condition that $z$ is a path in the constructed trellis. The trellis score is the product of those same factors, with terminal factor $1$ , so it equals $p (z, y)$ . Conversely every trellis path gives such a positive-mass hidden path.

2.1givenF1F2F3F4step 1.1algebra∎

If the trellis has no path, step 1.1 shows every summand in [F1] is zero; hence $p (y) = 0$ and no conditional path mass is defined. If it has a path, step 1.1 gives a positive summand, so $p (y) > 0$ . By [F3], finite-trellis Viterbi then returns a path maximizing $p (z, y)$ . Dividing all path masses by the same positive $p (y)$ preserves their order, so this path maximizes $p (z ∣ y)$ . The normalization in [F4] makes these masses a probability law, and the backpointer tie rule returns one of the maximizers.

Depends on

Used by

An exact two-state HMM sequence-MAP calculation Example

Dependency tree · two levels

7 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Manolis Kellis, 6.096 Algorithms for Computational Biology, Lecture 7: Gene Finding and HMMs, MIT OpenCourseWare (Spring 2005) (standard reference, not scraped)
Stanford CS262, Lecture 7: Hidden Markov Models (standard reference, not scraped)