Alphabeta Math
ExampleConstruction: AI-generatedVerification: 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.

Calibration examples under validation and distribution shift

Example

Four finite cases separate probability calibration, accuracy, empirical calibration summaries, conformal coverage, and performance under a changed test law.

First, on a one-point probability space let Y=1 and let the forecast be G=(9/10,1/10). Its top prediction is always correct, but its top confidence is 9/10. On any nonempty sample from this law, the one-bin ECE and MCE are both 1/10.

Second, take four validation labels 1,1,1,2 and give every example logits (2log⁡3,0). Fit temperature scaling on the finite candidate set {1,2}. At temperature 1 the forecast is (9/10,1/10); at temperature 2 it is (3/4,1/4). The validation NLL rule chooses temperature 2. Both temperatures predict class 1, while their one-bin ECE values are respectively 3/20 and 0.

Third, let the feature be rare with probability 1/10 and common with probability 9/10, let the true label always be 1, and use labels {1,2}. Take one calibration pair and the test pair as independent draws from this same law, with trivial training information and fixed score s(x,y)=1{x is rare}. At miscoverage level α=1/2, the split conformal set has marginal coverage 91/100 but coverage 1/10 conditional on the test feature being rare.

Fourth, let a source law put probability one on feature clean with label 1, and let a distinct target law put probability one on feature corrupted with label 1. Use the fixed score values s(clean,1)=0, s(clean,2)=1, s(corrupted,1)=1, and s(corrupted,2)=2. With one calibration example from the source law and α=1/2, the split conformal threshold is 0, so the prediction set at a target feature is empty and target coverage is 0.

Example references

Top-label calibration: gives the event-integral condition used to check the first finite model.

Binned expected and maximum calibration error: gives the one-bin ECE and MCE calculations.

Validation temperature scaling: defines the finite-candidate validation NLL selection in the second model.

Positive temperature scaling preserves the maximizing class: proves that both temperatures keep the same maximizing class.

Split conformal prediction set for classification: defines the adjusted split score threshold and classification set.

Split conformal marginal coverage: gives the conditional-on-training exchangeable-coverage guarantee used in the third model.

Regular conditional distribution: specifies the conditional-kernel identity used for the finite constant kernel.

Exchangeable random elements: exchangeability means invariance of the joint law under every coordinate permutation.

Source and target joint laws, risks, and covariate shift: defines distinct source and target joint laws.

Log and Brier losses are strictly proper: strict propriety selects the forecast matching the empirical validation label law.

The natural logarithm as the inverse of the exponential function: gives exp⁡(log⁡3)=3 for the exact softmax calculations.

The exponential addition formula exp⁡(x+y)=exp⁡(x)exp⁡(y): gives exp⁡(2log⁡3)=exp⁡(log⁡3)2.

Lei et al., full paper, Section 2.2 and Appendix A.1: supplies the split conformal order-statistic construction and rank argument in an iid regression setting.

Tibshirani, full lecture notes, Sections 1.2–2.3: derives the adjusted score rank, conditional-on-training coverage, and the distinction from feature-conditional coverage.

Facts & Assumptions

Given: The four finite models in the Example, the stated deterministic score rules, and the finite validation and calibration samples.

[F1]

Top-label calibration requires P(Y=Y^, C∈B)=E[1{C∈B}C] for every Borel B⊆[0,1]. Top-label calibration

[F2]

Binned ECE is the sample-size-weighted absolute accuracy-confidence gap, and MCE is the largest such gap over occupied bins. Binned expected and maximum calibration error

[F3]

Validation temperature scaling minimizes the finite-sample mean negative log probability over a finite nonempty set of positive temperatures and returns the smallest minimizer. Validation temperature scaling

[F4]

For every positive temperature, softmax has the same maximizing index set as its logit vector. Positive temperature scaling preserves the maximizing class

[F5]

The split classification set uses k=⌈(m+1)(1−α)⌉, the kth calibration score when k≤m, and q=+∞ when k=m+1. Split conformal prediction set for classification

[F6]

If the example tuple has a regular conditional distribution given the training sigma-field whose sections are exchangeable, the split set has conditional coverage at least 1−α; this is not a subgroup-conditional assertion. Split conformal marginal coverage

[F7]

A regular conditional distribution is an everywhere probability kernel whose evaluations satisfy the conditional-event integral identity. Regular conditional distribution

[F8]

Exchangeability means that the joint law is invariant under every coordinate permutation. Exchangeable random elements

