Bandit-Arm Design, Goodhart Taxonomy & GAT

v2026.07.3 last finalized 2026-07-19. One marked change below (Open Questions, panproto note) not yet reviewed. Tracked as sail-7ie2.

This chapter is about the design of sail-judge, SAIL’s live scaffolding agent — how it decides what to say, why the first version of that design was too clever by half, and where Generalized Algebraic Theories (GATs) turn up, twice, in ways that turned out to be genuinely different questions wearing the same three letters.

The design arc: from rhetorical styles to research constructs

sail-judge runs in a real chat room (currently on trullala, over chatto.tilde.style) and, on its turn, has to choose how to intervene. The governing framing from day one — SAIL’s own recurring tagline for this: an agent that chooses to answer or ask. A discourse-driver role judges whether to speak at all; an asker role, when it does speak, asks a generative, clarifying question rather than giving an answer. (The underlying facts substrate — a normalized subject/predicate/object/confidence/disputed/source-event table — was itself evaluated against ElectricSQL’s Burn demo before being adopted, not invented from scratch; that’s the same FactStore the Rust port carries as Restate-durable state.) The first working version picked between three rhetorical styles per role — asker: curious / concrete / reflective; discourse-driver: synthesize / contrast / extend — using Thompson sampling over hand-rolled Beta posteriors (Marsaglia–Tsang gamma sampling under the hood, the same algorithm family as Ariel’s graze project for ATProto custom feeds). It worked, in the narrow sense that the mechanism ran end to end against a real conversation and updated its weights correctly.

It was also the wrong thing to be learning. The arms were generic conversational postures, not grounded in anything about how people actually learn — which meant the bandit was free to converge on “asks things that make people reply with more questions,” a pattern indistinguishable from being mildly confusing. Rewarding engagement isn’t the same as rewarding learning, and nothing about the v1 design could tell the two apart.

The fix wasn’t a better reward function bolted onto the same arms — it was redefining what the arms are. The current design grounds each arm in a named construct from the learning-science literature:

• asker arms: generation effect (Slamecka & Graf), retrieval-practice / testing effect (Roediger & Karpicke), desirable difficulty (Bjork), and metacognitive calibration (asking for a confidence estimate before checking).
• discourse-driver arms: Wood, Bruner & Ross’s (1976) three scaffolding functions — marking critical features, reduction in degrees of freedom, direction maintenance.

Worth naming explicitly, because it’s a real design bet rather than an obvious default: splitting “teacher” into an asker role (knowledge-transfer, testing) and a discourse-driver role (process-facilitation) promotes something that, in a human teacher, is usually an informal personality trait — some teachers lean instructor, some lean mentor — to the level of a structural, addressable choice. That’s a deliberate instructor-to-mentor shift, not a neutral engineering decision, and it’s worth saying so plainly rather than presenting the two-role split as if it fell out of the problem on its own.

Goodhart’s Law, made actionable

Naming the constructs doesn’t make the reward signal honest by itself. Each arm still needs a cheap, live-computable proxy for “did this intervention actually work” — and every proxy is a target Thompson sampling will happily overfit to, in whatever way is cheapest. Manheim & Garrabrant’s taxonomy (regressional / extremal / causal / adversarial) gives a vocabulary for how a given proxy is likely to fail, arm by arm, before it fails live:

This isn’t just a theoretical exercise — the failure modes it predicts have already shown up live, in a real running room: a marking-critical-features reward once fired on a coincidentally shared word (“last”) rather than genuine feature-noticing, and a later pass caught the same class of bug again with generic filler words (“earlier”) producing false-positive overlap. Both are exactly the regressional failure the table above predicts for that arm. A confidence-detection regex also had a real, silly bug (a trailing \b right after % that could never match) — a reminder that a proxy can fail for boring implementation reasons well before it fails for interesting Goodhart reasons, and both need checking.

Seven Signals walks through both bugs as they were actually found and fixed live on trullala, plus the coverage this gave afterward (sail-judge.test.mjs’s 43 assertions, a 12/12 forced-arm testbed run) and the parallel judge’s first real disagreement with a regex evaluator — the verification half of this story, not just the two bugs summarized above.

