TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generated

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.

The finite-action Gibbs policy uniquely maximizes reward minus KL

Statement

Let $Y$ be a finite nonempty set, let $q$ be a probability vector on $Y$ with $q_{y} > 0$ for every $y$ , let $r : Y \to R$ , and let $β > 0$ . Define $Z = \sum_{y \in Y} q_{y} e^{r (y) / β}, p_{y}^{*} = \frac{q_{y} e^{r (y) / β}}{Z} .$ Then $Z$ is finite and positive, $p^{*}$ is a full-support probability vector, the maximum objective value is $F_{q, r, β} (p^{*}) = β \log Z$ , and for every probability vector $p$ on $Y$ , $F_{q, r, β} (p^{*}) - F_{q, r, β} (p) = β D (p ∥ p^{*}) \geq 0.$ Equality holds exactly when $p = p^{*}$ . Thus $p^{*}$ is the unique maximizer of the finite KL-regularized policy-improvement objective.

Statement references

Finite KL-regularized policy improvement: defines $F_{q, r, β}$ and the finite KL support convention.

Finite-label score loss: defines logarithmic loss as $- \log q_{y}$ and its expected loss as the corresponding finite sum.

Strict propriety of finite logarithmic loss: the truthful forecast uniquely minimizes expected logarithmic loss on the finite simplex.

Facts & Assumptions

Given: The finite nonempty set $Y$ , full-support probability vector $q$ , real reward $r$ , positive $β$ , and the vectors $p, p^{*}$ in the Statement.

[F1]

Finite KL-regularized policy improvement: $F_{q, r, β} (p) = \sum_{y} p_{y} r (y) - β D (p ∥ q)$ , and when the second vector is positive, $D (p ∥ q) = \sum_{y : p_{y} > 0} p_{y} \log (p_{y} / q_{y})$ with zero first-coordinate terms omitted.

[F2]

Strictly proper scoring rules on a finite label set: the finite expected logarithmic loss at forecast $v$ under probability vector $u$ is ${\overset{ˉ}{S}}_{\log} (u, v) = \sum_{y : u_{y} > 0} - u_{y} \log v_{y}$ .

[F3]

Log and Brier losses are strictly proper: for finite probability vectors $u, v$ , the expected logarithmic loss is minimized at the truthful forecast $v = u$ , with equality only there.

Proof

1.1givenalgebra

Since $Y$ is finite and each $q_{y} e^{r (y) / β}$ is a positive finite real, their sum $Z$ is positive and finite. The coordinates of $p^{*}$ are positive and sum to $1$ , so $p^{*}$ is a full-support probability vector.

2.1F1givenstep 1.1algebra

For each $y$ , the definition of $p^{*}$ gives $\log (p_{y}^{*} / q_{y}) = r (y) / β - \log Z$ . Substitution into the finite sum for $D (p ∥ p^{*})$ , omitting zero coordinates of $p$ , yields $β D (p ∥ p^{*}) = β D (p ∥ q) - \sum_{y} p_{y} r (y) + β \log Z = β \log Z - F_{q, r, β} (p)$ . All sums are finite, and all logarithm arguments in the sums are positive.

3.1F1step 2.1algebra

Substituting $p = p^{*}$ in step 2.1 gives $F_{q, r, β} (p^{*}) = β \log Z$ , because $D (p^{*} ∥ p^{*}) = 0$ . Therefore for every $p$ , step 2.1 gives $F_{q, r, β} (p^{*}) - F_{q, r, β} (p) = β D (p ∥ p^{*})$ .

4.1F1F2F3givenstep 3.1algebra∎

If $∣ Y ∣ = 1$ , its simplex contains only $p = p^{*}$ , so the objective gap is zero and the maximizer is unique. Otherwise identify $Y$ with a $K$ -label set, where $K = ∣ Y ∣ \geq 2$ . Since $p^{*}$ has full support, the difference ${\overset{ˉ}{S}}_{\log} (p, p^{*}) - {\overset{ˉ}{S}}_{\log} (p, p)$ is the finite sum $\sum_{y : p_{y} > 0} p_{y} \log (p_{y} / p_{y}^{*}) = D (p ∥ p^{*})$ by [F1] and [F2]. By [F3], this difference is nonnegative and is zero only when $p = p^{*}$ . As $β > 0$ , step 3.1 proves the stated inequality and uniqueness.

Depends on

Used by

Dependency tree · two levels

8 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

Rafael Rafailov et al., Direct Preference Optimization: Your Language Model is Secretly a Reward Model, arXiv:2305.18290v3 (2024) (standard reference, not scraped)
Purdue course lecture notes, Preference Optimization (PrefOpt) (standard reference, not scraped)