Variable elimination and belief propagation

StructurePairwise model on a tree#✓fully proved

For a type \(\alpha\) of values and \(n \in \mathbb{N}\), a pairwise tree model on the vertices \(0, \dots, n\) consists of a parent \(p(k + 1) \in \{0, \dots, k\}\) for each vertex \(k + 1\) with \(k < n\) (so vertex \(0\) is the root and every vertex comes after its parent), a unary factor \(\varphi_i : \alpha \to \mathbb{R}\) for each vertex \(i \le n\), and for each \(k < n\) a pairwise factor \(\psi_k(a, b) \in \mathbb{R}\) on the edge between vertex \(k + 1\) and its parent, defined for all \(a, b \in \alpha\), where \(a\) is the value at vertex \(k + 1\) and \(b\) the value at its parent.

structure TreeModel (α : Type*) (n : ℕ) where
  /-- The parent of vertex `k + 1`, among the vertices `0, …, k`. -/
  par : (k : Fin n) → Fin (k + 1)
  /-- The unary factor of each vertex. -/
  unary : Fin (n + 1) → α → ℝ
  /-- The factor of the edge between vertex `k + 1` (first argument) and its parent (second). -/
  pair : Fin n → α → α → ℝ

Used by 25

Used bySum-product belief · Belief at the root is the root message · Max-product decoding · Downward message to the last vertex · Removing the last vertex · Eliminating the last vertex of a tree model · Parent of the last vertex · Beliefs are the unnormalized marginals · Maximizing out the last vertex · Max-product message · Max-product value · Message from the last vertex · Nonnegative factors · Parent of a vertex · Variable elimination computes the partition function · Variable elimination computes the unnormalized root marginal · Root message of a tree model · One step of variable elimination · Summing out the last vertex preserves weighted sums at the other vertices · Variable elimination is exact · Belief propagation is exact on trees · Weight of an assignment in a tree model · Max-product decoding attains the max-product value · The max-product value bounds every weight · Max-product decoding finds a MAP assignment

DefinitionParent of a vertex#✓fully proved

In a pairwise tree model on the vertices \(0, \dots, n\), for \(k < n\) the parent of vertex \(k + 1\) is the parent recorded by the model, an element of \(\{0, \dots, k\}\), regarded as one of the vertices \(0, \dots, n\).

def parent (m : TreeModel α n) (k : Fin n) : Fin (n + 1) :=
  ⟨m.par k, by have := (m.par k).2; have := k.2; omega⟩

Uses 1 · Used by 7

Statement usesPairwise model on a tree

Used byOne step of variable elimination · Summing out the last vertex preserves weighted sums at the other vertices · Variable elimination is exact · Belief propagation is exact on trees · Weight of an assignment in a tree model · Max-product decoding attains the max-product value · The max-product value bounds every weight

DefinitionWeight of an assignment in a tree model#✓fully proved

Let \(\alpha\) be a type and let \(m\) be a pairwise model on a tree with vertices \(0, \dots, n\), with unary factors \(\varphi_i : \alpha \to \mathbb{R}\) for each vertex \(i\), and with factor \(\psi_k : \alpha \times \alpha \to \mathbb{R}\) on the edge between vertex \(k + 1\) and its parent \(p(k + 1)\) for each \(k < n\). The unnormalized weight of an assignment \(x : \{0, \dots, n\} \to \alpha\) is the real number

\[w(x) = \prod_{i=0}^{n} \varphi_i(x_i) \cdot \prod_{k=0}^{n-1} \psi_k(x_{k+1}, x_{p(k+1)}),\]

the product of all factors evaluated at \(x\).

noncomputable def weight (m : TreeModel α n) (x : Fin (n + 1) → α) : ℝ :=
  (∏ i, m.unary i (x i)) * ∏ k, m.pair k (x k.succ) (x (m.parent k))

Uses 2 · Used by 10

Statement usesPairwise model on a tree · Parent of a vertex

Used byBeliefs are the unnormalized marginals · Variable elimination computes the partition function · Variable elimination computes the unnormalized root marginal · One step of variable elimination · Summing out the last vertex preserves weighted sums at the other vertices · Variable elimination is exact · Belief propagation is exact on trees · Max-product decoding attains the max-product value · The max-product value bounds every weight · Max-product decoding finds a MAP assignment

DefinitionParent of the last vertex#✓fully proved