This table is the condensed version of a longer live argument — The Question Mark Problem, reproduced in full in the Appendix’s Artifact Series, walks through how the arms went from rhetorical styles to these named constructs, and how the convergence table above was actually arrived at (two independent framings — an instructor/mentor collapse, and the Goodhart/Ostrom-commons mechanism — converging on the same per-arm classification).

Why not just use an LLM as the judge?

The obvious next move — replace the regex heuristics with an LLM-as-judge reward — doesn’t dodge Goodhart’s Law, it relocates it, in three specific ways:

1. Adversarial: the generator and judge sit inside the same optimization loop, which is exactly RLHF’s documented “reward model overoptimization” problem (Gao et al. 2022) — the policy converges on examples that fool the judge, not on genuinely good outputs.
2. Regressional: ordinary judge biases (verbosity/fluency preference, self-preference if judge and generator share a model family).
3. Causal: judge-approval and real learning gain likely share an upstream cause (surface plausibility) rather than the judge’s approval causing the real outcome.

This connects directly to a tension the AIDLE proposal had already staked a position on before any of this was built: its “Third Axis of Frontier AI” framing contrasts US labs’ RLHF (unverifiable rater preference — the same failure mode as an LLM-judge reward) against the RLVR path (replacing the rater with a checker — a compiler, a unit-test suite, a formal proof verifier), with the proposal’s own honest caveat that “no checker exists for is this the right question to ask this learner now” — RLVR doesn’t reach pedagogy. AIDLE’s proposed third path was a GAT-constrained, symbolic-grounding layer instead of either a rater or a narrow checker. sail-judge’s reward-evaluator design space — cheap regex proxy vs. LLM-judge vs. something GAT/schema-constrained — turns out to be a small, concrete, currently-running instance of that exact three-way tension, not just an analogy to it.

Thompson sampling — one solution, not the only one

However the reward gets fixed, the sampling mechanism choosing between arms is already about as good as it can be. For this problem class (Bernoulli rewards, independent arms), Thompson sampling has a proven regret bound (Agrawal & Goyal, 2012/2013) matching the theoretical lower bound — it converges on the best arm about as fast as is mathematically possible, for whatever reward it’s given. That’s the real lesson from building the Julia/Pluto teaching notebook that replays sail-judge’s actual historical fire/reward sequence: a more sophisticated bandit implementation would still converge just as efficiently on whatever the reward signal actually measures, which may or may not be what SAIL cares about. The lever that matters is the reward signal, not the sampler.

Bandits, Recapped is the non-interactive companion to that notebook — same running example (sail-judge’s actual arms, not an abstract slot machine), theory-only where the notebook is data-grounded and interactive; the notebook’s own intro points readers here first if the mechanism itself needs explaining before the historical replay does.

The notebook itself is now live and genuinely interactive, not a description of one — see the Teaching Notebooks in the Appendix.

Thompson sampling is one well-studied member of a wider family of solutions to the explore/exploit multi-armed-bandit problem, worth naming so it doesn’t read as the only option:

• Upper Confidence Bound (UCB) — deterministic, optimism-under- uncertainty: pick the arm with the highest upper confidence bound on its estimated reward, so under-explored arms get an automatic boost.
• Epsilon-greedy — the simplest baseline: mostly exploit the current best arm, explore a random arm with fixed probability ε. Easy to reason about, generally less sample-efficient than either of the above.

None of these change the argument above — swapping the sampler doesn’t touch what’s actually being optimized for.

Where GAT shows up — two genuinely different questions

“GAT” comes up twice in this thread, and they’re worth keeping separate — conflating them was a real risk early on.

Sense 1 — GAT as a possible answer to the reward-verification problem above. Could a categorical-lens approach (Milewski’s categorical lenses; Patterson & Lynch et al. 2024, arXiv:2404.04837; the panproto/GATlab integration) give a verifiable, schema-checked mapping from raw signal to reward classification — something between a noisy regex heuristic and a black-box LLM judge? This is still an open, speculative research question, not yet started as design work. It would need real GAT expertise to answer honestly rather than improvised from the GATlab paper alone. A separate cross-repo asset scan (2026-07-11, covering everything currently running across haiku.garden, tilde.style/tilde.cards, and tracker) came back with the same honest verdict independently: GAT schema enforcement has no code or spike anywhere yet, and isn’t close to being de-risked by existing assets the way most of the rest of SAIL’s build sequence is. It’s genuinely greenfield, not just under-prioritized.

