Optimal Experiment Design [Lin56] #
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:
- Observation model
P(o|w,e): how experiments generate observations - Bayesian posterior
P(w|o,e): updated beliefs after observing - 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 ([HTB+25], 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 [vR03a]'s EUV for
deterministic observations (partition cells). This module generalizes
to stochastic observations; eig_deterministicObs_eq_euv proves that
EIG with deterministic observations recovers EUV (ℚ-cast, nonempty fibers).
The kernel-level Blackwell order behind both lives in
Core.Probability.Decision.Blackwell.
| This module (ℝ, stochastic) | DecisionTheory (ℚ, deterministic) |
|---|---|
ObservationModel | Question W (partition cells) |
marginalObs | cellProbability |
posterior | conditioning on cell membership |
dpValueR | condValue / DecisionProblem.value |
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/Probability/BayesianUpdate.lean and are re-exported here.
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 [Lin56]'s expected information gain.
Equations
- Core.eig om prior valueFn e = ∑ o : O, Core.marginalObs om prior e o * valueFn (Core.posterior om prior e o) - valueFn prior
Instances For
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.optimalExperiment om prior valueFn α = { score := fun (x : Unit) (e : E) => Real.exp (α * Core.eig om prior valueFn e), score_nonneg := ⋯ }
Instances For
Decision-theoretic value function over ℝ: the value of holding beliefs post
is the EU of the optimal action under those beliefs,
V(post) = maxₐ ∑_w post(w) · U(w,a) (0 if actions is empty).
The exact ℝ analog of DecisionTheory.DecisionProblem.value — same Finset.sup' shape,
so the deterministic-observation bridge (eig_deterministicObs_eq_euv)
matches definitionally cell by cell.
Equations
- Core.dpValueR utility actions post = if h : actions.Nonempty then actions.sup' h fun (a : A) => ∑ w : W, post w * utility w a else 0
Instances For
dpValueR is a support function, hence convex: the decision value
post ↦ maxₐ ∑_w post(w)·U(w,a) is a finite supremum of linear functionals of
the belief vector (convexOn_finset_sup' over LinearMap.proj-sums). The
convexity that every value-of-information inequality in this directory runs
on.
The deterministic-observation bridge, for real: with observations given by a
classifier classify : W → O whose fibers are all nonempty, the expected information
gain of the (single) deterministic experiment under the decision-theoretic value
function equals [vR03a]'s expected utility value of the corresponding
partition question — Core.DecisionTheory.DecisionProblem.questionUtility, cast from ℚ to ℝ.
The fiber-nonemptiness hypothesis keeps the Finset.image indexing faithful: empty
fibers would collapse in the cell set while still contributing (zero) terms to the
observation sum.
Marginal observation probabilities sum to the total prior mass: Σ_o P(o|e) = Σ_w prior(w).
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.
EIG of the decision value function is non-negative — Jensen applied to the support function: information cannot hurt an expected-utility maximizer ([Bla53]'s forward direction at the value level).