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.

Positive temperature scaling preserves the maximizing class

Statement

Let $K \geq 2$ , let $z \in R^{K}$ , and let $T > 0$ . Define $p_{j} (T) = \frac{\exp (z_{j} / T)}{\sum_{ℓ = 1}^{K} \exp (z_{ℓ} / T)} (j = 1, \dots, K) .$ Then $p (T)$ lies in the relative interior of $Δ_{K}$ in the affine hyperplane ${p \in R^{K} : \sum_{j} p_{j} = 1}$ and $\arg \max_{j \in {1, \dots, K}} p_{j} (T) = \arg \max_{j \in {1, \dots, K}} z_{j}$ . For the finite validation inputs and candidate temperatures specified in the validation temperature-scaling algorithm, every validation loss is finite and the stated smallest-minimizer rule returns a unique candidate.

Statement references

Validation temperature scaling: defines the finite candidate set, validation NLL, and tie-breaking rule whose well-definedness is also proved here.

The real exponential function and the number $e$ by a power series: defines the real exponential used in the softmax formula.

The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ : gives positivity of the exponential.

The exponential function is strictly increasing: supplies strict monotonicity for pairwise logit comparisons.

The natural logarithm as the inverse of the exponential function: defines the logarithm on positive reals, the domain of the validation losses.

Guo et al., full paper, Section 4.2: states that the scalar temperature leaves the maximizing class unchanged; the argument here verifies the claim under the stated positive-temperature hypotheses.

Facts & Assumptions

Given: $K \geq 2$ , a finite logit vector $z \in R^{K}$ , a positive temperature $T$ , and, for the algorithmic consequence, a nonempty finite validation sample and finite nonempty candidate temperature set.

[F1]

The temperature-scaling algorithm uses the displayed softmax probabilities, restricts candidate temperatures to a finite nonempty subset of $(0, \infty)$ , and chooses the smallest validation-NLL minimizer. Validation temperature scaling

[F2]

The real exponential is finite-valued and strictly positive on $R$ . The real exponential function and the number $e$ by a power series The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$

[F3]

The real exponential is strictly increasing. The exponential function is strictly increasing

[F4]

The natural logarithm is defined on $(0, \infty)$ . The natural logarithm as the inverse of the exponential function

Proof

1.1F1F2givenalgebra

For every $j$ , $w_{j} = \exp (z_{j} / T)$ is a finite positive real by [F2]. Hence $S = \sum_{ℓ = 1}^{K} w_{ℓ} > 0$ , each $p_{j} (T) = w_{j} / S$ is positive, and $\sum_{j} p_{j} (T) = 1$ . Put $ε = \frac{1}{2} \min_{j} p_{j} (T) > 0$ . If $u$ lies in the hyperplane $\sum_{j} u_{j} = 1$ and $∥ u - p (T) ∥_{2} < ε$ , then every $u_{j} > 0$ ; since the coordinates sum to one, $u \in Δ_{K}$ . Thus $p (T)$ is in the relative interior of $Δ_{K}$ .

2.1F1F4step 1.1algebra

For each validation example and class $j$ , step 1.1 gives $p_{T} (j ∣ x_{i}) > 0$ , so its logarithm is finite by [F4]. Thus each candidate loss is finite. The finite nonempty set $T$ has a nonempty finite set of minimizers, which has a unique smallest element; the algorithm therefore returns a unique $T^{*}$ .

3.1F1F2F3givenstep 1.1algebra∎

For any classes $j, ℓ$ , positivity of $T$ preserves the sign of $z_{j} - z_{ℓ}$ . By [F3], $\exp (z_{j} / T)$ and $\exp (z_{ℓ} / T)$ have the same strict order as $z_{j}$ and $z_{ℓ}$ ; division by their common positive denominator $S$ from step 1.1 preserves that order and preserves ties. Every pairwise comparison is therefore identical for $p (T)$ and $z$ , proving equality of their maximizing index sets.

Depends on

Used by

Calibration examples under validation and distribution shift Example

Cited to discharge well-definedness by Validation temperature scaling.

Dependency tree · two levels

21 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

Chuan Guo, Geoff Pleiss, Yu Sun, and Kilian Q. Weinberger, On Calibration of Modern Neural Networks, ICML 2017, Section 4.2 (standard reference, not scraped)