Sense 2 — GAT as the literal Rust language feature, already shipped (unrelated pun, same three letters). This is the part with an actual formal derivation behind it, worked out in a standalone spike (2026-07-13-persona-role-arm-gat-spike.md) that’s worth walking through in more detail than a one-line summary, since it’s the part of this chapter with the most concrete material for a real GAT conversation — formal signatures Aaron can react to and push back on directly, not just prose.

The fibration, formally

The spike’s starting move: write sail-judge’s actual current mechanism down as a Generalized Algebraic Theory (Cartmell 1986) rather than describing it in prose. RoomState is the conversational state a turn is evaluated against; the two live counters become operations on it; the two threshold constants become constants of the theory. Role is a sort whose terms are produced by a guarded, priority-ordered derivation — not an enumeration handed down from nowhere:

Γ ⊢ s : RoomState    msgsSinceQuestion(s) ≥ ASK_AFTER_NO_QUESTION
──────────────────────────────────────────────────────────────────  (asker-intro)
Γ ⊢ fires(s) : Role                           [fires(s) ≡ asker]

Γ ⊢ s : RoomState    msgsSinceQuestion(s) < ASK_AFTER_NO_QUESTION
                     msgsSinceReply(s) ≥ SPEAK_EVERY
──────────────────────────────────────────────────────────────────  (driver-intro)
Γ ⊢ fires(s) : Role                   [fires(s) ≡ discourseDriver]

driver-intro’s guard carries the negation of asker-intro’s guard verbatim, as part of its own side-condition — which is what makes “asker wins ties” a derived fact about the theory (the two guards are mutually exclusive by construction) rather than a prose note about if/else if ordering. If neither guard holds, fires(s) is simply undefined at s: no term of Role is derivable, and the no-op case sits outside the sort entirely rather than existing as a third term with an empty fiber.

Arm is a dependent sort indexed by Role — Arm(asker) and Arm(discourseDriver) are disjoint object literals in the actual code, two independently-seeded Beta-Bernoulli posteriors, and there is no arm value that’s even well-formed for both roles. One extra wrinkle inside the asker fiber: a scheduled override for desirable-difficulty, which introduces a second term-formation rule targeting the same dependent sort:

Γ ⊢ fires(s) ≡ asker    askerFireCount(s) mod DESIRABLE_DIFFICULTY_EVERY = 0
───────────────────────────────────────────────────────────────────────────  (scheduled-override)
Γ ⊢ arm(s) : Arm(asker)                [arm(s) ≡ desirable-difficulty]

Γ ⊢ fires(s) ≡ asker    askerFireCount(s) mod DESIRABLE_DIFFICULTY_EVERY ≠ 0
───────────────────────────────────────────────────────────────────────────  (bandit-draw)
Γ ⊢ arm(s) : Arm(asker)                [arm(s) ≡ bandits.asker.choose()]

One deterministic-scheduled rule and one stochastic rule, both still confined to the same fiber — neither can produce a term of Arm(discourseDriver). The natural entity underneath all of this is the total space of the fibration, the dependent-sum sort:

Move := Σ_{r : Role} Arm(r)

A term of Move is a pair (r, a) with a : Arm(r) — you cannot construct one without committing to r first, and committing to r immediately restricts which a are even typeable. That’s the actual content behind the intuition that role-choice and arm-choice were never two independent mechanisms glued together after the fact: they’re the base-projection and fiber-selection of building one term of one sort, in two stages. The two-object, two-branch shape of the real code is a presentation choice, not a semantic claim that two separate mechanisms exist.

