Decoders — from scored candidates to probability distributions

[McF74]

A Decoder maps a finite set of candidates carrying real-valued scores to a probability distribution over those candidates:

  scored candidates  --[Decoder]-->  P : Cand → ℝ

This file exposes the Decoder interface and three foundational instances: argminDecoder (uniform over LexProfile-lex-minimizers), argmaxDecoder (uniform over ℝ-maximizers), and softmaxDecoder α (exp(α·s) / Z over ℝ-scores).

The unifying principle is McFadden's Random Utility Model: every stochastic decoder is "argmax after a noise kernel applied to the scores". The noise distribution determines the choice rule (Gumbel ⇒ softmax, Gaussian ⇒ probit, point-mass ⇒ deterministic argmax). Noise-kernel-based decoders live in NoiseKernel.lean.

Zero-temperature bridge

softmaxDecoder α interpolates between soft and hard optimization: as α → ∞, the softmax distribution concentrates on the unique maximizer (when one exists), recovering argmaxDecoder — softmax_argmax_limit in Core.Agent.RationalAction.

Semiring connection

For deterministic (point-mass noise) decoders, the algebraic structure on scores is a semiring:

• argmaxDecoder over ℝ ↔ max-plus semiring
• argminDecoder over Tropical R ↔ min-plus (tropical) semiring
• softmaxDecoder over ℝ ↔ log-sum-exp ("warped") semiring

The zero-temperature limit softmax → argmax is precisely the semiring homomorphism log-sum-exp → max in the limit α → ∞; see Semiring.lean.

structure Core.Optimization.Decoder (Cand : Type u_1) (Score : Type u_2) : Type (max u_1 u_2)

A decoder maps scored candidates to a probability distribution.

Decoder Cand Score packages a single function: given a finite candidate set and a Score-valued evaluation, return a real-valued probability for each candidate.

The structure does not enforce that outputs are non-negative or sum to 1 — those are properties of well-behaved decoders, captured by IsProbDecoder below. Keeping the structure plain makes it easy to define non-normalized scoring functions (e.g., raw exp(score) rather than full softmax) and prove their probabilistic properties separately.

• decode : Finset Cand → (Cand → Score) → Cand → ℝ

  Decode a finite scored candidate set into a probability assignment.

class Core.Optimization.Decoder.IsProb {Cand : Type u_1} {Score : Type u_2} (d : Decoder Cand Score) : Prop

A decoder is a probability decoder when its outputs are non-negative and sum to 1 over any non-empty candidate set.

• nonneg (cands : Finset Cand) (score : Cand → Score) (c : Cand) : 0 ≤ d.decode cands score c

  All decoded probabilities are non-negative.

• sum_eq_one {cands : Finset Cand} : cands.Nonempty → ∀ (score : Cand → Score), ∑ c ∈ cands, d.decode cands score c = 1

  Decoded probabilities sum to 1 over any non-empty candidate set.

noncomputable def Core.Optimization.softmaxDecoder {Cand : Type u_1} (α : ℝ) : Decoder Cand ℝ

The softmax decoder: softmax over real-valued scores at temperature α.

decode cands score c = exp(α · score(c)) / Σ_{c' ∈ cands} exp(α · score(c')) when c ∈ cands, and 0 otherwise.

Equivalent to Core.softmax from RationalAction.lean but generalised from Fintype to a finite subset cands of a possibly-infinite type.

Equations

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

noncomputable def Core.Optimization.argmaxDecoder {Cand : Type u_1} {Score : Type u_2} [LinearOrder Score] : Decoder Cand Score

The argmax decoder: uniform distribution over the maximizers of score on cands. Deterministic (Dirac on the unique maximizer) when the maximum is achieved by exactly one candidate.

The α → ∞ limit of softmaxDecoder (see softmax_argmax_limit).

Equations

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

noncomputable def Core.Optimization.argminDecoder {Cand : Type u_1} {Score : Type u_2} [LinearOrder Score] : Decoder Cand Score

The argmin decoder: uniform distribution over the minimizers of score on cands. Instantiate Score = LexProfile Nat n for lex-min on integer cost vectors; with a single optimum, Dirac on it.

Equations

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

instance Core.Optimization.softmaxDecoder_isProb {Cand : Type u_1} (α : ℝ) : (softmaxDecoder α).IsProb

The softmax decoder is a proper probability decoder: outputs are non-negative and sum to 1 over any non-empty candidate set.

instance Core.Optimization.argmaxDecoder_isProb {Cand : Type u_1} {Score : Type u_2} [LinearOrder Score] : argmaxDecoder.IsProb

The argmax decoder is a proper probability decoder. The non-trivial part is that the set of winners is non-empty when cands is, so the uniform distribution 1/winners.card makes sense.

instance Core.Optimization.argminDecoder_isProb {Cand : Type u_1} {Score : Type u_2} [LinearOrder Score] : argminDecoder.IsProb

The argmin decoder is a proper probability decoder. Symmetric to the argmax case.