Certified Mechanistic Edits: Behavioral Guarantees for Skill Removal and Preservation

Md Sazid Uddin; Md. Khairul Alam Mazumder; M. F. Mridha

cs.LGOct 2, 2026

Certified Mechanistic Edits: Behavioral Guarantees for Skill Removal and Preservation

Authors: Md Sazid Uddin, Md. Khairul Alam Mazumder, M. F. Mridha

Organizations: Department of Computer Science American International University-Bangladesh (AIUB), Dhaka, Bangladesh

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.

Figures & tables

Work	Certified object	Quantifier domain	Edit’s behavioral effect?
Compact proofs [ 4 ]	accuracy bound of the unedited model	all inputs (small domains)	no
Formal Mech. Interp. [ 5 ]	circuit faithfulness under patching	continuous activation-patch values, finitely many inputs	no
Certified circuits [ 7 ]	stability of a discovered circuit	dataset resamplings	no
Verifiable Transformers [ 6 ]	four properties of a circuit explanation	final-residual perturbations; per-input edge necessity	no (disclaimed in [ 6 ] , §1.4)
BlockCert [ 9 ]	extraction fidelity; output-deviation bound	finite traced prompt set	partial (how much, not what)
Certified unlearning [ 8 ]	process indistinguishability	distribution over models	no (statistical)

TABLE I: Certification Object and Quantifier Domain comparison of related work with our own

Subject	Size	Prover	Pert. dims	Removal $\varepsilon^{\!*}$	Preservation $\varepsilon^{\!*}$ (unedited)
Toy MLP (separated)	$d{=}2$ , 16 hidden	SMT	2	$\geq 0.6$ a	$0.0996$ $(0.0996)$
Toy MLP (entangled)	$d{=}2$ , 16 hidden	SMT	2	$\geq 0.6$ a	$0.0961$ $(0.0961)$
Deep MLP	$3\text{-}12\text{-}8\text{-}2$	SMT	3	$\geq 0.5$ a	$0.0742$ $(0.0938)$ b
Gate transformer	8 wide, 2 heads	SMT (hull)	48	$0.0156$	$0.0125$ $(0.0344)$
Adder transformer	$p{=}5$ , 8 wide, 2 heads	SMT (siamese)	40	$\geq 0.05$ a	$\geq 0.002$ c
Softmax + LN transf.	64 wide, 4 heads, 2 layers	CROWN	448	$0.0091$ d	$0.0079$ , $0.0098$ d

TABLE II: Certified radii

\varepsilon^{\!*}

(Def. 4 ) by subject. Parenthesized values are skill

B

’s radius before the edit, so collateral reads as the drop. Exact removal radii are attained tipping points and exact preservation radii are bracketed within the bisection tolerance (Proposition 2 b,d); bound-propagation radii are sound lower bounds. Values from committed reports (App. D ).

Configuration	Noise vars	$\varepsilon=0$	$\varepsilon=0.005$
8 wide, 1 head, $L=4$	32	✓ 32 s	✓ 155 s
8 wide, 1 head, $L=6$	48	✓ 40 s	✓ 230 s
8 wide, 1 head, $L=8$	64	too loose	too loose
12 wide, 1 head, $L=6$	72	✓ 31 s	timeout
16 wide, 1 head, $L=6$	96	✓ 120 s	timeout
16 wide, 2 heads, $L=8$	128	timeout	timeout

TABLE III: Where exact certification stops. Each row is a configuration of the threshold-gate transformer; each cell is one all-sequences hull query of the unedited model’s skill-

A

claim, without noise or with it. The rule marks the frontier; the exact subject of Table II has the bold row’s size, with two heads.

Appendix figures & tables1 asset

Supplementary material from the paper’s appendix.

Appendix

Result	Script
Softmax + LayerNorm transformer, $448$ noise dimensions: certified $\leq$ attack for removal and both preservation claims (Fig. 2 )	run_boundprop_transformer.py †
Threshold-gate transformer, exact over all sequences: removal $0.016$ , preservation $0.013$ , collateral $0.034\to 0.013$ (Table II )	run_transformer.py
Distributed circuit: neither the attention heads nor the MLP alone removes skill $A$ (Fig. 3 )	results/rung2_circuit_search.py b
Modular-adder transformer: removal as exact independence of the summands, radius ${\geq}0.05$ (§ V-A )	run_rung3.py
Modular-adder transformer: correctness on all $625$ clean sequences, preservation radius ${\geq}0.002$ (§ V-A )	run_rung3_preservation.py
Constructed illusion: passes a $40{,}401$ -point grid with preservation proved, refuted by the solver (Fig. 1 a,b)	run_illusion.py

Appendix

TABLE IV: The command behind each reported result.

Machine Unlearning

Machine unlearning removes the influence of selected data or concepts from trained models while preserving useful behavior and avoiding full retraining.

See all 356 papers

Certified Circuits: Stability Guarantees for Mechanistic Circuits
Feb 26, 2026Alaa Anani, Tobias Lorenz, Bernt Schiele +2Circuit Discovery Mechanistic Interpretability
Max Planck Institute for Informatics, Saarland Informatics Campus, Saarbrücken, Germany · CISPA Helmholtz Center for Information Security, Saarbrücken, Germany
Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees
Feb 18, 2026Itamar Hadad, Guy Katz, Shahaf BassanCircuit Discovery Mechanistic Interpretability
School of Computer Science and Engineering, The Hebrew University of Jerusalem
From Latents to Wires: Surgical Post-Editing on Large Language Models
Sep 26, 2026Jiankai Jin, Xiangzheng Zhang, Zhao Liu +4Language Model Editing LLM Unlearning
AI Security Lab

Feb 26, 2026J/K move · Enter open · S save

Certified Circuits: Stability Guarantees for Mechanistic Circuits

Alaa Anani, Tobias Lorenz, Bernt Schiele, Mario Fritz+1

Max Planck Institute for Informatics, Saarland Informatics Campus, Saarbrücken, Germany · CISPA Helmholtz Center for Information Security, Saarbrücken, Germany

Circuit Discovery Mechanistic Interpretability Circuits in Language Models

Open paper AskPDF arXiv

Understanding how neural networks arrive at their predictions is essential for debugging, auditing, and deployment. Mechanistic interpretability pursues this goal by identifying circuits--minimal subnetworks responsible for specific behaviors. However, existing circuit discovery methods are brittle: circuits depend strongly on the chosen concept dataset and often fail to transfer out-of-distribution, raising doubts whether they capture the concept or merely dataset-specific artifacts. We introduce Certified Circuits, which provide provable stability guarantees for circuit discovery. Our framework wraps any black-box discovery algorithm with randomized data subsampling to certify that inclusion decisions over circuit components--neurons or edges of the model graph, depending on the base algorithm--are invariant to bounded edit-distance perturbations of the concept dataset. Unstable components are abstained from, yielding circuits that are more compact and more accurate. We validate across three architectures (ResNet, ViT, GPT-2) on vision (ImageNet and four OOD datasets) and language (IOI, IOI-Hard, Greater-Than) tasks. Certified circuits achieve up to 56% higher accuracy and up to 80% fewer components, and remain reliable where baselines degrade. Certified Circuits puts circuit discovery on formal ground by producing mechanistic explanations that are provably stable and better aligned with the target concept. Code: https://github.com/AlaaAnani/certified-circuits.

Abstract

Machine Unlearning

Explore similar work

Certified Circuits: Stability Guarantees for Mechanistic Circuits

Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees

From Latents to Wires: Surgical Post-Editing on Large Language Models