Tsvilodub, Mulligan, Snider, Hawkins and Franke (2026): Act or Clarify? Modeling Sensitivity to Uncertainty and Cost in Communication

The computational model of Experiment 1 explains when an agent asks a clarification question rather than answering under uncertainty. The questioner has one of two goals, with probability ε on the dispreferred one; a mention-some answer is worth 1 for its goal and 0 for the other, and the exhaustive answer is worth 1 − δ for either. The agent clarifies with a probability that is a logistic function of the expected regret of its best action, which is the value of learning the goal and van Rooy's value of the clarification question, min ε δ, and otherwise answers by a softmax policy over expected utility. Uncertainty therefore matters only while it stays below the cost of the exhaustive answer. With c read as the cost of asking, as the paper suggests, the gate softens the clarify-or-commit rule of Dong et al.

Main statements

• valueOfInformation_id_eq_expectedRegret: the expected regret of a best action is the value of perfect information.
• uncertainty_matters_most_when_costly: uncertainty raises clarification when the exhaustive answer is costly and leaves it unchanged when it is cheap.
• justListThemAll: with a cheap exhaustive answer, higher uncertainty means more exhaustive answers.
• half_lt_clarifyProb_iff: the gate favours clarifying exactly when Dong et al.'s agent would.

Implementation notes

• The gate reads the expected regret of the best action in its value form, the value of information of observing the goal, which needs no choice of a maximizer. The paper prints arg max in the regret where the maximum is meant.
• ε is a point of the unit interval and the prior is a Bernoulli measure; the paper's clamp ε ≤ 1/2 is a hypothesis. The softmax policy is the counting measure tilted by α · EU; the model has no listener.
• The fitted posterior means of Experiment 1 (ε of 0.17 and 0.49, δ of 0.11 and 0.32, τ of 3.60, c of 0.18) enter only through the orderings δ_S < ε_L < δ_L < ε_H ≤ 1/2. TooManyToList is not entailed: with a costly exhaustive answer, higher uncertainty raises both the gate and the policy's mass on the exhaustive answer, which pull the reaction's mass on it in opposite directions.
• Experiment 2, which the paper does not model, and the fit and model comparison are not formalized.

References

• [TMS+26]
• [RS61]
• [DHH+26]
• [vR03b]

Regret

noncomputable def TsvilodubEtAl2026.regret {W : Type u_1} {A : Type u_2} (U : W → A → ℝ) (w : W) (a : A) : ℝ

The regret of action a at world w is what the best action at w earns over a.

Equations

• TsvilodubEtAl2026.regret U w a = (⨆ (b : A), U w b) - U w a

noncomputable def TsvilodubEtAl2026.expectedRegret {W : Type u_1} {A : Type u_2} [MeasurableSpace W] (U : W → A → ℝ) (μ : MeasureTheory.Measure W) (a : A) : ℝ

The expected regret of action a averages its regret over the belief.

Equations

• TsvilodubEtAl2026.expectedRegret U μ a = ∫ (w : W), TsvilodubEtAl2026.regret U w a ∂μ

theorem TsvilodubEtAl2026.valueOfInformation_id_eq_expectedRegret {W : Type u_1} {A : Type u_2} [MeasurableSpace W] {U : W → A → ℝ} {μ : MeasureTheory.Measure W} [Finite W] [MeasurableSingletonClass W] [StandardBorelSpace W] [Nonempty W] [MeasureTheory.IsFiniteMeasure μ] {a : A} (ha : ∫ (w : W), U w a ∂μ = ProbabilityTheory.decisionValue U μ) : ProbabilityTheory.valueOfInformation (ProbabilityTheory.decisionValue U) ProbabilityTheory.Kernel.id μ = expectedRegret U μ a

The expected regret of a best action is the value of observing the world, the expected value of perfect information.

The decision problem

inductive TsvilodubEtAl2026.Goal : Type

The questioner's goal.

• g₁ : Goal
• g₂ : Goal

@[instance_reducible]

instance TsvilodubEtAl2026.instDecidableEqGoal : DecidableEq Goal

Equations

• TsvilodubEtAl2026.instDecidableEqGoal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TsvilodubEtAl2026.instReprGoal : Repr Goal

Equations

• TsvilodubEtAl2026.instReprGoal = { reprPrec := TsvilodubEtAl2026.instReprGoal.repr }

def TsvilodubEtAl2026.instReprGoal.repr : Goal → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TsvilodubEtAl2026.instFintypeGoal : Fintype Goal

Equations

• One or more equations did not get rendered due to their size.

instance TsvilodubEtAl2026.instNonemptyGoal : Nonempty Goal

@[instance_reducible]

instance TsvilodubEtAl2026.instMeasurableSpaceGoal : MeasurableSpace Goal

Equations