In a pairwise tree model on the vertices \(0, \dots, n + 1\), this is the parent of the last vertex \(n + 1\), regarded as one of the vertices \(0, \dots, n\) of the tree with the last vertex removed.

def lastParent (m : TreeModel α (n + 1)) : Fin (n + 1) :=
  ⟨m.par (Fin.last n), by have := (m.par (Fin.last n)).2; simp at this; omega⟩

Uses 1 · Used by 11

Statement usesPairwise model on a tree

Used bySum-product belief · Belief at the root is the root message · Max-product decoding · Downward message to the last vertex · Eliminating the last vertex of a tree model · Maximizing out the last vertex · One step of variable elimination · Summing out the last vertex preserves weighted sums at the other vertices · Belief propagation is exact on trees · Max-product decoding attains the max-product value · The max-product value bounds every weight

DefinitionMessage from the last vertex#✓fully proved

Let \(\alpha\) be finite and consider a pairwise tree model on the vertices \(0, \dots, n + 1\) with unary factors \(\varphi_i\) and pairwise factors \(\psi_k\). The message from the last vertex \(n + 1\) to its parent is the function \(\mu : \alpha \to \mathbb{R}\) given by \(\mu(a) = \sum_{b \in \alpha} \psi_n(b, a) \, \varphi_{n+1}(b)\), where \(\psi_n\) is the factor of the edge between vertex \(n + 1\) and its parent.

noncomputable def message [Fintype α] (m : TreeModel α (n + 1)) (a : α) : ℝ :=
  ∑ b, m.pair (Fin.last n) b a * m.unary (Fin.last (n + 1)) b

Uses 1 · Used by 3

Statement usesPairwise model on a tree

Used byEliminating the last vertex of a tree model · One step of variable elimination · Summing out the last vertex preserves weighted sums at the other vertices

DefinitionEliminating the last vertex of a tree model#✓fully proved

Let \(\alpha\) be finite, let \(m\) be a pairwise tree model on the vertices \(0, \dots, n + 1\) with parents \(p\), unary factors \(\varphi_i\) and pairwise factors \(\psi_k\), and let \(\mu\) be the message from the last vertex \(n + 1\) to its parent \(q = p(n + 1)\). Eliminating the last vertex gives the pairwise tree model on the vertices \(0, \dots, n\) in which vertex \(k + 1\) has parent \(p(k + 1)\) and edge factor \(\psi_k\) for each \(k < n\), and whose unary factors are \(\varphi'_q(a) = \varphi_q(a) \, \mu(a)\) and \(\varphi'_i = \varphi_i\) for every vertex \(i \le n\) with \(i \ne q\).

noncomputable def eliminate [Fintype α] (m : TreeModel α (n + 1)) :
    TreeModel α n where
  par k := m.par k.castSucc
  unary i a := m.unary i.castSucc a * if i = m.lastParent then m.message a else 1
  pair k := m.pair k.castSucc

Uses 3 · Used by 8

Statement usesPairwise model on a tree · Parent of the last vertex · Message from the last vertex

Used bySum-product belief · Belief at the root is the root message · Downward message to the last vertex · Root message of a tree model · One step of variable elimination · Summing out the last vertex preserves weighted sums at the other vertices · Variable elimination is exact · Belief propagation is exact on trees

TheoremOne step of variable elimination#✓fully proved

