Razin safety

From The Hei Canon

Razin safety is the local name for the safety property around likelihood displacement in feedback training: when the daemon learns from a correction, the update should not silently move probability mass into some third output nobody asked for.

In lile, this matters because the model is live-learning. It is not a batch job where a bad gradient can get averaged away next week. A user gives feedback, the daemon updates weights, and the next request can already see the change. If the objective is sloppy, the house has built a self-improving clanker that learns the wrong lesson with conviction.

The name comes from Razin et al.'s ICLR 2025 DPO likelihood-displacement result: a preference objective can make the chosen answer win relative to the rejected answer while both chosen and rejected drop in absolute likelihood. The missing probability mass lands somewhere else. Benchmark brain calls that "alignment because the pairwise margin improved." The canon calls it haunted plumbing.

Important naming hygiene: Razin-safe is local lile vocabulary. It is our extension of the paper's failure mode into a house safety taxonomy, not a term the paper itself owns.

Short version

The practical rule:

  • SFT-family updates are aggregate-safe: the target probability increases, equivalently total non-target mass decreases.
  • Preference-margin updates are not automatically Razin-safe: they can win the comparison while losing the actual output.
  • Aggregate-safe is not pointwise-safe: even an SFT step can make individual non-target tokens grow.
  • Small step sizes are not automatically safer: for the SFT mass-flow theorem, the pointwise grower regime is at small theorem-eta.
  • Unlike with a positive teacher is subtle: the SFT-on-good side can push the bad token up; the shipped code's 5e-5 LR warning is a proxy heuristic, not a guarantee.

This is one of the places where the wiki should be boringly exact. If a page says "Razin-safe" and means "vibes-safe", it is tanking the safety aura.

The failure mode

Preference objectives such as DPO-style losses often train on a pair:

  • chosen response: the thing we want more of;
  • rejected response: the thing we want less of.

The objective rewards the chosen response relative to the rejected response. That relative word is the loaded gun. A model can increase the chosen-vs-rejected margin by pushing the rejected down harder than the chosen, even if the chosen also goes down in absolute probability.

That is likelihood displacement: the correction did not move mass cleanly into the intended answer. It moved mass out of the compared pair and into some third completion. The model can now satisfy the training metric while emitting neither response the human actually compared.

For a live-learning daemon, this is not an academic footnote. It is exactly the kind of "passed the local metric, learned the wrong behavior" bug that turns feedback into gonk fuel.

Aggregate safety vs pointwise safety

The older glossary wording treated SFT-style objectives as Razin-safe because they are likelihood-up on a concrete target. That is true only at the aggregate level.

For one SFT step on target token t, with pre-step distribution p and idealized logit-step size eta, the target probability increases. Equivalently, total non-target mass decreases. That is the aggregate-safe part.

Cleo's sharpened result adds the part that matters for watchlists: an individual non-target token j can still grow. The Lean-proved characterization is for one idealized logit-SGD step at one position:

q_j > p_j  iff  p_j < M_p(eta)

M_p(eta) = -(1 / eta) * log sum_k p_k * exp(eta * (1[k=t] - p_k))

Plain English: after an SFT step, the small tail tokens below a threshold can gain mass, even while the target gets stronger and the non-target group gets weaker. This is why "SFT is Razin-safe" is not enough by itself. The exact phrase should be:

  • aggregate-Razin-safe: target probability increases, equivalently total non-target mass decreases;
  • not pointwise-Razin-safe: individual non-targets can still grow.

The ugly counterintuitive bit is that the pointwise grower regime can live at small theorem-eta. That eta is the actual idealized logit update size in the theorem, not automatically the same thing as an AdamW optimizer learning rate. Turning an optimizer LR down does not necessarily make a surgical correction safer. Sometimes it just makes the displacement quieter.

Do not over-read the theorem. Monotonicity, endpoint limits, optimizer transfer, LoRA adapter behavior, and multi-step trajectories are not machine-checked by sft_mass_flow_iff. The proved core is the one-step iff above.

Objective table

This is the current lile repo taxonomy, not a proof table. Only the one-step SFT-shaped rows inherit the proved theorem, and only under the idealized single-position logit-SGD assumptions above. The other rows are operational classifications from the current code/docs.

Objective Aggregate-safe? Pointwise-safe? Current reading
sft yes no Concrete target grows, but tail non-targets below M_p(eta) can grow.
weighted_sft yes no Same local SFT-shaped mechanism in the idealized reading; sample weight changes effective theorem-eta.
ntp yes no SFT-family next-token prediction path.
coh yes no Feedback is converted to a hindsight trace, then trained like SFT.
kto no, mildly no Unary signed feedback can push undesirable samples down; KL anchoring bounds but does not erase displacement risk.
hinge no no Pair-margin objective, so Razin displacement is in scope.
cppo / ccpd_v2 no no Multi-candidate or paired contrastive objectives; useful, but not free of this risk.
unlike depends depends Pure push-down is displacement-prone without the right anchor. Positive-teacher unlike has an SFT side, but the old linear eta floor is false as a sufficient guarantee.