• TsvilodubEtAl2026.instMeasurableSpaceGoal = ⊤

instance TsvilodubEtAl2026.instDiscreteMeasurableSpaceGoal : DiscreteMeasurableSpace Goal

inductive TsvilodubEtAl2026.Response : Type

A direct answer is one of the two mention-some answers or the exhaustive answer.

• ms1 : Response
• ms2 : Response
• exh : Response

@[instance_reducible]

instance TsvilodubEtAl2026.instDecidableEqResponse : DecidableEq Response

Equations

• TsvilodubEtAl2026.instDecidableEqResponse x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TsvilodubEtAl2026.instReprResponse : Repr Response

Equations

• TsvilodubEtAl2026.instReprResponse = { reprPrec := TsvilodubEtAl2026.instReprResponse.repr }

def TsvilodubEtAl2026.instReprResponse.repr : Response → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TsvilodubEtAl2026.instFintypeResponse : Fintype Response

Equations

• One or more equations did not get rendered due to their size.

instance TsvilodubEtAl2026.instNonemptyResponse : Nonempty Response

@[instance_reducible]

instance TsvilodubEtAl2026.instMeasurableSpaceResponse : MeasurableSpace Response

Equations

• TsvilodubEtAl2026.instMeasurableSpaceResponse = ⊤

instance TsvilodubEtAl2026.instDiscreteMeasurableSpaceResponse : DiscreteMeasurableSpace Response

def TsvilodubEtAl2026.utility (δ : ℝ) : Goal → Response → ℝ

The utilities at exhaustive-answer cost δ.

Equations

• TsvilodubEtAl2026.utility δ TsvilodubEtAl2026.Goal.g₁ TsvilodubEtAl2026.Response.ms1 = 1
• TsvilodubEtAl2026.utility δ TsvilodubEtAl2026.Goal.g₁ TsvilodubEtAl2026.Response.ms2 = 0
• TsvilodubEtAl2026.utility δ TsvilodubEtAl2026.Goal.g₂ TsvilodubEtAl2026.Response.ms1 = 0
• TsvilodubEtAl2026.utility δ TsvilodubEtAl2026.Goal.g₂ TsvilodubEtAl2026.Response.ms2 = 1
• TsvilodubEtAl2026.utility δ x✝ TsvilodubEtAl2026.Response.exh = 1 - δ

noncomputable def TsvilodubEtAl2026.prior (ε : ↑unitInterval) : MeasureTheory.Measure Goal

The prior at uncertainty ε puts probability ε on the dispreferred goal.

Equations

• TsvilodubEtAl2026.prior ε = ProbabilityTheory.bernoulliMeasure TsvilodubEtAl2026.Goal.g₂ TsvilodubEtAl2026.Goal.g₁ ε

instance TsvilodubEtAl2026.instIsProbabilityMeasureGoalPrior (ε : ↑unitInterval) : MeasureTheory.IsProbabilityMeasure (prior ε)

noncomputable def TsvilodubEtAl2026.expectedUtility (ε : ↑unitInterval) (δ : ℝ) (r : Response) : ℝ

The expected utility of an answer in the condition (ε, δ).

Equations

• TsvilodubEtAl2026.expectedUtility ε δ r = ∫ (g : TsvilodubEtAl2026.Goal), TsvilodubEtAl2026.utility δ g r ∂TsvilodubEtAl2026.prior ε

@[simp]

theorem TsvilodubEtAl2026.expectedUtility_ms1 {ε : ↑unitInterval} {δ : ℝ} : expectedUtility ε δ Response.ms1 = 1 - ↑ε

@[simp]

theorem TsvilodubEtAl2026.expectedUtility_ms2 {ε : ↑unitInterval} {δ : ℝ} : expectedUtility ε δ Response.ms2 = ↑ε

@[simp]

theorem TsvilodubEtAl2026.expectedUtility_exh {ε : ↑unitInterval} {δ : ℝ} : expectedUtility ε δ Response.exh = 1 - δ

theorem TsvilodubEtAl2026.decisionValue_utility {ε : ↑unitInterval} {δ : ℝ} (hε : ↑ε ≤ 1 / 2) : ProbabilityTheory.decisionValue (utility δ) (prior ε) = 1 - min (↑ε) δ

theorem TsvilodubEtAl2026.valueOfInformation_id_utility {ε : ↑unitInterval} {δ : ℝ} (hε : ↑ε ≤ 1 / 2) (hδ : 0 ≤ δ) : ProbabilityTheory.valueOfInformation (ProbabilityTheory.decisionValue (utility δ)) ProbabilityTheory.Kernel.id (prior ε) = min (↑ε) δ

