Certified edits guarantee removal and preservation of neural skills
Certified Mechanistic Edits: Behavioral Guarantees for Skill Removal and Preservation
Machine LearningArtificial IntelligenceCryptography and Security
Summary
Neural networks sometimes learn unwanted skills that need to be removed without breaking useful ones. The authors show a way to make changes to a network and mathematically guarantee the removal of certain skills while keeping others intact for every input in a specified range. They prove that just testing inputs can’t guarantee this, so their method uses formal techniques to provide strong behavior guarantees. This method works on simple and some standard-sized neural networks and relies on having clear definitions of the skills to remove.
What this means in practice
- •For machine learning engineers: Confidently remove harmful behaviors from neural models while ensuring other functions remain unaffected for known input ranges.
- •For security software developers: Create safer AI by formally certifying that certain unwanted capabilities are reliably disabled across continuous input regions.
Authors
Md Sazid Uddin, Md. Khairul Alam Mazumder, M. F. Mridha
Abstract
Mechanistic edits (ablations, weight edits, activation steering) are the standard tools for unlearning a harmful capability from a neural network while preserving useful ones. Current approaches validate their effects only by testing, which can never cover an entire continuous region of inputs. Prior work at the interpretability-verification boundary certifies descriptions of a model: what a circuit computes, or whether it faithfully explains the whole. We instead certify the behavioral effect of an edit: that disabling a circuit removes one skill and provably preserves another, for every input in a region; a feature non-interference guarantee in the information-flow-security sense. We demonstrate such certified edits from toy ReLU networks up to a standard softmax + LayerNorm transformer, proving removal and preservation over continuous embedding-space regions and reaching roughly 9x the input-perturbation dimension an exact solver can handle by switching to sound bound propagation. Furthermore, we prove that no finite deterministic black-box test can certify removal, exhibiting an edit that passes exhaustive testing yet provably fails on a survivor pocket that can be made arbitrarily small. Guarantees hold on small, standard-architecture networks and, like any removal claim, presuppose that the target skill admits a decidable specification, a property which real-world harms may not have.