A new paper proves that the usual way we check whether an AI unlearning edit worked, testing a bunch of examples, can never actually prove the skill is gone.
The method targets mechanistic edits: the ablations, weight tweaks, and activation steering researchers use to strip a harmful capability out of a model while keeping its useful skills intact. Instead of testing a sample of inputs, the authors use sound bound propagation to certify that an edit removes one skill and preserves another across an entire continuous region of a model's embedding space. They demonstrate the approach on networks ranging from toy ReLU models up to a standard transformer with softmax and LayerNorm, and the switch to bound propagation lets them cover roughly nine times the input-perturbation dimension an exact solver could handle.
That distinction matters because testing alone cannot rule out failure. The authors prove that no finite deterministic black-box test can certify a skill is truly removed: an edit can pass every test thrown at it and still fail on a survivor pocket of inputs that can be shrunk arbitrarily small and still exist. For anyone relying on unlearning to strip dangerous capabilities out of a model, that is the gap between we checked and we proved.
The guarantees so far only run on small, standard-architecture networks, and they require the target skill to have a decidable specification, a bar most real-world harms do not clear.