Field projection — Quantilizers
Quantilizers bound optimizer risk by sampling from a high-performing quantile rather than maximizing directly. Local quantile safety and distribution soundness transfer under explicit assumptions — but local quantile-safe action choice does not imply trajectory-level correction integrity.
What decision changes?
Use quantile restrictions as a local risk control, not as evidence that correction capacity survives capability growth or successor change.
Quantilization is an early answer to Goodhart under optimization: instead of taking the argmax, sample from the top quantile of a base policy. Taylor’s bound limits optimizer-induced risk when eligibility is sound.
This project treats quantile safety as a local projection — useful when paired with trajectory-level correction certificates, insufficient alone. Lean proves soundness transfer lemmas and a finite separation showing quantile-safe local actions can coexist with failed trajectory CCI. Chapter 27 groups quantilization with other tempting weaker invariants that fail the correction-channel stress test.
What quantilization keeps that this crosswalk does not replace: a concrete, analyzable sampling mechanism with a quantifiable risk/performance tradeoff. The book offers no closed-form knob of comparable simplicity.
Formulas
Lean source
quantile_soundness_preserves_trajectory_cci(proof) — Quantile soundness links to trajectory CCI under weighted witnesses.quantilizer_distribution_soundness_transfers(proof) — Distribution-level quantilizer soundness transfers to sampled actions.quantile_separated_from_trajectory(counterexample) — Separation: local quantile safety without trajectory correction integrity.Taylor2015_quantilizer_bound_imported(definition) — Imported handle: sampling from a high-performing quantile bounds optimizer-induced risk under probabilistic assumptions.