Generalised Surprisal and Incremental Alternative Sampling

@cite{giulianelli-etal-2026}

Parameterized family of processing difficulty measures that decomposes prediction into explicit temporal and representational dimensions, generalizing standard surprisal.

Standard surprisal treats prediction error as a single scalar (−log P(next word)). The generalised framework disentangles this into:

1. A warping function f mapping expected scores to processing measures
2. A scoring function g measuring how well alternatives match the target
3. A forecast horizon h: how many future symbols are considered
4. A representational level: the abstraction at which alternatives are compared

Standard surprisal is the special case (negLog, indicator, 1, predictive). Incremental information value is the family (identity, distance, h, l).

Main definitions

• SurprisalConfig: Complete generalised surprisal specification
• standardSurprisal: The configuration corresponding to @cite{levy-2008}
• informationValue: The IAS configuration at a given (horizon, level)
• PsychMeasure: Standard psycholinguistic response types
• ias_recovers_surprisal: Standard surprisal is a special case of IAS

Connection to existing infrastructure

• Core.InformationTheory.conditionalEntropy computes H(W|M), the expected surprisal under bounded memory
• Core.Divergence.kl_pointMass_eq_neg_log: KL with point mass = surprisal
• Core.ProcessingModel.ProcessingProfile: multi-dimensional processing cost, which IAS motivates decomposing by temporal and representational resolution

inductive Core.GeneralisedSurprisal.WarpingFn : Type

Warping functions mapping expected scores to processing measures. γ(w;c) = f(E[g(a,w,c)]).

• negLog : WarpingFn

  f(x) = −log(x): standard surprisal (bits)

• identity : WarpingFn

  f(x) = x: information value (raw expected distance)

instance Core.GeneralisedSurprisal.instDecidableEqWarpingFn : DecidableEq WarpingFn

Equations

• Core.GeneralisedSurprisal.instDecidableEqWarpingFn x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.GeneralisedSurprisal.instBEqWarpingFn.beq : WarpingFn → WarpingFn → Bool

Equations

• Core.GeneralisedSurprisal.instBEqWarpingFn.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.GeneralisedSurprisal.instBEqWarpingFn : BEq WarpingFn

Equations

• Core.GeneralisedSurprisal.instBEqWarpingFn = { beq := Core.GeneralisedSurprisal.instBEqWarpingFn.beq }

def Core.GeneralisedSurprisal.instReprWarpingFn.repr : WarpingFn → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Core.GeneralisedSurprisal.instReprWarpingFn : Repr WarpingFn

Equations

• Core.GeneralisedSurprisal.instReprWarpingFn = { reprPrec := Core.GeneralisedSurprisal.instReprWarpingFn.repr }

inductive Core.GeneralisedSurprisal.ScoringFn : Type

Scoring functions measuring prediction accuracy. g(a, w, c) evaluates alternative a against target w in context c.

• indicator : ScoringFn

  𝟙{w ≤ a}: binary prefix match. With negLog → standard surprisal.

• distance : ScoringFn

  d_r(a, w): representational distance. With identity → information value.

• similarity : ScoringFn

  sim(r(a), r(w)): semantic similarity. @cite{meister-giulianelli-pimentel-2024}

instance Core.GeneralisedSurprisal.instDecidableEqScoringFn : DecidableEq ScoringFn

Equations

• Core.GeneralisedSurprisal.instDecidableEqScoringFn x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.GeneralisedSurprisal.instBEqScoringFn.beq : ScoringFn → ScoringFn → Bool

Equations

• Core.GeneralisedSurprisal.instBEqScoringFn.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.GeneralisedSurprisal.instBEqScoringFn : BEq ScoringFn

Equations

• Core.GeneralisedSurprisal.instBEqScoringFn = { beq := Core.GeneralisedSurprisal.instBEqScoringFn.beq }

def Core.GeneralisedSurprisal.instReprScoringFn.repr : ScoringFn → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Core.GeneralisedSurprisal.instReprScoringFn : Repr ScoringFn

Equations

• Core.GeneralisedSurprisal.instReprScoringFn = { reprPrec := Core.GeneralisedSurprisal.instReprScoringFn.repr }

@[reducible, inline]

abbrev Core.GeneralisedSurprisal.ForecastHorizon : Type

Forecast horizon: how many future symbols each alternative spans. h = 1 is standard surprisal's implicit horizon (next word only).

Equations

• Core.GeneralisedSurprisal.ForecastHorizon = Nat

inductive Core.GeneralisedSurprisal.RepLevel : Type

Representational level at which predictions are evaluated.

Different layers of a neural language model capture different levels of linguistic processing. The key finding is that the most predictive level varies by psycholinguistic measure: lexical identity layers best predict explicit predictability; intermediate layers best predict reading times.

