Dong et al. (2026): Value of Information: A Framework for Human–Agent Communication

This file formalizes the clarify-or-commit policy of [DHH+26]. An agent holds a belief b over a user's latent intent θ, may commit to an action a of utility U(θ, a), or may ask a closed-ended question q whose answer y it predicts by an answer model p(y ∣ q, θ) and which costs the user c. The expected utility of committing, (1), is an integral against the belief, and the value of acting now, (2), is its best value, decisionValue. The value of a question, (3), is the answer-marginal expectation of the value of the posterior belief, so the value of information, (4), VoI(q) = Vpost(b, q) − V(b), is the value of information of the question as an experiment under the decision value, the notion the paper takes from [RS61], and the net value, (5), subtracts the cost. The agent clarifies with a question of positive net value and commits when none has one. Information cannot have negative value, voi_nonneg, so an uninformative question is never asked, not_clarifies_of_const; scaling the stakes scales the value of information, voi_smul, so a question worth asking at low stakes is worth asking at higher stakes, clarifies_smul, and a costlier question is asked less, clarifies_of_le. Appendix A shows this risk awareness on its 20 Questions task, where a correct animal guess is worth 1 and a correct diagnosis 10; appendixA reproduces the contrast on a two-candidate task with a yes/no question of reliability r, whose value of information is r − 1/2 by voi_reliability.

Implementation notes

The belief is a probability measure on intents and each question an answer kernel, so (1) to (4) are integrals, posteriors and values of information of the library, and the clarify-or-commit decision is the only new object. The policy's choice among the questions of positive net value, the sequential loop of Algorithm 1 with its clarification budget and linear cost T · c, and the language-model estimates of belief and answer distributions of §4.2 are not represented: the theorems concern the decision at one turn, at a fixed belief. Stakes are a scalar on the utility. The two-candidate task and the reliability 27/50 are this file's illustration, not the paper's.

References

• [DHH+26]
• [RS61]

The value of information and the clarify-or-commit decision, (3) to (5)

noncomputable def DongEtAl2026.postValue {Θ : Type u_1} {A : Type u_2} {Q : Type u_3} {Y : Type u_4} [MeasurableSpace Θ] [MeasurableSpace Y] [StandardBorelSpace Θ] [Nonempty Θ] (U : Θ → A → ℝ) (b : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure b] (P : Q → ProbabilityTheory.Kernel Θ Y) [∀ (q : Q), ProbabilityTheory.IsMarkovKernel (P q)] (q : Q) : ℝ

The value of asking question q, (3), is the expected value of the posterior belief.

Equations

• DongEtAl2026.postValue U b P q = ∫ (y : Y), ProbabilityTheory.decisionValue U ((ProbabilityTheory.posterior (P q) b) y) ∂b.bind ⇑(P q)

noncomputable def DongEtAl2026.voi {Θ : Type u_1} {A : Type u_2} {Q : Type u_3} {Y : Type u_4} [MeasurableSpace Θ] [MeasurableSpace Y] [StandardBorelSpace Θ] [Nonempty Θ] (U : Θ → A → ℝ) (b : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure b] (P : Q → ProbabilityTheory.Kernel Θ Y) [∀ (q : Q), ProbabilityTheory.IsMarkovKernel (P q)] (q : Q) : ℝ

The value of information of question q, (4), is the value of information of the question as an experiment under the decision value.

Equations

• DongEtAl2026.voi U b P q = ProbabilityTheory.valueOfInformation (ProbabilityTheory.decisionValue U) (P q) b

theorem DongEtAl2026.voi_eq {Θ : Type u_1} {A : Type u_2} {Q : Type u_3} {Y : Type u_4} [MeasurableSpace Θ] [MeasurableSpace Y] [StandardBorelSpace Θ] [Nonempty Θ] (U : Θ → A → ℝ) (b : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure b] (P : Q → ProbabilityTheory.Kernel Θ Y) [∀ (q : Q), ProbabilityTheory.IsMarkovKernel (P q)] (q : Q) : voi U b P q = postValue U b P q - ProbabilityTheory.decisionValue U b

noncomputable def DongEtAl2026.netVoi {Θ : Type u_1} {A : Type u_2} {Q : Type u_3} {Y : Type u_4} [MeasurableSpace Θ] [MeasurableSpace Y] [StandardBorelSpace Θ] [Nonempty Θ] (U : Θ → A → ℝ) (b : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure b] (P : Q → ProbabilityTheory.Kernel Θ Y) [∀ (q : Q), ProbabilityTheory.IsMarkovKernel (P q)] (c : ℝ) (q : Q) : ℝ

The net value of information of question q at cost c, (5), is its value of information less the cost.

Equations

• DongEtAl2026.netVoi U b P c q = DongEtAl2026.voi U b P q - c