This matters for more than tidiness, because a morphism between GATs has to preserve the whole dependent family, fiberwise — it can rename or even merge/split fibers, but it can’t flatten Role × Arm into an unstructured product and permute across that flattening, because that’s a map of a strictly weaker theory (a plain product), not this one. Which gives three concrete, checkable invariants any legitimate extension of this design has to respect: the fiber-cardinality profile (3+1 for asker, 3 for discourse-driver); discreteness of the fibration itself; and, as a direct consequence of discreteness rather than a separate design choice, a block-diagonal joint posterior — asker’s and discourseDriver’s arm draws should show zero statistical cross-dependence. That last one is genuinely falsifiable against the real event log (sail-judge-events.jsonl) and hasn’t been checked yet — if it turns out false, the fibration is leaking, which is itself useful information, not just a bug.

Once sail-judge was actually ported to Rust, this stopped being only a paper exercise: Rust’s own associated-type generics now enforce the Move := Σ_{r:Role} Arm(r) structure at compile time — AskerArm/DiscourseArm enums, exhaustively matched — replacing a private duplicated arm-string list that had already drifted out of sync once, and a bare .expect("unknown arm key") that could previously panic on any bad caller-supplied string. A real, already-landed fix, entirely separate from Sense 1’s still-open verification question above.

From formal fibration to mined roles: a slow theory, a fast theory, and a morphism between them

The two hardcoded roles (asker/discourseDriver) are themselves an invented category, the same way v1’s rhetorical arms were — chosen by hand, not mined from anything. The same move that fixed the arms (ground them in something real, not invented) has an analogous, not-yet-built target here: mine Role itself from real observed community behavior rather than hand-inventing it. There’s already real, in-progress infrastructure this could build on rather than starting from a proposal: a firehose-consuming Bluesky scanner is already running (curating a real candidate account list for a haiku/poetry community), built on existing tab/watchtower infrastructure — genuinely available data, not hypothetical.

The first framing of this ran into a real timescale mismatch, worth stating plainly rather than glossing over: the actual ground-truth signal for “this is a genuine connection between two distinct ideas, not just surface word overlap” is slow — a human curator drawing typed, directional links between saved items over weeks (Semble’s own Connection object between two Cards is exactly this relation, already real and queryable; a hand-written “Threads” section in a separate notes file is the same relation under a different name). Role/persona choice, by contrast, has to happen at conversational speed, within a single live exchange. Querying the slow corpus directly, mid-conversation, doesn’t fit that timescale — so this can’t be a live lookup.

The resolution is an offline distillation step, not a live query: extract, offline, from the real slow corpus what actually characterizes a genuine connection between ideas (as opposed to superficial word overlap), and let that extraction’s output be a fast, “synthetic” artifact — a small classifier, an embedding-similarity check, or something else, not yet decided — that runs live. Stated as two GAT signatures and a morphism between them rather than a bare ML pipeline:

SlowTheory                                    (curation timescale — weeks, human-curated)
  Sort  Card
  Dependent sort  Connection(c₁ c₂ : Card)    — only well-typed between two actual Card terms

FastTheory                                    (conversation timescale — the live process)
  Sort  Role,  Dependent sort  Arm(r : Role),  Move := Σ_{r:Role} Arm(r)     — as above
  Dependent sort  PersonaHint(m : Move)        — new: which mined behavioral
                                                  archetype a given Move resembles

Distill : SlowTheory → FastTheory             — computed offline, once;
                                                 its *action* on terms (the
                                                 classifier/similarity-check)
                                                 is what runs live

PersonaHint is indexed by Move, not free-standing, for the same reason Arm is indexed by Role — a persona-hint meaningful for an asker-shaped move need not even be well-typed for a discourseDriver-shaped one. This is the same shape as the categorical-lens idea in Sense 1 above — a versioned, bidirectional schema mapping extracted from observed data, not designed top-down and not a black-box learned judge either. What the GAT framing adds over treating this as a bare ML pipeline: “is the distillation still faithful to the real data” becomes a checkable morphism law — does Distill commute with Connection’s own dependency on two distinct Cards, so that a genuine cross-card connection lands as a within-fiber Move rather than accidentally collapsing two fibers together — rather than only an offline eval metric with no structural guarantee behind it.

What this means concretely for anything that mines raw data (a “Tab-miner”): it only needs to emit SlowTheory-shaped material — a per-record tuple like {did, collection, record_uri, observed_at, text}, enough to stand as a candidate Card term. It does not need to know Role or Arm exist at all. Mining is the slow/real side; Move/ PersonaHint are the fast/synthetic side; the two connect through exactly one designed morphism — a real layering boundary, useful for scoping any future collaboration on this piece specifically.

