Optimal Experiment Design @cite{lindley-1956}

@cite{hawkins-etal-2025} @cite{van-rooy-2003}

Domain-general framework for optimal experiment design: selecting experiments (questions, stimuli, tests) to maximize expected information gain (EIG).

Architecture

An experiment designer faces the same problem as a scientist planning an experiment: given prior beliefs about the world, which experiment will be most informative? The answer depends on three components:

1. Observation model P(o|w,e): how experiments generate observations
2. Bayesian posterior P(w|o,e): updated beliefs after observing
3. Value function V(posterior): how good is holding those beliefs

EIG(e) = E_o[V(posterior(·|o,e))] − V(prior)

This IS the structure of PRIOR-PQ's questioner Q (@cite{hawkins-etal-2025}, eq. 2.3): question = experiment, R₀'s response = observation, V(D^{r,q}) = expected decision value. Formalizing this connection shows that question selection is a special case of optimal experiment design.

Relationship to existing infrastructure

The Core.DecisionTheory module formalizes @cite{van-rooy-2003}'s EUV for deterministic observations (partition cells). This module generalizes to stochastic observations, with a bridge theorem showing that EIG with deterministic observations recovers EUV.

This module (ℝ, stochastic)	DecisionTheory (ℚ, deterministic)
ObservationModel	Question W (partition cells)
marginalObs	cellProbability
posterior	conditioning on cell membership
dpValueR	valueAfterLearning / dpValue
eig	questionUtility (EUV)
optimalExperiment	(no softmax wrapper in DecisionTheory)

Bayesian infrastructure

The ObservationModel, posterior, marginalObs, and their basic properties (posterior_nonneg, posterior_sum_one, posterior_marginalizes_to_prior) live in Core.Agent.BayesianUpdate and are re-exported here.

noncomputable def Core.ExperimentDesign.eig {W : Type u_1} {E : Type u_2} {O : Type u_3} [Fintype W] [Fintype O] (om : ObservationModel W E O) (prior : W → ℝ) (valueFn : (W → ℝ) → ℝ) (e : E) : ℝ

Expected information gain of experiment e relative to value function V:

EIG(e) = Σ_o P(o|e) · V(posterior(·|o,e)) − V(prior)

When V = max_a EU(a), this is the expected value of the experiment (generalization of Van Rooy's EUV from partitions to stochastic observations).

When V = −H(·) (negative entropy), this is the mutual information I(W;O|e), which equals @cite{lindley-1956}'s expected information gain.

Equations

• Core.ExperimentDesign.eig om prior valueFn e = ∑ o : O, Core.BayesianUpdate.marginalObs om prior e o * valueFn (Core.BayesianUpdate.posterior om prior e o) - valueFn prior

noncomputable def Core.ExperimentDesign.optimalExperiment {W : Type u_1} {E : Type u_2} {O : Type u_3} [Fintype W] [Fintype O] [Fintype E] (om : ObservationModel W E O) (prior : W → ℝ) (valueFn : (W → ℝ) → ℝ) (α : ℝ) : RationalAction Unit E

An optimal experiment designer: selects experiments with probability ∝ exp(α · EIG). This is a RationalAction whose state is Unit (stateless selector) and whose action space is the set of experiments E.

Connects experiment design to the Luce choice rule (§1 of RationalAction.lean): the designer soft-maximizes EIG with rationality parameter α.

Equations

• Core.ExperimentDesign.optimalExperiment om prior valueFn α = { score := fun (x : Unit) (e : E) => Real.exp (α * Core.ExperimentDesign.eig om prior valueFn e), score_nonneg := ⋯ }

noncomputable def Core.ExperimentDesign.dpValueR {W : Type u_1} [Fintype W] {A : Type u_4} (utility : W → A → ℝ) (actions : List A) : (W → ℝ) → ℝ

Decision-theoretic value function over ℝ: the value of holding beliefs post is the EU of the optimal action under those beliefs.

V(post) = max_a Σ_w post(w) · U(w,a)

This is the ℝ analog of DecisionTheory.dpValue. The connection to PRIOR-PQ: V(beliefs) = E_D[max_item Σ_w beliefs(w) · V(D, item)], where the outer expectation over D is folded into the utility function.

Equations

• Core.ExperimentDesign.dpValueR utility actions post = List.foldl (fun (best : ℝ) (a : A) => max best (∑ w : W, post w * utility w a)) 0 actions

theorem Core.ExperimentDesign.eig_deterministic_eq_euv {W : Type u_1} {O : Type u_3} [Fintype W] [Fintype O] [DecidableEq O] [DecidableEq W] {A : Type u_4} (classify : W → O) (utility : W → A → ℝ) (prior : W → ℝ) (_hprior : ∀ (w : W), 0 ≤ prior w) (_hprior_sum : ∑ w : W, prior w = 1) (actions : List A) : eig (deterministicObs classify) prior (dpValueR utility actions) () = ∑ o : O, marginalObs (deterministicObs classify) prior () o * dpValueR utility actions (posterior (deterministicObs classify) prior () o) - dpValueR utility actions prior

When observations are deterministic (partition cells), EIG equals Van Rooy's expected utility value (EUV).

The proof requires showing that the ℝ-valued Bayesian posterior on partition cells is equivalent to the ℚ-valued conditional EU in DecisionTheory.questionUtility.

TODO: The bridge requires converting between ℝ and ℚ arithmetic and showing that posterior with indicator likelihoods reduces to conditioning on the cell {w | classify w = o}.

theorem Core.ExperimentDesign.marginalObs_sum {W : Type u_1} {E : Type u_2} {O : Type u_3} [Fintype W] [Fintype O] (om : ObservationModel W E O) (prior : W → ℝ) (e : E) : ∑ o : O, marginalObs om prior e o = ∑ w : W, prior w

Marginal observation probabilities sum to the total prior mass: Σ_o P(o|e) = Σ_w prior(w).

theorem Core.ExperimentDesign.eig_nonneg_of_convex {W : Type u_1} {E : Type u_2} {O : Type u_3} [Fintype W] [Fintype O] (om : ObservationModel W E O) (prior : W → ℝ) (valueFn : (W → ℝ) → ℝ) (e : E) (hprior : ∀ (w : W), 0 ≤ prior w) (hprior_sum : ∑ w : W, prior w = 1) (hconvex : ∀ (f g : W → ℝ) (t : ℝ), 0 ≤ t → t ≤ 1 → (valueFn fun (w : W) => t * f w + (1 - t) * g w) ≤ t * valueFn f + (1 - t) * valueFn g) : 0 ≤ eig om prior valueFn e

EIG is non-negative when V is convex (Jensen's inequality).

For convex V: E[V(posterior)] ≥ V(E[posterior]) = V(prior). The posterior averages back to the prior (by posterior_marginalizes_to_prior): Σ_o P(o|e) · posterior(w|o,e) = prior(w).

Jensen's inequality then gives V(prior) ≤ E_o[V(posterior)], hence EIG ≥ 0.