def DongEtAl2026.Clarifies {Θ : Type u_1} {A : Type u_2} {Q : Type u_3} {Y : Type u_4} [MeasurableSpace Θ] [MeasurableSpace Y] [StandardBorelSpace Θ] [Nonempty Θ] (U : Θ → A → ℝ) (b : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure b] (P : Q → ProbabilityTheory.Kernel Θ Y) [∀ (q : Q), ProbabilityTheory.IsMarkovKernel (P q)] (c : ℝ) (questions : Finset Q) : Prop

The agent clarifies when some question of questions has positive net value, and commits otherwise.

Equations

• DongEtAl2026.Clarifies U b P c questions = ∃ q ∈ questions, 0 < DongEtAl2026.netVoi U b P c q

theorem DongEtAl2026.not_clarifies_iff {Θ : Type u_1} {A : Type u_2} {Q : Type u_3} {Y : Type u_4} [MeasurableSpace Θ] [MeasurableSpace Y] [StandardBorelSpace Θ] [Nonempty Θ] (U : Θ → A → ℝ) (b : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure b] (P : Q → ProbabilityTheory.Kernel Θ Y) [∀ (q : Q), ProbabilityTheory.IsMarkovKernel (P q)] (c : ℝ) (questions : Finset Q) : ¬Clarifies U b P c questions ↔ ∀ q ∈ questions, netVoi U b P c q ≤ 0

theorem DongEtAl2026.not_clarifies_iff_sup'_le {Θ : Type u_1} {A : Type u_2} {Q : Type u_3} {Y : Type u_4} [MeasurableSpace Θ] [MeasurableSpace Y] [StandardBorelSpace Θ] [Nonempty Θ] (U : Θ → A → ℝ) (b : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure b] (P : Q → ProbabilityTheory.Kernel Θ Y) [∀ (q : Q), ProbabilityTheory.IsMarkovKernel (P q)] (c : ℝ) {questions : Finset Q} (h : questions.Nonempty) : ¬Clarifies U b P c questions ↔ questions.sup' h (netVoi U b P c) ≤ 0

By the paper's commit rule, the agent commits exactly when the best net value is at most 0.

theorem DongEtAl2026.value_add_lt_postValue {Θ : Type u_1} {A : Type u_2} {Q : Type u_3} {Y : Type u_4} [MeasurableSpace Θ] [MeasurableSpace Y] [StandardBorelSpace Θ] [Nonempty Θ] (U : Θ → A → ℝ) (b : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure b] (P : Q → ProbabilityTheory.Kernel Θ Y) [∀ (q : Q), ProbabilityTheory.IsMarkovKernel (P q)] {c : ℝ} {q : Q} (h : 0 < netVoi U b P c q) : ProbabilityTheory.decisionValue U b + c < postValue U b P q

Clarifying with a question of positive net value raises the expected utility net of its cost above the value of committing now.

theorem DongEtAl2026.clarifies_of_le {Θ : Type u_1} {A : Type u_2} {Q : Type u_3} {Y : Type u_4} [MeasurableSpace Θ] [MeasurableSpace Y] [StandardBorelSpace Θ] [Nonempty Θ] (U : Θ → A → ℝ) (b : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure b] (P : Q → ProbabilityTheory.Kernel Θ Y) [∀ (q : Q), ProbabilityTheory.IsMarkovKernel (P q)] {c c' : ℝ} (hcc' : c ≤ c') {questions : Finset Q} (h : Clarifies U b P c' questions) : Clarifies U b P c questions

A costlier question is asked less: the clarifying region shrinks as the cost rises.

theorem DongEtAl2026.voi_smul {Θ : Type u_1} {A : Type u_2} {Q : Type u_3} {Y : Type u_4} [MeasurableSpace Θ] [MeasurableSpace Y] [StandardBorelSpace Θ] [Nonempty Θ] (U : Θ → A → ℝ) (b : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure b] (P : Q → ProbabilityTheory.Kernel Θ Y) [∀ (q : Q), ProbabilityTheory.IsMarkovKernel (P q)] {s : ℝ} (hs : 0 ≤ s) (q : Q) : voi (s • U) b P q = s * voi U b P q

Scaling the stakes scales the value of information.

theorem DongEtAl2026.not_clarifies_of_const {Θ : Type u_1} {A : Type u_2} {Q : Type u_3} {Y : Type u_4} [MeasurableSpace Θ] [MeasurableSpace Y] [StandardBorelSpace Θ] [Nonempty Θ] (U : Θ → A → ℝ) (b : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure b] (P : Q → ProbabilityTheory.Kernel Θ Y) [∀ (q : Q), ProbabilityTheory.IsMarkovKernel (P q)] {c : ℝ} (hc : 0 ≤ c) {questions : Finset Q} (hP : ∀ q ∈ questions, ∃ (ν : MeasureTheory.Measure Y), P q = ProbabilityTheory.Kernel.const Θ ν) : ¬Clarifies U b P c questions

Uninformative questions are never asked, at any nonnegative cost.