theorem TsvilodubEtAl2026.questionUtility_bot {ε : ↑unitInterval} {δ : ℝ} (hε : ↑ε ≤ 1 / 2) (hδ : 0 ≤ δ) : Question.utility (utility δ) (prior ε) ⊥ = min (↑ε) δ

The clarification question asks which goal the questioner has, the finest question about the goal, so its value as a question in the sense of [vR03b] is min ε δ.

The clarification gate

noncomputable def TsvilodubEtAl2026.clarifyProb (τ c : ℝ) (ε : ↑unitInterval) (δ : ℝ) : ↑unitInterval

The probability of clarifying is the logistic function, with slope τ and threshold c, of the value of learning the goal.

Equations

• One or more equations did not get rendered due to their size.

theorem TsvilodubEtAl2026.coe_clarifyProb {ε : ↑unitInterval} {δ : ℝ} (τ c : ℝ) (hε : ↑ε ≤ 1 / 2) (hδ : 0 ≤ δ) : ↑(clarifyProb τ c ε δ) = (τ * (min (↑ε) δ - c)).sigmoid

theorem TsvilodubEtAl2026.tl_justAsk {εL εH : ↑unitInterval} {δ τ : ℝ} (hτ : 0 < τ) (c : ℝ) (hδ : 0 ≤ δ) (hε : εL < εH) (hH : ↑εH ≤ 1 / 2) (hL : ↑εL < δ) : clarifyProb τ c εL δ < clarifyProb τ c εH δ

With a costly exhaustive answer, higher uncertainty means more clarification, the paper's TL;JustAsk.

theorem TsvilodubEtAl2026.noNeedToAsk {εL εH : ↑unitInterval} {δ : ℝ} (τ c : ℝ) (hδ : 0 ≤ δ) (hL : δ ≤ ↑εL) (hH : δ ≤ ↑εH) (hεL : ↑εL ≤ 1 / 2) (hεH : ↑εH ≤ 1 / 2) : clarifyProb τ c εL δ = clarifyProb τ c εH δ

With an exhaustive answer cheaper than either uncertainty, uncertainty makes no difference to clarification, the paper's NoNeedToAsk.

theorem TsvilodubEtAl2026.clarification_rises_with_cost {ε : ↑unitInterval} {δS δL τ : ℝ} (hτ : 0 < τ) (c : ℝ) (hε : ↑ε ≤ 1 / 2) (hS : 0 ≤ δS) (hεS : δS < ↑ε) (hδ : δS < δL) : clarifyProb τ c ε δS < clarifyProb τ c ε δL

Once uncertainty exceeds the smaller cost, a costlier exhaustive answer means more clarification, the main effect of option-space size on clarification in Experiment 1.

theorem TsvilodubEtAl2026.uncertainty_matters_most_when_costly {εL εH : ↑unitInterval} {δS δL τ : ℝ} (hτ : 0 < τ) (c : ℝ) (hS : 0 ≤ δS) (hSL : δS ≤ ↑εL) (hε : εL < εH) (hH : ↑εH ≤ 1 / 2) (hL : ↑εL < δL) : clarifyProb τ c εL δS = clarifyProb τ c εH δS ∧ clarifyProb τ c εL δL < clarifyProb τ c εH δL

Uncertainty raises clarification when the exhaustive answer is costly and leaves it unchanged when it is cheap, the interaction the paper tests.

theorem TsvilodubEtAl2026.clarifyProb_of_ablated {ε : ↑unitInterval} {δ : ℝ} (τ c : ℝ) (hε : ↑ε ≤ 1 / 2) (hδ : 0 ≤ δ) (h : ↑ε = 0 ∨ δ = 0) : ↑(clarifyProb τ c ε δ) = (τ * (0 - c)).sigmoid

Without cost or without uncertainty, the ablated models of the model comparison, the gate is the same in every condition.

The behavioral policy

noncomputable def TsvilodubEtAl2026.policy (α : ℝ) (ε : ↑unitInterval) (δ : ℝ) : MeasureTheory.Measure Response

The behavioral policy at the condition (ε, δ) is the softmax of α · EU.

Equations

• TsvilodubEtAl2026.policy α ε δ = MeasureTheory.Measure.count.tilted fun (r : TsvilodubEtAl2026.Response) => α * TsvilodubEtAl2026.expectedUtility ε δ r

instance TsvilodubEtAl2026.instIsProbabilityMeasureResponsePolicy (α : ℝ) (ε : ↑unitInterval) (δ : ℝ) : MeasureTheory.IsProbabilityMeasure (policy α ε δ)

theorem TsvilodubEtAl2026.policy_real_singleton (α : ℝ) (ε : ↑unitInterval) (δ : ℝ) (r : Response) : (policy α ε δ).real {r} = Real.exp (α * expectedUtility ε δ r) / ∑ r' : Response, Real.exp (α * expectedUtility ε δ r')

