Prefix probabilities of a generative process

A generative process is a probability measure over complete structures together with their yields, and it induces probabilities on strings: the prefix probability of a string is the mass of the structures whose yield extends it ([Sto95]'s prefix probability, computed there by Earley parsing), and the conditional probability of the next word is the process conditioned on the prefix, at the structures consistent with the extended prefix. The law of the next word reads the conditioned process at the position after the prefix, with none where the yield ends there, and a word's surprisal is its surprisal under this law. This is the shared input of surprisal theory: [Hal01] defines word difficulty as the log-ratio of successive prefix probabilities, and [Lev08] proves that ratio equals the relative entropy of the induced belief update.

Main definitions

• consistent: the structures whose yield extends a prefix.
• nextProb: the induced conditional probability of the next word.
• nextWord: the law of the next word, none for the end of the yield.

Main results

• nextProb_eq_div: the next-word probability as a ratio of prefix probabilities.
• nextWord_singleton_some, nextWord_singleton_none: the law of the next word gives each word its conditional probability and the end the probability that the yield is the prefix.
• nextWord_stringMeasure: a tight autoregressive model's conditional distributions are the next-word laws of the language model it defines ([DTHP+23]).
• cond_consistent_append: the chain rule for conditional prefix probabilities.

References

• [Sto95]
• [Hal01]
• [Lev08]
• [DTHP+23]

def Surprisal.consistent {T : Type u_1} {W : Type u_2} (str : T → List W) (ws : List W) : Set T

The complete structures whose yield extends the prefix ws.

Equations

• Surprisal.consistent str ws = {t : T | ws <+: str t}

@[simp]

theorem Surprisal.consistent_nil {T : Type u_1} {W : Type u_2} (str : T → List W) : consistent str [] = Set.univ

theorem Surprisal.consistent_anti {T : Type u_1} {W : Type u_2} (str : T → List W) {ws ws' : List W} (h : ws <+: ws') : consistent str ws' ⊆ consistent str ws

Longer prefixes select fewer structures.

theorem Surprisal.measurableSet_consistent {T : Type u_1} {W : Type u_2} [MeasurableSpace T] (str : T → List W) [DiscreteMeasurableSpace T] (ws : List W) : MeasurableSet (consistent str ws)

noncomputable def Surprisal.nextProb {T : Type u_1} {W : Type u_2} [MeasurableSpace T] (P : MeasureTheory.Measure T) (str : T → List W) (ws : List W) (w : W) : ENNReal

The conditional probability of the next word w after the prefix ws under the process P: the process conditioned on the prefix, at the structures consistent with the extended prefix.

Equations

• Surprisal.nextProb P str ws w = P[Surprisal.consistent str (ws ++ [w]) | Surprisal.consistent str ws]

theorem Surprisal.nextProb_eq_div {T : Type u_1} {W : Type u_2} [MeasurableSpace T] (P : MeasureTheory.Measure T) (str : T → List W) [DiscreteMeasurableSpace T] (ws : List W) (w : W) : nextProb P str ws w = P (consistent str (ws ++ [w])) / P (consistent str ws)

The next-word probability as a ratio of prefix probabilities.

theorem Surprisal.cond_consistent_append {T : Type u_1} {W : Type u_2} [MeasurableSpace T] (P : MeasureTheory.Measure T) (str : T → List W) [DiscreteMeasurableSpace T] [MeasureTheory.IsFiniteMeasure P] (ws xs ys : List W) : P[consistent str (ws ++ xs ++ ys) | consistent str ws] = P[consistent str (ws ++ xs) | consistent str ws] * P[consistent str (ws ++ xs ++ ys) | consistent str (ws ++ xs)]

The chain rule: the probability of extending a prefix by xs ++ ys is the probability of extending it by xs times the probability of then extending by ys.

noncomputable def Surprisal.nextWord {T : Type u_1} {W : Type u_2} [MeasurableSpace T] (P : MeasureTheory.Measure T) (str : T → List W) [MeasurableSpace W] (ws : List W) : MeasureTheory.Measure (Option W)

The law of what follows the prefix ws: the process conditioned on the prefix, read at the position after it, with none where the yield ends.

Equations

• Surprisal.nextWord P str ws = MeasureTheory.Measure.map (fun (t : T) => (str t)[ws.length]?) P[|Surprisal.consistent str ws]

theorem Surprisal.nextWord_singleton_some {T : Type u_1} {W : Type u_2} [MeasurableSpace T] (P : MeasureTheory.Measure T) (str : T → List W) [MeasurableSpace W] [DiscreteMeasurableSpace T] [MeasurableSingletonClass W] (ws : List W) (w : W) : (nextWord P str ws) {some w} = nextProb P str ws w

The law of the next word gives a word its conditional probability.

theorem Surprisal.nextWord_singleton_none {T : Type u_1} {W : Type u_2} [MeasurableSpace T] (P : MeasureTheory.Measure T) (str : T → List W) [MeasurableSpace W] [DiscreteMeasurableSpace T] [MeasurableSingletonClass W] (ws : List W) : (nextWord P str ws) {none} = P[{t : T | str t = ws} | consistent str ws]

The law of the next word gives the end of the yield the probability that the yield is the prefix.

theorem Surprisal.nextWord_stringMeasure {W : Type u_2} [MeasurableSpace W] [MeasurableSingletonClass W] [Countable W] (M : AutoregressiveSequenceModel W) (hM : M.IsTight) {x : List W} (hx : M.prefixProb x ≠ 0) : nextWord M.stringMeasure id x = M.next x

A tight autoregressive model's conditional distribution after a prefix of positive probability is the next-word law of the language model it defines.