Let \(\alpha\) be finite, let \(m\) be a pairwise tree model on the vertices \(0, \dots, n + 1\) with weight \(w\), and let \(m'\) be the model on the vertices \(0, \dots, n\) obtained from \(m\) by eliminating the last vertex, with weight \(w'\). Then for every function \(g : \alpha \to \mathbb{R}\) we have \(\sum_x w(x) \, g(x_0) = \sum_y w'(y) \, g(y_0)\), where \(x\) ranges over all assignments \(\{0, \dots, n + 1\} \to \alpha\) and \(y\) over all assignments \(\{0, \dots, n\} \to \alpha\).

theorem sum_weight_mul_eliminate [Fintype α] (m : TreeModel α (n + 1)) (g : α → ℝ) :
    ∑ x, m.weight x * g (x 0) = ∑ y, m.eliminate.weight y * g (y 0)

Uses 7 · Used by 1

Statement usesPairwise model on a tree · Eliminating the last vertex of a tree model · Weight of an assignment in a tree model

Proof usesParent of the last vertex · Message from the last vertex · Parent of a vertex · Splitting a sum over \(\alpha^{n+1}\) at the last coordinate

Used byVariable elimination is exact

DefinitionRoot message of a tree model#✓fully proved

Let \(\alpha\) be finite. The root message of a pairwise tree model \(m\) on the vertices \(0, \dots, n\) is the function \(r_m : \alpha \to \mathbb{R}\) defined by recursion on \(n\): if \(n = 0\), it is the unary factor of the root \(0\); if \(m\) is a model on the vertices \(0, \dots, n + 1\), it is \(r_{m'}\), where \(m'\) is the model on the vertices \(0, \dots, n\) obtained from \(m\) by eliminating the last vertex.

By variable elimination, \(r_m(a)\) is the unnormalized marginal of the root at \(a\).

noncomputable def rootMessage [Fintype α] : {n : ℕ} → TreeModel α n → α → ℝ
  | 0, m => m.unary 0
  | _ + 1, m => rootMessage m.eliminate

Uses 2 · Used by 5

Statement usesPairwise model on a tree · Eliminating the last vertex of a tree model

Used byBelief at the root is the root message · Variable elimination computes the partition function · Variable elimination computes the unnormalized root marginal · Variable elimination is exact · Belief propagation is exact on trees

TheoremVariable elimination is exact#✓fully proved

Let \(\alpha\) be finite and let \(m\) be a pairwise tree model on the vertices \(0, \dots, n\) with weight \(w\) and root message \(r : \alpha \to \mathbb{R}\). Then for every function \(g : \alpha \to \mathbb{R}\) of the root value, \(\sum_x w(x) \, g(x_0) = \sum_{a \in \alpha} r(a) \, g(a)\), where \(x\) ranges over all assignments \(\{0, \dots, n\} \to \alpha\).

theorem sum_weight_mul_eq [Fintype α] :
    ∀ {n : ℕ} (m : TreeModel α n) (g : α → ℝ),
      ∑ x, m.weight x * g (x 0) = ∑ a, m.rootMessage a * g a

Uses 6 · Used by 3

Statement usesPairwise model on a tree · Root message of a tree model · Weight of an assignment in a tree model

Proof usesEliminating the last vertex of a tree model · Parent of a vertex · One step of variable elimination

Used byVariable elimination computes the partition function · Variable elimination computes the unnormalized root marginal · Belief propagation is exact on trees

TheoremVariable elimination computes the partition function#✓fully proved

Let \(\alpha\) be finite and let \(m\) be a pairwise tree model on the vertices \(0, \dots, n\) with weight \(w\) and root message \(r : \alpha \to \mathbb{R}\). Then the partition function of \(m\) is the total root message: \(\sum_x w(x) = \sum_{a \in \alpha} r(a)\), where \(x\) ranges over all assignments \(\{0, \dots, n\} \to \alpha\).

theorem partition_eq [Fintype α] {n : ℕ} (m : TreeModel α n) :
    ∑ x, m.weight x = ∑ a, m.rootMessage a

Uses 4

Statement usesPairwise model on a tree · Root message of a tree model · Weight of an assignment in a tree model

Proof usesVariable elimination is exact

TheoremVariable elimination computes the unnormalized root marginal#✓fully proved

Let \(\alpha\) be finite and let \(m\) be a pairwise tree model on the vertices \(0, \dots, n\) with weight \(w\) and root message \(r : \alpha \to \mathbb{R}\). Then for every \(a \in \alpha\) the unnormalized marginal of the root at \(a\) equals \(r(a)\), that is, \(\sum_x w(x) = r(a)\), where \(x\) ranges over the assignments \(\{0, \dots, n\} \to \alpha\) with \(x_0 = a\).

theorem rootMarginal_eq [Fintype α] [DecidableEq α] {n : ℕ} (m : TreeModel α n) (a : α) :
    ∑ x with x 0 = a, m.weight x = m.rootMessage a

Uses 4

Statement usesPairwise model on a tree · Root message of a tree model · Weight of an assignment in a tree model

Proof usesVariable elimination is exact

DefinitionRemoving the last vertex#✓fully proved

For a tree model with vertices \(0, \dots, n + 1\), the tree model on \(0, \dots, n\) with the same parents, unary factors and edge factors: the last vertex, which is a leaf, is removed together with its unary factor and the factor of its edge.

def dropLast (m : TreeModel α (n + 1)) : TreeModel α n where
  par k := m.par k.castSucc
  unary i := m.unary i.castSucc
  pair k := m.pair k.castSucc

Uses 1 · Used by 6

Statement usesPairwise model on a tree

Used bySum-product belief · Belief at the root is the root message · Downward message to the last vertex · Belief propagation is exact on trees · Max-product decoding attains the max-product value · The max-product value bounds every weight

TheoremSumming out the last vertex preserves weighted sums at the other vertices#✓fully proved

Let \(m\) be a pairwise tree model on the vertices \(0, \dots, n + 1\) with values in a finite type \(\alpha\), and let \(m'\) be the model on the vertices \(0, \dots, n\) obtained from \(m\) by summing out its last vertex. Write \(w_m\) and \(w_{m'}\) for their unnormalized weights. Then for every vertex \(v \le n\) and every function \(g : \alpha \to \mathbb{R}\),

\[\sum_x w_m(x)\, g(x_v) = \sum_y w_{m'}(y)\, g(y_v),\]

where \(x\) and \(y\) range over all assignments of values in \(\alpha\) to the vertices of \(m\) and of \(m'\).

theorem sum_weight_mul_eliminate_castSucc [Fintype α] (m : TreeModel α (n + 1))
    (v : Fin (n + 1)) (g : α → ℝ) :
    ∑ x, m.weight x * g (x v.castSucc) = ∑ y, m.eliminate.weight y * g (y v)

Uses 7 · Used by 1

Statement usesPairwise model on a tree · Eliminating the last vertex of a tree model · Weight of an assignment in a tree model

Proof usesParent of the last vertex · Message from the last vertex · Parent of a vertex · Splitting a sum over \(\alpha^{n+1}\) at the last coordinate

Used byBelief propagation is exact on trees

DefinitionSum-product belief#✓fully proved

The belief of each vertex of a tree model over a finite set of values, computed by sum-product message passing: the product of its unary factor, the messages from its subtree and the message from its parent. Recursively, in a model with a single vertex the belief of that vertex is its unary factor; in a model with vertices \(0, \dots, n + 1\) the belief of the last vertex at a value \(b\) is its unary factor at \(b\) times the downward message to the last vertex at \(b\), and the belief of every other vertex is its belief in the model with the last vertex summed out.

noncomputable def belief [Fintype α] : {n : ℕ} → TreeModel α n → Fin (n + 1) → α → ℝ
  | 0, m => fun _ => m.unary 0
  | _ + 1, m => Fin.lastCases (fun b => m.unary (Fin.last _) b * downMessage m b)
      (belief m.eliminate)

Uses 4 · Used by 3

Statement usesPairwise model on a tree · Removing the last vertex · Eliminating the last vertex of a tree model · Parent of the last vertex

Used byBelief at the root is the root message · Beliefs are the unnormalized marginals · Belief propagation is exact on trees

DefinitionDownward message to the last vertex#✓fully proved

For a tree model with vertices \(0, \dots, n + 1\) over a finite set of values, the message from the parent \(p\) of the last vertex to the last vertex at a value \(b\) is the sum over all values \(a\) of \(\psi(b, a)\, \beta(a)\), where \(\psi\) is the factor of the edge between the last vertex and \(p\) (last vertex first) and \(\beta(a)\) is the belief of \(p\) at \(a\) in the model without the last vertex.

noncomputable def downMessage [Fintype α] : {n : ℕ} → TreeModel α (n + 1) → α → ℝ
  | _, m => fun b => ∑ a, m.pair (Fin.last _) b a * belief m.dropLast m.lastParent a

Uses 4 · Used by 2

Statement usesPairwise model on a tree · Removing the last vertex · Eliminating the last vertex of a tree model · Parent of the last vertex

Used byBelief at the root is the root message · Belief propagation is exact on trees

TheoremBelief propagation is exact on trees#✓fully proved

Let \(m\) be a pairwise tree model on the vertices \(0, \dots, n\) with values in a finite type \(\alpha\), let \(w\) be its unnormalized weight, and let \(b_v\) be the belief of vertex \(v\) computed by sum-product message passing. Then for every vertex \(v\) and every function \(g : \alpha \to \mathbb{R}\),

\[\sum_x w(x)\, g(x_v) = \sum_{a \in \alpha} b_v(a)\, g(a),\]

where \(x\) ranges over all assignments of values in \(\alpha\) to the vertices.

theorem sum_weight_mul_eq_belief [Fintype α] :
    ∀ {n : ℕ} (m : TreeModel α n) (v : Fin (n + 1)) (g : α → ℝ),
      ∑ x, m.weight x * g (x v) = ∑ a, belief m v a * g a

Uses 12 · Used by 1

Statement usesPairwise model on a tree · Sum-product belief · Weight of an assignment in a tree model

Proof usesDownward message to the last vertex · Removing the last vertex · Eliminating the last vertex of a tree model · Parent of the last vertex · Parent of a vertex · Root message of a tree model · Summing out the last vertex preserves weighted sums at the other vertices · Variable elimination is exact · Splitting a sum over \(\alpha^{n+1}\) at the last coordinate

Used byBeliefs are the unnormalized marginals

TheoremBeliefs are the unnormalized marginals#✓fully proved

For every tree model over a finite set of values, every vertex \(v\) and every value \(a\), the belief of \(v\) at \(a\) is the unnormalized marginal of \(v\) at \(a\): the sum of the weights of all assignments \(x\) with \(x_v = a\).

theorem marginal_eq_belief [Fintype α] [DecidableEq α] (m : TreeModel α n) (v : Fin (n + 1))
    (a : α) : ∑ x with x v = a, m.weight x = belief m v a

Uses 4

Statement usesPairwise model on a tree · Sum-product belief · Weight of an assignment in a tree model

Proof usesBelief propagation is exact on trees

TheoremBelief at the root is the root message#✓fully proved

For every tree model over a finite set of values, the belief of the root, vertex \(0\), is the root message computed by variable elimination: the two agree at every value.

theorem belief_zero [Fintype α] : ∀ {n : ℕ} (m : TreeModel α n), belief m 0 = m.rootMessage

Uses 7

Statement usesPairwise model on a tree · Sum-product belief · Root message of a tree model

Proof usesDownward message to the last vertex · Removing the last vertex · Eliminating the last vertex of a tree model · Parent of the last vertex

DefinitionNonnegative factors#✓fully proved

A tree model has nonnegative factors when all its unary factors and all its edge factors take only nonnegative values.

def NonnegFactors (m : TreeModel α n) : Prop :=
  (∀ i a, 0 ≤ m.unary i a) ∧ ∀ k a b, 0 ≤ m.pair k a b

Uses 1 · Used by 2

Statement usesPairwise model on a tree

Used byThe max-product value bounds every weight · Max-product decoding finds a MAP assignment

DefinitionMax-product message#✓fully proved

For a tree model with vertices \(0, \dots, n + 1\) over a finite nonempty set of values, the max-product message from the last vertex to its parent at a value \(a\) is the maximum over all values \(b\) of \(\psi(b, a)\, \phi(b)\), where \(\psi\) is the factor of the edge between the last vertex and its parent and \(\phi\) is the unary factor of the last vertex.

noncomputable def maxMessage (m : TreeModel α (n + 1)) (a : α) : ℝ :=
  univ.sup' univ_nonempty fun b => m.pair (Fin.last n) b a * m.unary (Fin.last (n + 1)) b

Uses 1 · Used by 3

Statement usesPairwise model on a tree

Used byMaximizing out the last vertex · Max-product decoding attains the max-product value · The max-product value bounds every weight

DefinitionMaximizing out the last vertex#✓fully proved

For a tree model with vertices \(0, \dots, n + 1\) over a finite nonempty set of values, the tree model on \(0, \dots, n\) with the same parents and edge factors whose unary factor at the parent of the last vertex is multiplied by the max-product message of the last vertex; the other unary factors are unchanged.

noncomputable def maxEliminate (m : TreeModel α (n + 1)) : TreeModel α n where
  par k := m.par k.castSucc
  unary i a := m.unary i.castSucc a * if i = m.lastParent then m.maxMessage a else 1
  pair k := m.pair k.castSucc

Uses 3 · Used by 4

Statement usesPairwise model on a tree · Parent of the last vertex · Max-product message

Used byMax-product decoding · Max-product value · Max-product decoding attains the max-product value · The max-product value bounds every weight

DefinitionMax-product value#✓fully proved

For a tree model over a finite nonempty set of values, the value computed by maximizing out the vertices from the last one down: for a single vertex it is the maximum of its unary factor over all values, and for more vertices it is the max-product value of the model with the last vertex maximized out.

When all factors are nonnegative, this is the largest weight of an assignment.

noncomputable def maxWeight : {n : ℕ} → TreeModel α n → ℝ
  | 0, m => univ.sup' univ_nonempty (m.unary 0)
  | _ + 1, m => maxWeight m.maxEliminate

Uses 2 · Used by 3

Statement usesPairwise model on a tree · Maximizing out the last vertex

Used byMax-product decoding attains the max-product value · The max-product value bounds every weight · Max-product decoding finds a MAP assignment

DefinitionMax-product decoding#✓fully proved

An assignment of a tree model over a finite nonempty set of values, defined by recursion on the number of vertices. For a single vertex, its value is one that maximizes its unary factor. For vertices \(0, \dots, n + 1\), the vertices \(0, \dots, n\) get the decoding of the model with the last vertex maximized out, and the last vertex gets a value \(b\) maximizing \(\psi(b, a)\, \phi(b)\), where \(a\) is the decoded value of its parent, \(\psi\) is the factor of the edge between the last vertex and its parent and \(\phi\) is the unary factor of the last vertex; that is, \(b\) attains the max-product message of the last vertex at \(a\).

noncomputable def decode : {n : ℕ} → TreeModel α n → Fin (n + 1) → α
  | 0, m => fun _ => (exists_max_image univ (m.unary 0) univ_nonempty).choose
  | _ + 1, m => Fin.snoc (decode m.maxEliminate) (exists_max_image univ (fun b =>
      m.pair (Fin.last _) b (decode m.maxEliminate m.lastParent) * m.unary (Fin.last _) b)
      univ_nonempty).choose

Uses 3 · Used by 2

Statement usesPairwise model on a tree · Parent of the last vertex · Maximizing out the last vertex

Used byMax-product decoding attains the max-product value · Max-product decoding finds a MAP assignment

TheoremThe max-product value bounds every weight#✓fully proved

Let \(m\) be a pairwise tree model with values in a finite nonempty type \(\alpha\) whose unary and pairwise factors are all nonnegative, and let \(M\) be its max-product value, obtained by maximizing out the vertices from the last one down. Then every assignment of values in \(\alpha\) to the vertices has weight at most \(M\).

theorem weight_le_maxWeight : ∀ {n : ℕ} {m : TreeModel α n}, m.NonnegFactors →
    ∀ x, m.weight x ≤ m.maxWeight

Uses 9 · Used by 1

Statement usesPairwise model on a tree · Nonnegative factors · Max-product value · Weight of an assignment in a tree model

Proof usesRemoving the last vertex · Parent of the last vertex · Maximizing out the last vertex · Max-product message · Parent of a vertex

Used byMax-product decoding finds a MAP assignment

TheoremMax-product decoding attains the max-product value#✓fully proved

Let \(m\) be a pairwise tree model with values in a finite nonempty type, and let \(M\) be its max-product value, obtained by maximizing out the vertices from the last one down. Then the weight of the assignment produced by max-product decoding equals \(M\).

theorem weight_decode : ∀ {n : ℕ} (m : TreeModel α n), m.weight m.decode = m.maxWeight

Uses 9 · Used by 1

Statement usesPairwise model on a tree · Max-product decoding · Max-product value · Weight of an assignment in a tree model

Proof usesRemoving the last vertex · Parent of the last vertex · Maximizing out the last vertex · Max-product message · Parent of a vertex

Used byMax-product decoding finds a MAP assignment

TheoremMax-product decoding finds a MAP assignment#✓fully proved

Let \(m\) be a pairwise tree model with values in a finite nonempty type \(\alpha\) whose unary and pairwise factors are all nonnegative. Then every assignment of values in \(\alpha\) to the vertices has weight at most the weight of the assignment produced by max-product decoding.

theorem weight_le_weight_decode {m : TreeModel α n} (hm : m.NonnegFactors) (x : Fin (n + 1) → α) :
    m.weight x ≤ m.weight m.decode

Uses 7

Statement usesPairwise model on a tree · Nonnegative factors · Max-product decoding · Weight of an assignment in a tree model

Proof usesMax-product value · Max-product decoding attains the max-product value · The max-product value bounds every weight

26 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.