Cross-entropy loss

DefinitionCross-entropy loss#✓fully proved

Let \(f\) be a probabilistic classifier, assigning to each input \(x \in X\) a probability distribution \(f(x)\) on a finite set of labels, and let \(D = ((x_1, y_1), \dots, (x_N, y_N))\) be a labelled sample. The cross-entropy (log) loss of \(f\) on \(D\), in bits, is the value in \([0, \infty]\)

\[\Big(\sum_{n=1}^{N} H\big(\delta_{y_n}, f(x_n)\big)\Big) / N,\]

where \(H\) is the cross-entropy and \(\delta_y\) is the point mass at \(y\); it is \(0\) when \(N = 0\).

noncomputable def crossEntropyLoss (f : X → PMF α) (D : Fin N → X × α) : ℝ≥0∞ :=
  (∑ n, crossEntropy (PMF.pure (D n).2) (f (D n).1)) / N

Uses 1 · Used by 5

Statement usesCross-entropy

Used byThe cross-entropy loss is the average negative log-likelihood · Cross-entropy loss via the likelihood · The cross-entropy loss is infinite exactly when a label is ruled out · Minimizing cross-entropy is maximum likelihood · Comparing cross-entropy losses of classifiers that rule out no label

TheoremThe cross-entropy loss is the average negative log-likelihood#✓fully proved

Let \(f\) be a probabilistic classifier, assigning to each input \(x \in X\) a probability distribution \(f(x)\) on a finite set of labels, and let \(D = ((x_1, y_1), \dots, (x_N, y_N))\) be a labelled sample. The cross-entropy loss of \(f\) on \(D\) equals the average surprisal of the labels,

\[\Big(\sum_{n=1}^{N} s\big(f(x_n)(y_n)\big)\Big) / N,\]

where \(s(q) = -\log_2 q\) is the surprisal of a probability \(q\), with \(s(0) = \infty\), and the average is computed in \([0, \infty]\).

theorem crossEntropyLoss_eq (f : X → PMF α) (D : Fin N → X × α) :
    crossEntropyLoss f D = (∑ n, surprisal (f (D n).1 (D n).2)) / N

Uses 4 · Used by 2

Statement usesCross-entropy loss · Surprisal

Proof usesCross-entropy · Cross-entropy of a point mass

Used byCross-entropy loss via the likelihood · The cross-entropy loss is infinite exactly when a label is ruled out

TheoremThe cross-entropy loss is infinite exactly when a label is ruled out#✓fully proved

Let \(f\) be a probabilistic classifier, assigning to each input \(x \in X\) a probability distribution \(f(x)\) on a finite set of labels, and let \(D = ((x_1, y_1), \dots, (x_N, y_N))\) be a labelled sample with \(N \ge 1\). The cross-entropy loss of \(f\) on \(D\) is \(\infty\) if and only if \(f(x_n)(y_n) = 0\) for some \(n\).

theorem crossEntropyLoss_eq_top_iff (f : X → PMF α) (D : Fin N → X × α) (hN : N ≠ 0) :
    crossEntropyLoss f D = ∞ ↔ ∃ n, f (D n).1 (D n).2 = 0

Uses 3 · Used by 1

Statement usesCross-entropy loss

Proof usesThe cross-entropy loss is the average negative log-likelihood · Surprisal

Used byMinimizing cross-entropy is maximum likelihood

TheoremCross-entropy loss via the likelihood#✓fully proved

Let \(f\) be a probabilistic classifier, assigning to each input \(x \in X\) a probability distribution \(f(x)\) on a finite set of labels, and let \(D = ((x_1, y_1), \dots, (x_N, y_N))\) be a labelled sample with \(f(x_n)(y_n) \ne 0\) for every \(n\). Then the cross-entropy loss of \(f\) on \(D\) equals \(-\log_2(L) / N\), where \(L = \prod_{n=1}^{N} f(x_n)(y_n)\) is the likelihood of the sample and the division is computed in \([0, \infty]\), so that both sides are \(0\) when \(N = 0\).

theorem crossEntropyLoss_eq_neg_logb_prod (f : X → PMF α) (D : Fin N → X × α)
    (hpos : ∀ n, f (D n).1 (D n).2 ≠ 0) :
    crossEntropyLoss f D =
      ENNReal.ofReal (-logb 2 (∏ n, (f (D n).1 (D n).2).toReal)) / N

Uses 3 · Used by 1

Statement usesCross-entropy loss

Proof usesThe cross-entropy loss is the average negative log-likelihood · Surprisal

Used byComparing cross-entropy losses of classifiers that rule out no label

TheoremComparing cross-entropy losses of classifiers that rule out no label#✓fully proved

Let \(f\) and \(g\) be probabilistic classifiers, each assigning to every input \(x \in X\) a probability distribution on a finite set of labels, and let \(D = ((x_1, y_1), \dots, (x_N, y_N))\) be a labelled sample with \(N \ge 1\) such that \(f(x_n)(y_n) \ne 0\) and \(g(x_n)(y_n) \ne 0\) for every \(n\). Then the cross-entropy loss of \(f\) on \(D\) is at most that of \(g\) if and only if \(\prod_{n=1}^{N} g(x_n)(y_n) \le \prod_{n=1}^{N} f(x_n)(y_n)\).

theorem crossEntropyLoss_le_iff_of_ne_zero (f g : X → PMF α) (D : Fin N → X × α) (hN : N ≠ 0)
    (hf : ∀ n, f (D n).1 (D n).2 ≠ 0) (hg : ∀ n, g (D n).1 (D n).2 ≠ 0) :
    crossEntropyLoss f D ≤ crossEntropyLoss g D ↔
      ∏ n, (g (D n).1 (D n).2).toReal ≤ ∏ n, (f (D n).1 (D n).2).toReal

Uses 2 · Used by 1

Statement usesCross-entropy loss

Proof usesCross-entropy loss via the likelihood

Used byMinimizing cross-entropy is maximum likelihood

TheoremMinimizing cross-entropy is maximum likelihood#✓fully proved

Let \(f\) and \(g\) be probabilistic classifiers, each assigning to every input \(x \in X\) a probability distribution on a finite set of labels, and let \(D = ((x_1, y_1), \dots, (x_N, y_N))\) be a labelled sample with \(N \ge 1\). Then the cross-entropy loss of \(f\) on \(D\) is at most that of \(g\) if and only if \(\prod_{n=1}^{N} g(x_n)(y_n) \le \prod_{n=1}^{N} f(x_n)(y_n)\), that is, \(f\) gives the labels at least as large a likelihood as \(g\).

A label predicted to be impossible gives likelihood \(0\) and loss \(\infty\).

theorem crossEntropyLoss_le_iff (f g : X → PMF α) (D : Fin N → X × α) (hN : N ≠ 0) :
    crossEntropyLoss f D ≤ crossEntropyLoss g D ↔
      ∏ n, (g (D n).1 (D n).2).toReal ≤ ∏ n, (f (D n).1 (D n).2).toReal

Uses 3

Statement usesCross-entropy loss

Proof usesThe cross-entropy loss is infinite exactly when a label is ruled out · Comparing cross-entropy losses of classifiers that rule out no label

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.