• lexical : RepLevel

  Layer 0 / embedding: decontextualized lexical identity

• shallowSyntactic : RepLevel

  Early-to-intermediate layers: shallow syntactic processing

• syntactic : RepLevel

  Intermediate layers: deep syntactic, shallow semantic

• semantic : RepLevel

  Deep layers: fully contextualized semantics

• predictive : RepLevel

  Final layer: specialized for next-token prediction

instance Core.GeneralisedSurprisal.instDecidableEqRepLevel : DecidableEq RepLevel

Equations

• Core.GeneralisedSurprisal.instDecidableEqRepLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.GeneralisedSurprisal.instBEqRepLevel.beq : RepLevel → RepLevel → Bool

Equations

• Core.GeneralisedSurprisal.instBEqRepLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.GeneralisedSurprisal.instBEqRepLevel : BEq RepLevel

Equations

• Core.GeneralisedSurprisal.instBEqRepLevel = { beq := Core.GeneralisedSurprisal.instBEqRepLevel.beq }

def Core.GeneralisedSurprisal.instReprRepLevel.repr : RepLevel → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Core.GeneralisedSurprisal.instReprRepLevel : Repr RepLevel

Equations

• Core.GeneralisedSurprisal.instReprRepLevel = { reprPrec := Core.GeneralisedSurprisal.instReprRepLevel.repr }

inductive Core.GeneralisedSurprisal.DistanceSummary : Type

How pairwise distances between alternative sets are aggregated.

Different summaries capture different notions of predictability: mean is the unbiased discrepancy estimate; min asks whether any hypothesis is close to the outcome; max captures worst-case error.

Key finding: under min, surprisal correlates most strongly with intermediate layers and medium horizons, revealing that surprisal's predictability is closest to a best-case (closest-hypothesis) notion rather than average discrepancy.

• mean : DistanceSummary

  Average pairwise distance. Equivalent to the original information value definition.

• min : DistanceSummary

  Minimum pairwise distance. Closest pre-observation hypothesis.

• max : DistanceSummary

  Maximum pairwise distance. Worst-case prediction error.

instance Core.GeneralisedSurprisal.instDecidableEqDistanceSummary : DecidableEq DistanceSummary

Equations

• Core.GeneralisedSurprisal.instDecidableEqDistanceSummary x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.GeneralisedSurprisal.instBEqDistanceSummary.beq : DistanceSummary → DistanceSummary → Bool

Equations

• Core.GeneralisedSurprisal.instBEqDistanceSummary.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.GeneralisedSurprisal.instBEqDistanceSummary : BEq DistanceSummary

Equations

• Core.GeneralisedSurprisal.instBEqDistanceSummary = { beq := Core.GeneralisedSurprisal.instBEqDistanceSummary.beq }

def Core.GeneralisedSurprisal.instReprDistanceSummary.repr : DistanceSummary → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Core.GeneralisedSurprisal.instReprDistanceSummary : Repr DistanceSummary

Equations

• Core.GeneralisedSurprisal.instReprDistanceSummary = { reprPrec := Core.GeneralisedSurprisal.instReprDistanceSummary.repr }

structure Core.GeneralisedSurprisal.SurprisalConfig : Type

A generalised surprisal model: the complete parameter set for a specific processing measure.

• warp : WarpingFn
• scoring : ScoringFn
• horizon : ForecastHorizon
• level : RepLevel

instance Core.GeneralisedSurprisal.instDecidableEqSurprisalConfig : DecidableEq SurprisalConfig

Equations

• Core.GeneralisedSurprisal.instDecidableEqSurprisalConfig = Core.GeneralisedSurprisal.instDecidableEqSurprisalConfig.decEq

def Core.GeneralisedSurprisal.instDecidableEqSurprisalConfig.decEq (x✝ x✝¹ : SurprisalConfig) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

instance Core.GeneralisedSurprisal.instBEqSurprisalConfig : BEq SurprisalConfig

Equations

• Core.GeneralisedSurprisal.instBEqSurprisalConfig = { beq := Core.GeneralisedSurprisal.instBEqSurprisalConfig.beq }

def Core.GeneralisedSurprisal.instBEqSurprisalConfig.beq : SurprisalConfig → SurprisalConfig → Bool

Equations

• One or more equations did not get rendered due to their size.
• Core.GeneralisedSurprisal.instBEqSurprisalConfig.beq x✝¹ x✝ = false

def Core.GeneralisedSurprisal.instReprSurprisalConfig.repr : SurprisalConfig → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Core.GeneralisedSurprisal.instReprSurprisalConfig : Repr SurprisalConfig

Equations

