Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-generatedPipeline-generatedprecheck pass
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.

An observed-range language-model scaling fit

Example

Kaplan et al. measured held-out next-token cross-entropy for decoder-only autoregressive Transformer language models trained on WebText2. Here decoder-only means a stack of causal self-attention and positionwise feedforward blocks with residual connections and rowwise layer normalization, omitting the encoder and encoder–decoder cross-attention sublayers. With positional information and a vocabulary-probability output, it assigns a next-token conditional distribution given earlier tokens; its sequence likelihood factors into those next-token probabilities. Let N be the paper’s non-embedding parameter count, D the training dataset size in tokens, and L the held-out test loss. The tested model sizes range from 768 to 1.5×109 non-embedding parameters, and tested dataset sizes range from 22×106 to 23×109 tokens. WebText2 contains 20.3 million documents and 2.29×1010 tokens, of which 6.6×108 were reserved for testing.

The paper reports three separate empirical one-variable fits, each for its stated regime, rather than one joint formula. For parameter-limited models trained to convergence on sufficiently large data,

L(N)≈(NcN)αN,αN≈0.076,Nc≈8.8×1013 non-embedding parameters.

For large models trained on a limited dataset with early stopping,

L(D)≈(DcD)αD,αD≈0.095,Dc≈5.4×1013 tokens.

For compute-efficient training with a sufficiently large dataset and an optimally sized model, the source uses a batch-adjusted non-embedding compute estimate. At a fixed target loss, let B>0 be the actual batch size in tokens, S>0 the actual number of training steps, and Bcrit>0 the critical batch size in tokens. In the paper’s empirical batch-size model, set

C=6NBS,Smin⁡=S1+Bcrit/B,Cmin⁡=C1+B/Bcrit=6NBcritSmin⁡.

Here C estimates actual non-embedding training FLOPs, Smin⁡ estimates the minimum step count at large batch size, and Cmin⁡ estimates the minimum compute at small batch size. These are model-based adjustments, not exact laws for arbitrary training runs; compute is converted to PF-days for the fitted curve below. Its fitted compute curve is

L(Cmin⁡)≈(Ccmin⁡Cmin⁡)αCmin⁡,αCmin⁡≈0.050,Ccmin⁡≈3.1×108 PF-days.

The compute fit spans eight orders of magnitude in Cmin⁡. The reported compute-allocation fits are Nopt∝Cmin⁡0.73, Bcrit∝Cmin⁡0.24, and Smin⁡∝Cmin⁡0.03; the last exponent is sufficiently small that the authors say it may be consistent with zero. The paper’s table labels the reported S-min relation as a lower bound. The paper also gives a separate model-derived compute-loss exponent of about 0.054; it is not the empirical fit value 0.050. The scale constants depend on vocabulary and tokenization.

For any doubling that stays within a fit’s measured range, the corresponding fitted curve predicts a loss ratio of 2−0.076, 2−0.095, or 2−0.050 in its respective regime. Applying any curve beyond its reported range, or interpreting a smooth loss fit as a prediction about an unmeasured capability, is extrapolation. The paper reports similar model-size trends on a finite set of other text datasets after WebText2 training, but this is not a universal transfer or reliability guarantee under distribution shift. These are empirical fits, not general theorems about emergent capability, downstream-task performance, other modalities, or universally optimal compute allocation.

Example references

Foundation models as broad-pretraining and adaptation systems: gives the report’s qualitative foundation-model usage and states that pretraining loss entails no general capability or transfer guarantee.

Transformer encoder, decoder, and fixed-width expressivity blocks: supplies the causal self-attention, positionwise feedforward, residual, and normalization components; its encoder–decoder layer additionally has cross-attention, which the decoder-only variant described here omits. This example imports no expressivity or universality theorem.

Kaplan et al., Scaling Laws for Neural Language Models, §§1.2, 2.1–2.3, 3.2–3.3, 5.1, 6.1–6.3, §8, and Appendix A: empirical one-variable fits, parameter and dataset ranges, batch-adjusted compute definition, allocation fits, and stated limits.

Facts & Assumptions

Given: Each reported curve is a fitted empirical relation used only in its stated training regime. Its scale variable is positive, and its exponent is the approximate value stated in the example.

[F1]

Foundation models as broad-pretraining and adaptation systems: a foundation model is broadly pretrained and adapted to downstream tasks; the definition guarantees no downstream performance from a pretraining loss.

[F2]

Transformer encoder, decoder, and fixed-width expressivity blocks: the encoder–decoder layer includes causal self-attention, cross-attention to encoder states, and a positionwise feedforward sublayer, with residual connections and rowwise normalization. Its causal mask admits keys only at positions j≤i; the decoder-only variant in this example omits cross-attention.

Verification

1.1givenalgebra

For x,xc,λ>0 and a fitted power curve L^(x)=(xc/x)α, exponent laws give L^(λx)/L^(x)=((xc/(λx))/(xc/x))α=λ−α.

2.1givenF1F2step 1.1algebra∎

Set λ=2 and use in turn (x,α)=(N,0.076), (D,0.095), and (Cmin⁡,0.050) in their respective regimes; the fitted ratios are 2−0.076, 2−0.095, and 2−0.050. The allocation fits similarly multiply Nopt, Bcrit, and Smin⁡ by 20.73, 20.24, and 20.03 when Cmin⁡ doubles. These substitutions unpack the empirical fits only; [F1] and [F2] do not turn them into transfer or architecture theorems.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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