Monte Carlo estimation of generalized surprisal

Generalized surprisal warps an expectation over the alternatives a language model samples, and [GOC24] estimate it by warping the mean score of finitely many sampled alternatives. The estimator is consistent when the warping is continuous: by the strong law of large numbers the mean score converges almost surely to the expected score (ae_tendsto_mcEstimate). With the identity warping it is also unbiased (integral_mcEstimate_id).

Main definitions

• mcEstimate: the warped mean score of the first N alternatives.

Main results

• ae_tendsto_mcEstimate: consistency for a warping continuous at the expected score.
• integral_mcEstimate_id: unbiasedness for the identity warping.

Implementation notes

• The alternatives are random variables on a probability space, each distributed as the language model in the context; the paper draws them by ancestral sampling. Consistency assumes them pairwise independent, the hypothesis of mathlib's strong law.
• Consistency needs the warping continuous only at the expected score, where the paper assumes it continuous.

References

• [GOC24]

noncomputable def Surprisal.mcEstimate {C : Type u_1} {A : Type u_2} {W : Type u_3} (f : ℝ → ℝ) (g : A → W → C → ℝ) (c : C) (w : W) (v : ℕ → A) (N : ℕ) : ℝ

The Monte Carlo estimate of generalized surprisal from the first N alternatives v: the warping f of their mean score against the target w in the context c.

Equations

• Surprisal.mcEstimate f g c w v N = f ((↑N)⁻¹ * ∑ n ∈ Finset.range N, g (v n) w c)

theorem Surprisal.ae_tendsto_mcEstimate {C : Type u_1} {A : Type u_2} {W : Type u_3} [MeasurableSpace C] [MeasurableSpace A] {Ω : Type u_4} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {L : ProbabilityTheory.Kernel C A} {g : A → W → C → ℝ} {c : C} {w : W} {V : ℕ → Ω → A} {f : ℝ → ℝ} (hV : ∀ (n : ℕ), Measurable (V n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (V n) P = L c) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (V i) (V j) P) (hg : Measurable fun (a : A) => g a w c) (hint : MeasureTheory.Integrable (fun (a : A) => g a w c) (L c)) (hf : ContinuousAt f (∫ (a : A), g a w c ∂L c)) : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (N : ℕ) => mcEstimate f g c w (fun (n : ℕ) => V n ω) N) Filter.atTop (nhds (genSurprisal L f g c w))

The Monte Carlo estimate is consistent: for pairwise independent alternatives distributed as the language model and a warping continuous at the expected score, it converges almost surely to the generalized surprisal.

theorem Surprisal.integral_mcEstimate_id {C : Type u_1} {A : Type u_2} {W : Type u_3} [MeasurableSpace C] [MeasurableSpace A] {Ω : Type u_4} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {L : ProbabilityTheory.Kernel C A} {g : A → W → C → ℝ} {c : C} {w : W} {V : ℕ → Ω → A} (hV : ∀ (n : ℕ), Measurable (V n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (V n) P = L c) (hint : MeasureTheory.Integrable (fun (a : A) => g a w c) (L c)) {N : ℕ} (hN : N ≠ 0) : ∫ (ω : Ω), mcEstimate id g c w (fun (n : ℕ) => V n ω) N ∂P = genSurprisal L id g c w

With the identity warping, the Monte Carlo estimate from N ≠ 0 alternatives distributed as the language model is unbiased.