Cotterell (2026): Surprisal Theory is Tautological (without Rational Grounding)

Surprisal theory holds that the processing difficulty of a unit in context is an affine function of its surprisal under some language model, with a positive slope and a baseline that may depend on the context. The paper argues that the claim is a tautology unless the language model is constrained: any nonnegative difficulty measure d over the next unit, or the end of the string, given a prefix, defines the model whose next-unit distribution is the softmax of -d, and its surprisal is d plus the log partition function of the prefix (surprisal_softmaxModel), so the claim holds with slope one and the negative log partition function as baseline. The one condition is that the model be a language model, i.e. tight. When the end difficulty is bounded along a series whose exponentials diverge, the softmax model ends with probability at least those exponentials over the size of the extended alphabet, and it is tight by Du and colleagues' sufficient condition (isTight_softmaxModel). A tight model's next-unit distributions are the next-unit laws of the language model it defines (Surprisal.nextWord_stringMeasure), so the difficulty is the surprisal of the unit under that language model up to a context-dependent baseline (surprisal_nextWord_softmaxModel), the tautology (exists_isTight_difficulty_eq_surprisal). A constant bound C also bounds the expected length by (1 - η) / η for η = exp (-C) over the size of the extended alphabet (lintegral_length_softmaxModel_le). Without the bound the construction can fail: an end difficulty growing linearly in the length of the prefix leaves the softmax model non-tight (not_isTight_softmaxModel_length).

Implementation notes

• The difficulty measure takes the next unit before the prefix, d o u for d(o | u), with none for the end of the string, and the model's next-unit kernel is the softmax kernel ProbabilityTheory.Kernel.softmax of the real score -d.
• The divergence hypothesis is stated in ℝ≥0∞, where a sum of nonnegative terms equals ∞ exactly when the series diverges; the paper states it for real series.
• The paper's bound f is nonnegative and its constant bound positive; neither sign condition is needed here.
• The paper remarks that the softmax construction need not give a language model but gives no example; not_isTight_softmaxModel_length is an added witness.
• The paper's fitness measure, its consistency theorem for maximum-likelihood estimation, and its scaling implication are not formalized.

References

• [Cot26]
• [DTHP+23]

noncomputable def Cotterell2026.softmaxModel {α : Type u_1} [Fintype α] [MeasurableSpace α] (d : Option α → List α → ℝ) : AutoregressiveSequenceModel α

The model whose next-unit distribution after u is the softmax of -d (· | u).

Equations

• Cotterell2026.softmaxModel d = { next := ProbabilityTheory.Kernel.softmax fun (u : List α) (o : Option α) => ↑(-d o u), isMarkovKernel_next := ⋯ }

theorem Cotterell2026.real_next_softmaxModel {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (d : Option α → List α → ℝ) (u : List α) (o : Option α) : ((softmaxModel d).next u).real {o} = Real.softmax (fun (o : Option α) => -d o u) o

theorem Cotterell2026.surprisal_softmaxModel {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (d : Option α → List α → ℝ) (u : List α) (o : Option α) : InformationTheory.surprisal ((softmaxModel d).next u) o = d o u + Real.log (∑ o' : Option α, Real.exp (-d o' u))

The surprisal of the softmax model is the difficulty plus the log partition function of the prefix.

theorem Cotterell2026.le_next_softmaxModel {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {d : Option α → List α → ℝ} (hd : ∀ (o : Option α) (u : List α), 0 ≤ d o u) (u : List α) (o : Option α) : ENNReal.ofReal (Real.exp (-d o u)) / ↑(Fintype.card (Option α)) ≤ ((softmaxModel d).next u) {o}

A nonnegative difficulty measure gives every next unit probability at least exp (-d o u) over the size of the extended alphabet.

theorem Cotterell2026.isTight_softmaxModel {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {d : Option α → List α → ℝ} (hd : ∀ (o : Option α) (u : List α), 0 ≤ d o u) {f : ℕ → ℝ} (hf : ∀ (u : List α), d none u ≤ f (u.length + 1)) (hdiv : ∑' (t : ℕ), ENNReal.ofReal (Real.exp (-f (t + 1))) = ⊤) : (softmaxModel d).IsTight

Proposition 1(a): a nonnegative difficulty measure whose end difficulty after a prefix of length t - 1 is at most f t, with ∑ exp (-f t) divergent, gives a tight softmax model.

theorem Cotterell2026.not_isTight_softmaxModel_length {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] [Nonempty α] : ¬(softmaxModel fun (o : Option α) (u : List α) => o.elim (↑u.length + 1) fun (x : α) => 0).IsTight

The softmax model need not be a language model: an end difficulty growing linearly in the length of the prefix, with every other difficulty zero, leaves it non-tight.

theorem Cotterell2026.surprisal_nextWord_softmaxModel {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {d : Option α → List α → ℝ} (hd : ∀ (o : Option α) (u : List α), 0 ≤ d o u) {f : ℕ → ℝ} (hf : ∀ (u : List α), d none u ≤ f (u.length + 1)) (hdiv : ∑' (t : ℕ), ENNReal.ofReal (Real.exp (-f (t + 1))) = ⊤) (u : List α) (o : Option α) : InformationTheory.surprisal (Surprisal.nextWord (softmaxModel d).stringMeasure id u) o = d o u + Real.log (∑ o' : Option α, Real.exp (-d o' u))

Under a tight softmax model, the surprisal of a unit under the next-unit law of the language model is the difficulty plus the log partition function of the prefix.

theorem Cotterell2026.exists_isTight_difficulty_eq_surprisal {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {d : Option α → List α → ℝ} (hd : ∀ (o : Option α) (u : List α), 0 ≤ d o u) {f : ℕ → ℝ} (hf : ∀ (u : List α), d none u ≤ f (u.length + 1)) (hdiv : ∑' (t : ℕ), ENNReal.ofReal (Real.exp (-f (t + 1))) = ⊤) : ∃ (M : AutoregressiveSequenceModel α), M.IsTight ∧ ∃ (b : List α → ℝ), ∀ (o : Option α) (u : List α), d o u = InformationTheory.surprisal (Surprisal.nextWord M.stringMeasure id u) o + b u

The tautology: a nonnegative difficulty measure whose end difficulty is bounded along a series with divergent exponentials is the surprisal of the next unit under some language model, up to a context-dependent baseline.

theorem Cotterell2026.lintegral_length_softmaxModel_le {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {d : Option α → List α → ℝ} (hd : ∀ (o : Option α) (u : List α), 0 ≤ d o u) {C : ℝ} (hC : ∀ (u : List α), d none u ≤ C) : ∫⁻ (x : List α), ↑x.length ∂(softmaxModel d).stringMeasure ≤ (1 - ENNReal.ofReal (Real.exp (-C)) / ↑(Fintype.card (Option α))) / (ENNReal.ofReal (Real.exp (-C)) / ↑(Fintype.card (Option α)))

Proposition 1(b): a constant bound C on the end difficulty bounds the expected length of the softmax model by (1 - η) / η, for η = exp (-C) over the size of the extended alphabet.

theorem Cotterell2026.lintegral_length_softmaxModel_ne_top {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {d : Option α → List α → ℝ} (hd : ∀ (o : Option α) (u : List α), 0 ≤ d o u) {C : ℝ} (hC : ∀ (u : List α), d none u ≤ C) : ∫⁻ (x : List α), ↑x.length ∂(softmaxModel d).stringMeasure ≠ ⊤

The softmax model of a bounded end difficulty has finite expected length.