Generalized surprisal

This file defines the generalized surprisal of [GOC24]. A comprehender's language model is a Markov kernel from contexts to alternative continuations, and a generalized surprisal model is a pair of a warping function f : ℝ → ℝ and a scoring function g, which scores an alternative against the target in the context. The generalized surprisal of the target is the warped expected score. The score fixes what counts as an accurate prediction, and the warping the functional relationship between prediction accuracy and the measured cost, the question [SL13] ask of surprisal.

Surprisal [Lev08] is the model with the negative logarithm and the indicator score, and the next-unit probability the model with the identity and the indicator: every warping of the indicator score is a warping of the target's probability. Information value [GWF23], summarised by its mean, is the model with the identity and a distance score. A model is anticipatory when its score ignores the target and responsive otherwise, the distinction [PMW+23] draw informally for reading times; an anticipatory model assigns every target the same value, and entropy is the anticipatory model that scores each alternative by its own surprisal.

Main definitions

• genSurprisal L f g c w: the generalized surprisal of w in the context c.
• IsAnticipatory g: the score g is constant in the target.
• informationValue, indicatorScore.

Main results

• genSurprisal_indicatorScore, genSurprisal_negLog_indicatorScore: a warping of the indicator model is that warping of the target's probability; with the negative logarithm, the target's surprisal.
• IsAnticipatory.genSurprisal_eq: an anticipatory model does not depend on the target.
• not_isAnticipatory_indicatorScore: the indicator score is responsive.
• genSurprisal_id_surprisal: entropy is an anticipatory generalized surprisal.

References

• [GOC24]
• [GWF23]
• [Lev08]
• [PMW+23]
• [SL13]

noncomputable def Surprisal.genSurprisal {C : Type u_1} {A : Type u_2} {W : Type u_3} [MeasurableSpace C] [MeasurableSpace A] (L : ProbabilityTheory.Kernel C A) (f : ℝ → ℝ) (g : A → W → C → ℝ) (c : C) (w : W) : ℝ

The generalized surprisal of the target w in the context c under the model (f, g): the warping f of the expected score g a w c of the alternatives a that the language model L samples in the context.

Equations

• Surprisal.genSurprisal L f g c w = f (∫ (a : A), g a w c ∂L c)

noncomputable def Surprisal.informationValue {C : Type u_1} {A : Type u_2} {W : Type u_3} [MeasurableSpace C] [MeasurableSpace A] (L : ProbabilityTheory.Kernel C A) (d : A → W → C → ℝ) (c : C) (w : W) : ℝ

Information value with the mean as its summary statistic: the expected distance d from the alternatives to the target.

Equations

• Surprisal.informationValue L d c w = ∫ (a : A), d a w c ∂L c

theorem Surprisal.genSurprisal_id {C : Type u_1} {A : Type u_2} {W : Type u_3} [MeasurableSpace C] [MeasurableSpace A] (L : ProbabilityTheory.Kernel C A) (g : A → W → C → ℝ) (c : C) (w : W) : genSurprisal L id g c w = informationValue L g c w

The generalized surprisal with the identity warping is the expected score.

Anticipation and responsivity

def Surprisal.IsAnticipatory {C : Type u_1} {A : Type u_2} {W : Type u_3} (g : A → W → C → ℝ) : Prop

A scoring function is anticipatory when it is constant in the target, so that the model measures an uncertainty fixed by the context and the language model. A model whose score is not anticipatory is responsive.

Equations

• Surprisal.IsAnticipatory g = ∀ (a : A) (w w' : W) (c : C), g a w c = g a w' c

theorem Surprisal.IsAnticipatory.genSurprisal_eq {C : Type u_1} {A : Type u_2} {W : Type u_3} [MeasurableSpace C] [MeasurableSpace A] {g : A → W → C → ℝ} (hg : IsAnticipatory g) (L : ProbabilityTheory.Kernel C A) (f : ℝ → ℝ) (c : C) (w w' : W) : genSurprisal L f g c w = genSurprisal L f g c w'

An anticipatory model assigns every target the same value.

The indicator score

noncomputable def Surprisal.indicatorScore {C : Type u_1} {W : Type u_3} (a w : W) : C → ℝ

The indicator score: one when the alternative is the target.

Equations

• Surprisal.indicatorScore a w x✝ = {w}.indicator 1 a

theorem Surprisal.not_isAnticipatory_indicatorScore {C : Type u_1} {W : Type u_3} [Nontrivial W] [Nonempty C] : ¬IsAnticipatory indicatorScore

The indicator score is responsive.

theorem Surprisal.genSurprisal_indicatorScore {C : Type u_1} {W : Type u_3} [MeasurableSpace C] [MeasurableSpace W] [MeasurableSingletonClass W] (L : ProbabilityTheory.Kernel C W) (c : C) (w : W) (f : ℝ → ℝ) : genSurprisal L f indicatorScore c w = f ((L c).real {w})

A warping of the indicator model is that warping of the target's probability; with the identity it is the probability itself.

theorem Surprisal.genSurprisal_negLog_indicatorScore {C : Type u_1} {W : Type u_3} [MeasurableSpace C] [MeasurableSpace W] [MeasurableSingletonClass W] (L : ProbabilityTheory.Kernel C W) (c : C) (w : W) : genSurprisal L (fun (x : ℝ) => -Real.log x) indicatorScore c w = InformationTheory.surprisal (L c) w

Surprisal is the indicator model with the negative logarithm.

Entropy

theorem Surprisal.isAnticipatory_surprisal {C : Type u_1} {A : Type u_2} {W : Type u_3} [MeasurableSpace C] [MeasurableSpace A] (L : ProbabilityTheory.Kernel C A) : IsAnticipatory fun (a : A) (x : W) (c : C) => InformationTheory.surprisal (L c) a

Scoring each alternative by its own surprisal is anticipatory.

theorem Surprisal.genSurprisal_id_surprisal {C : Type u_1} {A : Type u_2} {W : Type u_3} [MeasurableSpace C] [MeasurableSpace A] [Countable A] [MeasurableSingletonClass A] (L : ProbabilityTheory.Kernel C A) [ProbabilityTheory.IsMarkovKernel L] (c : C) (hL : MeasureTheory.Integrable (InformationTheory.surprisal (L c)) (L c)) (w : W) : genSurprisal L id (fun (a : A) (x : W) (c : C) => InformationTheory.surprisal (L c) a) c w = InformationTheory.measureEntropy (L c)

Entropy is the anticipatory model with the identity warping that scores each alternative by its own surprisal.