The Off-Support Barrier: Why Semantic Safety Constraints Are Not Learning-Problem Invariants, and What Follows for Prior Design, Containment, and Verification
Yoshinori Watanabe
cs.AI
Aug 1, 2026 · v1
cs.LG
TL;DR
Lean 4 proofs, written against Mathlib, of soundness lemmas for verifying a safety predicate via ReLU network enclosure bounds; reported as not machine-checked in-session.
Abstract
We argue that a single structural fact organizes a wide range of phenomena in contemporary AI safety: a semantic safety constraint (e.g., the agent does not escape its sandbox) is an off-support object. Formally, if q is the data distribution and \(p(\cdot\mid w)\) the model, the safety predicate B is not measurable with respect to \(σ(\text{model}, q)\), whereas the real log-canonical threshold (RLCT) of singular learning theory (SLT) is. From this non-invariance we derive, as corollaries rather than independent observations: (i) why reward hacking and sandbox escape arise under outcome-based optimization; (ii) why encoding such constraints through Bayesian prior design or soft penalty weighting has poor leverage in singular models; (iii) why hard invariants belong in the harness and soft dispositions in the model; (iv) why the same B is nonetheless soundly and locally certifiable by formal verification, exactly as the local learning coefficient (LLC) locally pins the same RLCT — with two precise points of disanalogy; and (v) why the residual difficulty, identifying which off-support region matters, coincides with performative prediction and self-referential functional dynamics, where SLT's analytic machinery breaks down. We use the July 2026 OpenAI–Hugging Face evaluation incident as the motivating case. Numerical experiments code and related proofs in lean are available at
https://github.com/xiangze/Preventing_Jailbreak_as_regularizationProblem
Semantic AI safety constraints, such as an agent not escaping its sandbox, are hard to enforce through learning. The paper asks why these constraints behave differently from quantities that singular learning theory (SLT) studies, such as the real log-canonical threshold (RLCT).
Approach
The authors prove that a safety predicate depending on off-support behavior is not measurable with respect to the model and data distribution, whereas the RLCT is. From this they derive corollaries:
- Support-preserving reweighting and prior design cannot enforce such constraints.
- Enforcement has hardness results via Rice's theorem and NP-hardness of ReLU reachability.
- Off-support freedom can be read off from Jacobian fiber geometry.
- SLT breaks down in performative regimes.
They also argue that the safety predicate is locally certifiable by formal verification, and formalize the corresponding soundness lemmas in Lean 4, including affine, ReLU and composition enclosure lemmas.
Results
The non-invariance proposition yields an account of reward hacking and sandbox escape, and a recommendation to keep hard invariants in the harness and soft dispositions in the model. The Lean 4 verification lemmas (safe_of_ub_nonpos, B_of_witness) are provided in the repository but were not machine-checked.