theorem TsvilodubEtAl2026.policy_real_lt_iff {ε : ↑unitInterval} {δ α : ℝ} (hα : 0 < α) {r r' : Response} : (policy α ε δ).real {r} < (policy α ε δ).real {r'} ↔ expectedUtility ε δ r < expectedUtility ε δ r'

theorem TsvilodubEtAl2026.policy_real_exh_lt {εL εH : ↑unitInterval} {δ α : ℝ} (hα : 0 < α) (hε : εL < εH) (hH : ↑εH ≤ 1 / 2) : (policy α εL δ).real {Response.exh} < (policy α εH δ).real {Response.exh}

The layered reaction

inductive TsvilodubEtAl2026.Reaction : Type

A reaction either clarifies or commits to a direct answer.

• clarify : Reaction
• act (r : Response) : Reaction

def TsvilodubEtAl2026.instDecidableEqReaction.decEq (x✝ x✝¹ : Reaction) : Decidable (x✝ = x✝¹)

Equations

• TsvilodubEtAl2026.instDecidableEqReaction.decEq TsvilodubEtAl2026.Reaction.clarify TsvilodubEtAl2026.Reaction.clarify = isTrue ⋯
• TsvilodubEtAl2026.instDecidableEqReaction.decEq TsvilodubEtAl2026.Reaction.clarify (TsvilodubEtAl2026.Reaction.act r) = isFalse ⋯
• TsvilodubEtAl2026.instDecidableEqReaction.decEq (TsvilodubEtAl2026.Reaction.act r) TsvilodubEtAl2026.Reaction.clarify = isFalse ⋯
• TsvilodubEtAl2026.instDecidableEqReaction.decEq (TsvilodubEtAl2026.Reaction.act a) (TsvilodubEtAl2026.Reaction.act b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TsvilodubEtAl2026.instDecidableEqReaction : DecidableEq Reaction

Equations

• TsvilodubEtAl2026.instDecidableEqReaction = TsvilodubEtAl2026.instDecidableEqReaction.decEq

@[instance_reducible]

instance TsvilodubEtAl2026.instReprReaction : Repr Reaction

Equations

• TsvilodubEtAl2026.instReprReaction = { reprPrec := TsvilodubEtAl2026.instReprReaction.repr }

def TsvilodubEtAl2026.instReprReaction.repr : Reaction → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TsvilodubEtAl2026.instMeasurableSpaceReaction : MeasurableSpace Reaction

Equations

• TsvilodubEtAl2026.instMeasurableSpaceReaction = ⊤

instance TsvilodubEtAl2026.instDiscreteMeasurableSpaceReaction : DiscreteMeasurableSpace Reaction

noncomputable def TsvilodubEtAl2026.reaction (τ c α : ℝ) (ε : ↑unitInterval) (δ : ℝ) : MeasureTheory.Measure Reaction

The reaction clarifies with the gate's probability and otherwise acts by the policy.

Equations

• One or more equations did not get rendered due to their size.

theorem TsvilodubEtAl2026.reaction_real_clarify (τ c α : ℝ) (ε : ↑unitInterval) (δ : ℝ) : (reaction τ c α ε δ).real {Reaction.clarify} = ↑(clarifyProb τ c ε δ)

theorem TsvilodubEtAl2026.reaction_real_act (τ c α : ℝ) (ε : ↑unitInterval) (δ : ℝ) (r : Response) : (reaction τ c α ε δ).real {Reaction.act r} = (1 - ↑(clarifyProb τ c ε δ)) * (policy α ε δ).real {r}

theorem TsvilodubEtAl2026.justListThemAll {εL εH : ↑unitInterval} {δS : ℝ} (τ c : ℝ) {α : ℝ} (hα : 0 < α) (hS : 0 ≤ δS) (hSL : δS ≤ ↑εL) (hε : εL < εH) (hH : ↑εH ≤ 1 / 2) : (reaction τ c α εL δS).real {Reaction.act Response.exh} < (reaction τ c α εH δS).real {Reaction.act Response.exh}

With an exhaustive answer cheaper than either uncertainty, higher uncertainty means more exhaustive answers, the paper's JustListThemAll.

The gate as a softened clarify-or-commit rule

theorem TsvilodubEtAl2026.half_lt_clarifyProb_iff {τ : ℝ} (hτ : 0 < τ) (c : ℝ) (ε : ↑unitInterval) (δ : ℝ) : 1 / 2 < ↑(clarifyProb τ c ε δ) ↔ DongEtAl2026.Clarifies (utility δ) (prior ε) (fun (x : Unit) => ProbabilityTheory.Kernel.id) c {()}

The clarification question reveals the goal, so as a question of [DHH+26] it is the identity kernel, and the gate exceeds one half exactly when their agent, with asking cost c, clarifies.