[F9]

The logarithmic score is strictly proper on the finite probability simplex. Log and Brier losses are strictly proper

[F10]

For positive u, log⁡u is the inverse of exp⁡; the exponential obeys exp⁡(a+b)=exp⁡(a)exp⁡(b). The natural logarithm as the inverse of the exponential function The exponential addition formula exp⁡(x+y)=exp⁡(x)exp⁡(y)

[F11]

A source-target pair consists of two probability laws on the feature-label product space, and they may be distinct. Source and target joint laws, risks, and covariate shift

[A1]

In the rare-feature model, calibration and test examples are independent draws from the same finite joint law μ on feature-label pairs, and the training sigma-field is trivial. The score rule is fixed and measurable on the finite feature-label space.

[A2]

In the clean/corrupted model, the calibration example is drawn from the source law and the test example from the distinct target law.

Verification

1.1F1F2givenalgebra

In the first model, Y^=1 and C=9/10 almost surely. For B={9/10}, the left side of [F1] is 1 and the right side is 9/10, so top-label calibration fails despite accuracy 1. In the single occupied bin, [F2] gives both errors as ∣1−9/10∣=1/10.

1.2F3F4F9F10givenalgebra

By [F10], temperature 1 gives first-class probability exp⁡(2log⁡3)/(1+exp⁡(2log⁡3))=9/10, while temperature 2 gives exp⁡(log⁡3)/(1+exp⁡(log⁡3))=3/4. The empirical NLL is the log-score risk Sˉlog⁡(p,pT) under the validation label frequencies p=(3/4,1/4). Strict propriety [F9] therefore makes the value at (3/4,1/4) strictly smaller than at (9/10,1/10), so [F3] selects T=2. By [F4], both temperatures predict class 1. Their one-bin gaps from the observed accuracy 3/4 are ∣3/4−9/10∣=3/20 and ∣3/4−3/4∣=0.

1.3A1F5F6F7F8givenalgebra

In the rare-feature model, m=1 and α=1/2 give k=⌈2(1/2)⌉=1, so the threshold is the single calibration score: it is 1 for a rare calibration feature and 0 for a common one. Write Q for the finite joint law of the calibration and test pairs; by [A1], Q(z1,z2)=μ(z1)μ(z2), which is unchanged by swapping coordinates. For the trivial training sigma-field, whose only events are ∅ and the whole space, the constant kernel with value Q satisfies [F7]: the conditional-event integral is zero for ∅ and is the ordinary law identity for the whole space. By [F8] its section is exchangeable. The finite score rule is measurable, so [F6] applies and yields conditional-on-training marginal coverage at least 1/2.

2.1A1F5step 1.3algebra

If the test feature is common, its true-label score is 0≤q for either possible threshold, so coverage is 1. If it is rare, its true-label score is 1, which is included exactly when the independent calibration feature is rare, an event of probability 1/10. Thus subgroup coverage is 1/10, while marginal coverage is (9/10)⋅1+(1/10)⋅(1/10)=91/100.

3.1A2F5F6F11givenalgebra∎

In the clean/corrupted model, the calibration score is always 0, so k=1 gives q=0. At the target feature, both candidate labels have scores 1 or 2, hence neither belongs to C(corrupted) and target coverage is 0. The calibration/test pair law assigns mass one to (clean, corrupted) and zero to (corrupted, clean), so it is not invariant under swapping; the exchangeability hypothesis in [F6] fails.

Remarks

Ovadia et al. report an empirical benchmark, not a general theorem. For their MNIST rotations and translations, their 80 corruption/intensity combinations on CIFAR-10 and ImageNet, their 20 Newsgroups class shift, and their Criteo categorical-token randomization, the reported behavior depends on the method and shift. In particular, temperature-scaling ECE rises with increasing corruption on CIFAR-10 and ImageNet, and its Brier score is worse than the vanilla method for the reported Criteo shift. Their method ordering differs between MNIST and the image benchmarks, so no universal ensemble ranking or calibration guarantee under shift follows. For fully out-of-label-set inputs, Ovadia et al. note that no ground-truth class lies in the model's label set; they report prediction-confidence and predictive-entropy histograms for those inputs rather than ECE. Their text experiments also plot confidence versus accuracy for mixtures of in-distribution and OOD examples.

Remarks references

Ovadia et al., full paper, Sections 2–5: specifies the evaluated models, datasets, shift families, metrics, and empirical conclusions summarized here.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

53 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