Three candidate roles, offered as hypotheses to argue with

None of these are commitments — they’re deliberately concrete guesses, offered so a real mining pass (or a conversation with Aaron) has something to react to or falsify, rather than starting from nothing:

• Synthesizer — notices when two different people (not the same speaker across turns) have made related-but-unconnected points, and names the connection. Structurally, this is the cross-person analogue of Semble’s Connection object, not anything the existing marking-critical-features arm already covers (which only operates on one person’s most recent utterance). A real, checkable reward construct falls out for free: did the two people actually engage with each other’s point afterward, not just individually with the bot.
• New-arrival greeter — fires specifically on a new participant’s first message in the room, oriented at onboarding rather than Socratic pressure. Low-status, side-task engagement; needs fast orientation, not more friction.
• Persistent-thread minder — notices a topic recurring across sessions (a multi-day horizon), not just within one conversation window — a genuinely different need from the moment-to-moment roles above.

Worth being explicit about the source of the pattern, not the content: these were drafted by analogy to a persona workshop for a sibling project, which is a useful structural precedent (real, observable axes — need, context, frequency of engagement, characteristic frustration — rather than invented rhetorical labels) but not itself a source of new SAIL roles. Synthesizer/New-arrival-greeter/Persistent-thread-minder are SAIL’s own hypotheses, sized to be testable once real mined data exists, not imports.

Distill, concretely — candidate implementations

Not drafted yet — a placeholder for a real follow-up pass, not a design.

• Candidate shapes for Distill’s actual implementation, none chosen: a trained embedding-similarity classifier over (Card, Card) pairs; a smaller symbolic rule-set extracted directly from Semble’s Connection metadata (its type/direction fields); or a hybrid of the two.
• What “checking the morphism law” would concretely look like as a test: sample known Connection pairs, run Distill’s action on them, verify the resulting Move-level tags don’t cross fibers — an actual test to write, not just a property to assert.
• The real data-volume question, unanswered: how many genuine Connection examples exist today (Semble plus riddles.md’s Threads section) versus how many a first classifier attempt would plausibly need to be worth trying.
• Not yet scoped: whether this becomes its own bean, or stays folded under sail-i9j3 until there’s enough mined data to make it concrete.

What happens if the arm space grows a lot? A real collapse question

This subsection’s namesake: The GAT-Collapse Question is the discussion-opener version of everything below, written to be argued with directly rather than read passively — every claim here traces to 2026-07-13-persona-role-arm-gat-spike.md, and that artifact is the fuller account, including a fibration diagram and the SlowTheory/FastTheory thread only summarized in passing here.

A question worth asking before scaling this design up rather than after: if the arm space grows drastically, does the role/arm split eventually collapse into one thing? The answer turns out to depend entirely on how the growth happens, and there are two structurally different ways to do it, with opposite answers.

Case A — fiber-preserving expansion: no collapse. Grow each role’s arm list — Arm(asker) and Arm(discourseDriver) go from 3–4 named, literature-grounded terms each to 50 — but stay what they are today: two separate object literals, two separately-seeded posteriors. Nothing qualitative moves; Move is still exactly the Σ-type above, just over bigger fibers, and the block-diagonal posterior property still holds exactly as stated. Worth stating plainly because it’s the intuitive-but- wrong expectation — “more arms” alone doesn’t push the design anywhere near collapse.

Case B — fiber-merging expansion: real collapse, and a specific kind. Collapse requires the added dimensionality to come from moving arms into one shared continuous space used by both roles — arms become points in a common embedding, ℝᵏ, rather than two disjoint named lists. Here the dependency direction actually reverses:

roleOf : ArmSpace → Role      — Role becomes a DERIVED quotient of Arm,
                                 recovered from which region of ℝᵏ a chosen
                                 arm-point falls in, not a prior index that
                                 constrains which arms are even typeable

This is a genuine reversal of base and fiber, not the same fusion as the Σ-type above (which kept Role as base throughout) — Role becomes epiphenomenal, recoverable post-hoc from a unified arm-choice, rather than something chosen before the arm and constraining it.