• Core.GeneralisedSurprisal.instReprSurprisalConfig = { reprPrec := Core.GeneralisedSurprisal.instReprSurprisalConfig.repr }

def Core.GeneralisedSurprisal.standardSurprisal : SurprisalConfig

Standard surprisal: −log P(next word). @cite{levy-2008} @cite{smith-levy-2013}

Equations

• One or more equations did not get rendered due to their size.

def Core.GeneralisedSurprisal.informationValue (h : ForecastHorizon) (l : RepLevel) : SurprisalConfig

Incremental information value at temporal-representational resolution (h, l). @cite{giulianelli-etal-2026}

Equations

• Core.GeneralisedSurprisal.informationValue h l = { warp := Core.GeneralisedSurprisal.WarpingFn.identity, scoring := Core.GeneralisedSurprisal.ScoringFn.distance, horizon := h, level := l }

inductive Core.GeneralisedSurprisal.PsychMeasure : Type

Standard psycholinguistic response types that index processing effort.

• predictabilityRating : PsychMeasure
• clozeProbability : PsychMeasure
• clozeSurprisal : PsychMeasure
• firstFixationRT : PsychMeasure
• firstPassRT : PsychMeasure
• rightBoundedRT : PsychMeasure
• goPastRT : PsychMeasure
• selfPacedRT : PsychMeasure
• n400 : PsychMeasure
• p600 : PsychMeasure

instance Core.GeneralisedSurprisal.instDecidableEqPsychMeasure : DecidableEq PsychMeasure

Equations

• Core.GeneralisedSurprisal.instDecidableEqPsychMeasure x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.GeneralisedSurprisal.instBEqPsychMeasure : BEq PsychMeasure

Equations

• Core.GeneralisedSurprisal.instBEqPsychMeasure = { beq := Core.GeneralisedSurprisal.instBEqPsychMeasure.beq }

def Core.GeneralisedSurprisal.instBEqPsychMeasure.beq : PsychMeasure → PsychMeasure → Bool

Equations

• Core.GeneralisedSurprisal.instBEqPsychMeasure.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.GeneralisedSurprisal.instReprPsychMeasure : Repr PsychMeasure

Equations

• Core.GeneralisedSurprisal.instReprPsychMeasure = { reprPrec := Core.GeneralisedSurprisal.instReprPsychMeasure.repr }

def Core.GeneralisedSurprisal.instReprPsychMeasure.repr : PsychMeasure → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Core.GeneralisedSurprisal.PsychMeasure.isExplicit : PsychMeasure → Bool

Explicit predictability judgements (cloze, rating) vs. implicit processing signatures (RTs, ERPs). Best-predicting IAS configurations differ between these classes: explicit measures peak at h = 1 with lexical-level representations; implicit measures benefit from longer horizons and intermediate representations.

Equations

• Core.GeneralisedSurprisal.PsychMeasure.predictabilityRating.isExplicit = true
• Core.GeneralisedSurprisal.PsychMeasure.clozeProbability.isExplicit = true
• Core.GeneralisedSurprisal.PsychMeasure.clozeSurprisal.isExplicit = true
• x✝.isExplicit = false

def Core.GeneralisedSurprisal.PsychMeasure.expectedSign : PsychMeasure → Int

Expected sign of the relationship between information value and measurement. Positive: higher info value → larger response. Negative: inverse.

Equations

• Core.GeneralisedSurprisal.PsychMeasure.predictabilityRating.expectedSign = -1
• Core.GeneralisedSurprisal.PsychMeasure.clozeProbability.expectedSign = -1
• Core.GeneralisedSurprisal.PsychMeasure.clozeSurprisal.expectedSign = 1
• Core.GeneralisedSurprisal.PsychMeasure.firstFixationRT.expectedSign = 1
• Core.GeneralisedSurprisal.PsychMeasure.firstPassRT.expectedSign = 1
• Core.GeneralisedSurprisal.PsychMeasure.rightBoundedRT.expectedSign = 1
• Core.GeneralisedSurprisal.PsychMeasure.goPastRT.expectedSign = 1
• Core.GeneralisedSurprisal.PsychMeasure.selfPacedRT.expectedSign = 1
• Core.GeneralisedSurprisal.PsychMeasure.n400.expectedSign = -1
• Core.GeneralisedSurprisal.PsychMeasure.p600.expectedSign = 1

theorem Core.GeneralisedSurprisal.ias_recovers_surprisal : (have __src := informationValue 1 RepLevel.predictive; { warp := WarpingFn.negLog, scoring := ScoringFn.indicator, horizon := __src.horizon, level := __src.level }) = standardSurprisal

Standard surprisal is IAS at horizon 1 with predictive-level representation and negLog/indicator replacing identity/distance. Subsumption by construction.