theorem DongEtAl2026.voi_nonneg {Θ : Type u_1} {A : Type u_2} {Q : Type u_3} {Y : Type u_4} [MeasurableSpace Θ] [MeasurableSpace Y] [StandardBorelSpace Θ] [Nonempty Θ] (U : Θ → A → ℝ) (b : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure b] (P : Q → ProbabilityTheory.Kernel Θ Y) [∀ (q : Q), ProbabilityTheory.IsMarkovKernel (P q)] [Finite Θ] [MeasurableSingletonClass Y] [Finite Y] [Finite A] (q : Q) : 0 ≤ voi U b P q

Information cannot have negative value.

theorem DongEtAl2026.clarifies_smul {Θ : Type u_1} {A : Type u_2} {Q : Type u_3} {Y : Type u_4} [MeasurableSpace Θ] [MeasurableSpace Y] [StandardBorelSpace Θ] [Nonempty Θ] (U : Θ → A → ℝ) (b : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure b] (P : Q → ProbabilityTheory.Kernel Θ Y) [∀ (q : Q), ProbabilityTheory.IsMarkovKernel (P q)] [Finite Θ] [MeasurableSingletonClass Y] [Finite Y] [Finite A] {s s' : ℝ} (hs : 0 ≤ s) (hss' : s ≤ s') {c : ℝ} {questions : Finset Q} (h : Clarifies (s • U) b P c questions) : Clarifies (s' • U) b P c questions

A question worth asking at stakes s is worth asking at any higher stakes s': the commit-without-asking region shrinks as the stakes rise.

A two-candidate task with a yes/no question

def DongEtAl2026.correct (θ a : Bool) : ℝ

A correct guess is worth 1 and an incorrect one 0.

Equations

• DongEtAl2026.correct θ a = if a = θ then 1 else 0

def DongEtAl2026.answer (r : ℝ) (θ y : Bool) : ℝ

answer r θ y is the probability that a yes/no question of reliability r answers y at θ.

Equations

• DongEtAl2026.answer r θ y = if y = θ then r else 1 - r

noncomputable def DongEtAl2026.question (r : ℝ) : ProbabilityTheory.Kernel Bool Bool

A yes/no question of reliability r answers correctly with probability r.

Equations

• DongEtAl2026.question r = ProbabilityTheory.Kernel.ofFunOfCountable fun (θ : Bool) => ∑ y : Bool, ENNReal.ofReal (DongEtAl2026.answer r θ y) • MeasureTheory.Measure.dirac y

theorem DongEtAl2026.decisionValue_correct (μ : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.decisionValue correct μ = max (μ.real {true}) (μ.real {false})

theorem DongEtAl2026.answer_nonneg {r : ℝ} (h₀ : 0 ≤ r) (h₁ : r ≤ 1) (θ y : Bool) : 0 ≤ answer r θ y

theorem DongEtAl2026.question_real_singleton {r : ℝ} (h₀ : 0 ≤ r) (h₁ : r ≤ 1) (θ y : Bool) : ((question r) θ).real {y} = answer r θ y

theorem DongEtAl2026.isMarkovKernel_question {r : ℝ} (h₀ : 0 ≤ r) (h₁ : r ≤ 1) : ProbabilityTheory.IsMarkovKernel (question r)

theorem DongEtAl2026.comp_question_real {r : ℝ} (h₀ : 0 ≤ r) (h₁ : r ≤ 1) (y : Bool) : ((ProbabilityTheory.uniformOn Set.univ).bind ⇑(question r)).real {y} = 1 / 2

Each answer has marginal probability 1/2 under the uniform belief.

theorem DongEtAl2026.posterior_question_real {r : ℝ} (h₀ : 0 ≤ r) (h₁ : r ≤ 1) (y θ : Bool) : ((ProbabilityTheory.posterior (question r) (ProbabilityTheory.uniformOn Set.univ)) y).real {θ} = answer r θ y

After answer y, the posterior puts the reliability r on the answered candidate.

theorem DongEtAl2026.voi_reliability {r : ℝ} (h₀ : 0 ≤ r) (h₁ : r ≤ 1) (hr : 1 / 2 ≤ r) : ProbabilityTheory.valueOfInformation (ProbabilityTheory.decisionValue correct) (question r) (ProbabilityTheory.uniformOn Set.univ) = r - 1 / 2

The value of information of a yes/no question of reliability r ≥ 1/2 on a two-candidate task is r − 1/2.

theorem DongEtAl2026.appendixA : ¬Clarifies correct (ProbabilityTheory.uniformOn Set.univ) (fun (x : Unit) => question (27 / 50)) (1 / 20) {()} ∧ Clarifies (10 • correct) (ProbabilityTheory.uniformOn Set.univ) (fun (x : Unit) => question (27 / 50)) (1 / 20) {()}

As in Appendix A, at cost 1/20 a question of reliability 27/50 is skipped when a correct guess is worth 1 and asked when it is worth 10.