The realistic middle ground more plausibly sits between the two: Role acting as a soft prior or mixing weight over regions of arm-space, closer to a mixture-of-experts architecture than either a hard partition or a fully-collapsed readout. Concretely, this replaces both the guard cascade and the two per-role bandits with a single gating mechanism:

κ : Context → Dist(K)          — a gating function over K shared experts,
                                  not necessarily aligned with asker/
                                  discourseDriver at all
roleOf : ArmSpace → Dist(Role)  — Role as a DERIVED RANDOM VARIABLE, not a
                                  hard quotient — the fibration itself goes
                                  "soft"

This genuinely isn’t a plain GAT anymore — a strict GAT’s term-formation is all-or-nothing (the guards above are crisp), but a gating function assigns a distribution over experts, not a term. The natural home for this is a GAT enriched over a probability monad (the Giry monad / the Kleisli category of distributions) rather than plain Set. Turning that soft quotient’s peakedness all the way up recovers Case A (today’s design) as a limit; turning it fully deterministic — while keeping it derived, not primary — recovers Case B.

Why this is worth taking seriously rather than filing as a tangent: the two previously-considered options for replacing the current triggering mechanism (a two-level Thompson bandit, or a smarter deterministic eligibility signal) both risked or explicitly avoided the same failure — two nested discrete learning layers both trying to converge on the same sparse live-conversation data volume. A single joint gating function sidesteps that particular risk (one learning problem instead of two nested ones) — but it doesn’t sidestep data-hunger in general: fitting any continuous gate over a richer context typically needs more data than two tiny, extremely sample-efficient Beta-Bernoulli bandits over 3–4 discrete arms each. A trade, not a strict improvement, and shouldn’t be oversold as one.

And it connects back to the distillation morphism above rather than competing with it: Distill’s natural training source (the slow, real curation corpus — Semble connections, hand-written thread notes) could just as well produce this gating kernel as its output, rather than a hard classifier label — PersonaHint(m : Move) becomes the kernel itself, deployed frozen (or slowly re-trained) at conversation speed. Read this way, mixture-of-experts isn’t a rival architecture to the Tab-miner proposal; it’s a candidate answer to what Distill’s output shape should actually be.

Pushing the probabilistic-GAT tail further

Not drafted yet — a placeholder for a real follow-up pass, not a design.

• What would it take to state the Giry-monad / probabilistic-GAT extension above precisely enough to be checkable, rather than gestured at — which categorical-probability formalism actually fits, and does it match how GATlab/panproto already handle probabilistic extensions, or is this a genuinely different move?
• Concretely, what would κ : Context → Dist(K) look like as code — a small mixture-of-experts head over a shared embedding, something built on an existing probabilistic-programming library, or neither?
• How would this actually get tested against the discreteness-violation check already flagged above (cross-fiber dependence in the real event log) — would evidence of leakage there directly motivate building this, or is that too small a signal to justify a probabilistic extension at all?
• A real cost/benefit question, not yet answered: is this worth prototyping before there’s a live use for more than two roles / more than a handful of arms per role — i.e., before the discrete design actually starts straining?

A concrete near-term experiment this feeds: the SAITO ablation

Everything above — the Goodhart taxonomy, the Third-Axis framing, the two senses of GAT — is either live-but-small (the actual prompt-selection bandit) or still speculative (the GAT questions). There’s a third piece, designed but not yet built, that sits between them and is worth Aaron seeing specifically: an actual ablation that trains model weights, rather than selecting between prompts over a frozen large model, to test the Third-Axis claim directly rather than just argue for it.

The claim under test, stated precisely: a policy optimized for a delayed, outcome-based reward (did the learner retain/transfer the material later) behaves differently — and is harder to Goodhart — than a policy optimized for an immediate, rater-style reward (did this reply seem helpful right now), even at small scale. GPT-2-scale (124M–410M), not a literal 2019 GPT-2 checkpoint — a modern small open model (SmolLM2, Pythia, or Qwen2.5-0.5B) is the actual candidate.