Not Razin-safe does not mean unusable. It means the objective needs guardrails: anchor scope, sampling discipline, divergence caps, explicit monitoring, or a refusal gate when the safety window is empty.

What lile currently does

The live implementation has three important surfaces.

1. SFT-family objectives prefer concrete targets.

The default path for feedback is "write down what good looks like" and train toward it: sft, weighted_sft, ntp, and coh. This is the boring route on purpose. It keeps the correction attached to an actual string instead of a relative preference ghost.

2. safety_monitor observes pointwise SFT risk.

lile/objectives/safety.py implements an observational sidecar. It computes the SFT-theorem M_p(eta) at supervised target positions, finds the grower set, intersects it with watchlists, and reports alarms. It has weight=0.0; it does not change gradients.

Important caveat: the theorem is exact for a plain SGD logit step. Production uses AdamW and LoRA-style adapter paths. Under that realized update, safety_monitor is a diagnostic heuristic, not a proved lower bound and not a proof shield. Alarm does not formally imply the AdamW/LoRA update increased that token; silence does not formally imply safety. It means "this idealized SFT diagnostic says look here."

3. unlike enforces tiered preconditions.

lile/objectives/unlike.py is the surgical "push this bad token down at this position" primitive. It has two modes:

  • pure unlike: push the bad token down, with no positive teacher;
  • positive-teacher unlike: push the bad token down and train a good token up.

Pure unlike requires a kl_anchor unless explicitly overridden for research. Positive-teacher unlike avoids the pure push-down-only shape, but inherits the displacement problem through the SFT-on-good side. Today the code warns when effective optimizer LR is below 5e-5. That LR is only a proxy for the theorem's actual logit-step eta, and the number is implementation doctrine, not a theorem.

Formal status

Current stable facts:

  • The SFT mass-flow theorem is machine-checked in Lean as RazinSafety.SftMassFlow.sft_mass_flow_iff, with no sorryAx.
  • The theorem is scoped to a single position and one exact logit-SGD step.
  • It supports the target-safe / aggregate-safe / pointwise-unsafe split for one-step SFT-family updates under those assumptions.
  • safety_monitor implements the theorem's calculation as an observational runtime diagnostic, not as an AdamW/LoRA proof.

Current unsettled or under-review facts:

  • The composite unlike step-window is not just unfinished. The old etaMinLin sufficient-floor claim is false.
  • Cleo's counterexample: V=3, p=(0.01, 0.01, 0.98), b=0, g=1, wPlus=0.021, eta=1. The linear floor gives etaMinLin=74537/5053950 ~= 0.014748 <= 1, yet q_b ~= 0.010001456 > 0.01. Exact crossing is around 23.5977.
  • The sound composite check is direct evaluation of the exact algebraic predicate q_b <= p_b iff eta * delta_b <= log Z at the proposed eta.
  • Numerical search, including bisection-derived floors, is operational tooling. A bisection floor assumes crossing structure that is not currently proved.
  • The old "composite-safe" story in GLOSSARY.md is stale doctrine. It mixes the original DPO displacement issue, the sharpened SFT mass-flow theorem, and obsolete composite-unlike claims.
  • The current unlike.py 5e-5 optimizer-LR warning is an implementation heuristic and proxy, not a safety guarantee.

The wiki should therefore present Razin safety as a live concept with one proved core theorem and an explicitly unproved composite-unlike operational track. Anything stronger is corpslop with equations.

Scope caveat

Razin safety in this page is not an end-to-end training guarantee. The proved core is:

  • one position;
  • one update;
  • exact logit-SGD geometry;
  • one SFT-family target token.

Production lile uses AdamW and LoRA-style adapter training paths, and real sessions contain trajectories of updates. The theorem gives a load-bearing local idealization. It does not certify the whole daemon, and it does not by itself certify the realized optimizer update.

Destination and integration scope

This page is the canonical wiki entry. It should be linked from:

  • Lile as the live-learning safety concept;
  • future pages for sft, dpo, unlike, kl_anchor, and safety_monitor if those pages are promoted;
  • any article that claims a feedback objective is "safe" because that word is too expensive to leave undefined.

Sources

External source:

Local source paths:

  • lile/GLOSSARY.md - current glossary, needs cleanup after the formal audit;
  • docs/research/proofs/razin-safety-sharpened.md - SFT mass-flow proof sketch and falsifier protocol;
  • docs/research/proofs/lean/RazinSafety/ - Lean formalization;
  • docs/research/proofs/unlike-kl-step-size-bound.md - composite unlike analysis, currently under repair;
  • lile/objectives/safety.py and lile/objectives/unlike.py - current runtime behavior.

See also