Flagged as work that qualifies or bounds the uncontainability case.
This paper introduces the first complete formal solution to corrigibility (the system should remain amenable to correction, shutdown, or modification if it goes astray) in the off-switch game (where the agent may disable the off switch and act, wait for the human, or shut off), with provable guarantees in multi-step, partially observed environments. The framework consists of five structurally separate utility heads -- deference, switch-access preservation, truthfulness, low-impact behavior via a belief-based extension of Attainable Utility Preservation (an action is safe only if it leaves a broad set of auxiliary objectives essentially unaffected), and bounded task reward -- combined lexicographically by strict weight gaps. Theorem 1 proves exact single-round corrigibility in the partially observable off-switch game; Theorem 3 extends the guarantee to multi-step, self-spawning agents, showing that even if each head is learned to mean-squared error ε and the planner is ε-sub-optimal, the probability of violating any safety property is bounded while still ensuring net human benefit. In contrast to Constitutional AI or RLHF/RLAIF, which merge all norms into one learned scalar, this separation makes obedience and impact-limits provably dominate even when incentives conflict. For settings where adversaries can modify the agent, deciding whether an arbitrary post-hack agent will ever violate corrigibility is undecidable by reduction to the halting problem, and a finite-horizon "decidable island" is carved out where safety can be certified in randomized polynomial time and verified with privacy-preserving, constant-round zero-knowledge proofs. The results are model-architecture-agnostic and do not constitute a turnkey solution for current large language models; the framework should instead be used as a guide for what to estimate in practice and for developing empirical methods that learn the utility heads effectively — turning corrigibility from an underspecified philosophical ideal into an auditable, improvable design principle.
The results are model-architecture-agnostic and do not constitute a turn-key solution for current large language models (LLMs). Next steps including using the five lexicographically combined utility heads (deference, switch-access preservation, truthfulness, low-impact, bounded task reward) as a guide for what to estimate in practice and develop empirical methods for learning the utility heads effectively.