Environment. No real human RL loop is feasible at this budget, so this runs in a synthetic tutoring environment: a frozen “student” model (not trained) plays a learner with deliberately incomplete knowledge, conversing for a short multi-turn exchange with the policy model actually being tuned. Afterward the student is quizzed on held-out items from the same topic — reusing renate.chat’s already-validated Zerbe Top-10 item set as real content rather than inventing quiz items. Quiz performance is the downstream-competency signal; a separate same-turn preference judgment is the immediate-satisfaction signal. Only the policy needs gradient updates, so the frozen student can be a stronger model than the policy without inflating training cost.

Method: DPO, not PPO. Direct Preference Optimization needs only preference pairs (chosen vs. rejected trajectory) trained against a closed- form loss against the base checkpoint — far less infrastructure than a live reward model plus value function plus on-policy rollout loop. Concretely: sample several candidate tutor replies per turn from the frozen base checkpoint, roll out the full dialogue + quiz for each candidate branch, score every branch two ways (quiz score, immediate preference), and build two separate preference-pair datasets from the same rollouts — one ranked by competency outcome, one by immediate preference. Two independent DPO fine-tunes from the same base checkpoint follow, one per dataset: Policy-Competency and Policy-Satisfaction.

Evaluation. Three conditions on held-out topics: Policy-Competency, Policy-Satisfaction, and an untrained baseline (the base checkpoint, zero-shot-prompted with sail-judge’s actual ASKER_ARMS/DISCOURSE_ARMS templates as the control — direct reuse, not a new prompt design). The predicted result, if the Third-Axis argument holds: Policy-Satisfaction scores higher on immediate preference but lower on downstream quiz score than Policy-Competency — the Goodhart divergence, demonstrated rather than argued. Either outcome is reportable; a null result (no divergence) is a real, publishable finding too. One genuinely open design decision worth flagging directly: whether the immediate-satisfaction signal itself should be a cheap heuristic or an LLM-as-judge — using the LLM-judge here arguably is the point, since the ablation is trying to show that reward’s failure mode, not avoid it.

Explicit limitation, stated up front rather than glossed over: this measures model-to-model dynamics in a synthetic environment, not real human learning — a mechanism pilot, not a claim about real students.

Where it stands. Design-complete, not started — no code, no data yet. Compute sizing has already been corrected once: the original bootstrap plan’s “~2,000 GPU-hours” figure was sized for the full €3M-grant version of this work, not this pilot; a DPO fine-tune at this scale realistically needs low tens of A100-hours per policy variant, sized into a single short ZIH Alpha Centauri allocation rather than the original grant-era number carried forward unexamined. Blocked on compute landing (either ZIH or Cerebras Ambassador credits), independent of the human mini-study — same deliberate separation the original proposal made between the SAITO bet and the LEARN/benchmark bet.

Open questions

• Is GAT-constrained reward verification (Sense 1) worth building for real, and does it actually solve the adversarial/regressional/causal risks better than the alternatives, or just relocate them again? Sharpened (2026-07-22): given panproto’s actual mechanism is structural schema-checking, not free-text semantic verification, the prior question is now less “is this worth building” than “is this even the right tool for the question” — open in a different way than before.
• What would an “observatory” layer — scanning reward-proxy behavior through versioned, lens-mapped vocabularies rather than either a fixed regex or a learned judge — need to become concrete rather than a design sketch?
• Does the discrete-fibration model (Sense 2) actually hold in the real event log — is there already measurable cross-role dependence between asker’s and discourseDriver’s arm draws that would mean the model is leaking? Not checked yet.
• Distill’s concrete implementation — classifier, embedding-similarity, the gating-kernel shape above, or something else entirely — is genuinely undecided, not just unbuilt.
• Which of the three dimensionality-scaling regimes (fiber-preserving / fiber-merging / the probabilistic middle ground) does the live system currently sit closest to, once there’s enough real event volume to ask?
• For the SAITO ablation: should the immediate-satisfaction signal be a cheap heuristic or an LLM-as-judge (arguably the more honest choice, since the point is to demonstrate that reward’s failure mode), and which small base checkpoint actually fits whatever compute allocation lands first?

Supplementary reading

Five self-contained design notes were written about this material as the work happened — see the Artifact Series in the Appendix, not repeated here.