PaperlayerView exact revision on arXiv

Source-linked AI summary

Certified Mechanistic Edits: Behavioral Guarantees for Skill Removal and Preservation

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

arXiv:2610.03502v1cs.LGcs.AIcs.CR

TL;DR

Mechanistic edits are often evaluated on finite prompts, while the desired guarantee concerns removal and preservation across a continuous input region. This paper formalizes behavioral certificates, proves a limit on deterministic black-box testing, and extends certification beyond exact-solver cases with sound bound propagation.

  • Problem

    Finite test sets check only tested inputs, leaving no guarantee that an edit removes a skill and preserves another throughout a continuous region.

    Source: §I · p. 1, Research gaps · p. 3

  • Method

    The paper formalizes certified edits over continuous input regions and uses exact SMT encoding with sound bound propagation for cases the exact solver cannot handle.

    Source: A. Exact encoding (SMT) · p. 5, §VII · p. 9

  • Results

    No finite deterministic black-box behavioral test can certify removal, and bound propagation extends certification to a standard softmax + LayerNorm transformer.

    Source: C. No finite test certifies removal (P3) · p. 5, §VII · p. 9

  • Takeaways & Limitations

    The framework makes removal and preservation claims for every input in a continuous region rather than only for sampled inputs.

    Source: §VII · p. 9

    The guarantees are demonstrated on small, standard-architecture networks, and bound-propagation results are sound but not exact.

    Source: §VI · p. 8

Abstract

from arXiv · show

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.

I. INTRODUCTION

Mechanistic edits are commonly evaluated on held-out prompts, but those tests cannot establish removal and preservation for every input in a continuous region. The paper develops formal behavioral certificates and distinguishes them from prior certificates of model descriptions or average effects.

I. INTRODUCTION

  • Finite test sets check only the inputs tested, whereas the paper seeks proofs that one skill is removed and another preserved throughout a continuous input region.The guarantee is framed as feature non-interference: the edited component’s output is independent of a forbidden input feature throughout the region.Source: §I · p. 1

Contributions of this paper:

  • Sound bound propagation reaches roughly 9× the exact frontier’s perturbation dimension, alongside a framework for certified edits and an exact SMT method.The framework formalizes certified edits and radii, proves composition and cheap computability, and proves no finite deterministic black-box test can certify removal.Source: Contributions of this paper · pp. 1–2

Scope of the guarantees:

  • The guarantees are demonstrated on small, standard-architecture networks and presuppose a decidable ground-truth specification for the skills being removed or preserved.The paper notes that real harmful capabilities often lack such specifications.Source: Scope of the guarantees · p. 2

II. RELATED WORK: THE DESCRIPTION AXIS VS. THE EDIT AXIS

  • Prior work certifies model descriptions or average effects, while this paper certifies an edit’s worst-case behavioral effect over a continuous region.The paper presents the two certificate types as complementary.Source: §II · p. 2

Research gaps

The paper identifies gaps in certifying an edit’s behavior, the limits of finite deterministic testing, and exact accounts of steering collateral damage. It addresses them with continuous-region certificates, impossibility results, and edit-separation results.

Research gaps

  • 40,401 grid points can still miss a solver-found survivor, illustrating why finite deterministic tests cannot certify removal.The paper identifies the absence of prior certificates for removal of one skill and preservation of another over every input in a continuous region.Source: Research gaps · pp. 2–3, Figure 1 · p. 3
  • The third gap is an exact account of how surgical edits differ from steering in collateral damage; the paper pairs this with continuous-region certificates.The proposed framework uses an SMT solver and extends to sound bound propagation where exact encoding stops.Source: Research gaps · p. 3

A. Definitions

The section defines the network, behavioral claims, edits, and certified radius, then establishes how certified regions compose and how the radius is computed.

A. Definitions

  • The model is a rational-weight, one-hidden-layer ReLU network on [0, 1]^d, with each output coordinate treated as a head.Its inputs map to outputs through W2 ρ(W1x + b1) + b2.Source: A. Definitions · p. 3
  • Removal requires the edited model’s target-head output to be nonpositive throughout its region, while preservation requires a pair of claims on the preserved skill’s regions.A certificate proves the universal claim by showing that a violating input does not exist.Source: A. Definitions · p. 3
  • Ablation zeros selected neurons, a weight edit removes a neuron’s contribution to a head, and steering shifts pre-activations by adding a vector to the hidden bias.Targeted suppression lowers selected neurons by a specified dose.Source: A. Definitions · p. 3
  • The certified radius is the largest inflation of a region for which a claim remains valid, with inflation clipped to the model domain.The executed float64 program can differ from the exact rational network; certificates with slack above the stated rounding bound transfer to execution.Source: A. Definitions · p. 3

B. Regions compose and the radius is computable (P1–P2)

  • Certified regions are downward closed and closed under unions, and radius membership is monotone in inflation; bisection brackets the radius within τ.Removal radii attain their supremum, while preservation guarantees only validity below the supremum; a solver timeout conservatively fails a probe but voids the bracket.Source: B. Regions compose and the radius is… · p. 4

C. No finite test certifies removal (P3)

The paper proves that finite deterministic testing cannot certify removal, and constructs edits that pass tests while retaining a small survivor region.

C. No finite test certifies removal (P3)

  • The intervention illusion is a theorem of the framework, not merely an artifact of particular models.The construction is also executed in the illusion experiment.Source: C. No finite test certifies removal (P3) · p. 4
  • For any finite test set and any δ > 0, an edited model can pass removal tests while retaining a nonempty open survivor set smaller than δ times the removal region.The same construction preserves both claims for skill B over their full regions.Source: C. No finite test certifies removal (P3) · p. 4
  • No finite deterministic adaptive query protocol can both be sound for removal and nontrivial on a region with nonempty interior.The result excludes randomized adaptive testers and white-box analysis from its scope.Source: C. No finite test certifies removal (P3) · pp. 4–5
  • Three hidden neurons form a localized hat-shaped response that vanishes at every test point, while a bias shift makes the edited output exceed zero only on a narrow slab.The slab’s relative volume can be made smaller than δ.Source: C. No finite test certifies removal (P3) · p. 5

D. Surgery vs. steering (P4)

Proposition 4 distinguishes targeted suppression from ablation and characterizes how steering can affect a preserved head’s margin.

D. Surgery vs. steering (P4)

  • Targeted suppression and ablation produce identical edits on D when the dose is at least the maximum targeted-neuron pre-activation over D.The proposition compares their resulting certificates and radii as well.Source: D. Surgery vs. steering (P4) · p. 5
  • Removal-certifying doses form an interval [s*(R), ∞), with finite threshold s*(R) non-decreasing as the region grows.More input wiggle room therefore demands at least as much dose.Source: D. Surgery vs. steering (P4) · p. 5
  • On pattern-stable points, steering shifts a head’s logit linearly with dose; a circuit disjoint from that head causes zero collateral at every dose.When the steering direction is heard by the preserved head, its margin erodes with dose and can be exceeded.Source: D. Surgery vs. steering (P4) · p. 5
  • The one-hidden-layer result makes the surgical-versus-steering comparison a theorem, while its extension to deeper networks remains open because residual terms pass through later nonlinearities.The propositions have machine-checked witnesses, while P1 follows from the universal quantifier.Source: D. Surgery vs. steering (P4) · p. 5

IV. METHOD

The method uses exact SMT proofs where networks fit linear arithmetic and sound bound propagation for softmax and LayerNorm, while reporting the limits of both approaches.

A. Exact encoding (SMT)

  • The exact pipeline encodes rational weights and ReLUs in Z3, proving universal claims by checking whether a violating input is unsatisfiable.Unsatisfiability certifies the claim; satisfiability returns a counterexample, and bisection finds certified radii.Source: A. Exact encoding (SMT) · p. 5
  • A continuous hull relaxation replaces discrete token choices with mixture weights over the embedding simplex, enabling certification without the combinatorial branching of Boolean token selectors.Because the relaxed region contains the discrete inputs, an unsatisfiable query still certifies the discrete claim.Source: A. Exact encoding (SMT) · p. 5
  • The rational-network proof transfers to float execution when its slack exceeds the rounding gap; the reported toy and threshold-gate certificates use slack of 10^-9 and 10^-6, respectively.A zero-margin claim need not transfer to the float program.Source: A. Exact encoding (SMT) · p. 5

B. Bound-propagation extension (CROWN)

  • Because softmax and LayerNorm are outside linear arithmetic, the method uses sound but incomplete CROWN bounds, which can miss true claims but cannot certify false ones.On the toy ReLU MLP, CROWN exactly reproduces the complete SMT solver’s certified radius; this tightness is not established for the softmax subject.Source: B. Bound-propagation extension (CROWN) · pp. 5–6

C. Scope of the bound-propagation results

skills) can be proved over a whole input region on a transformer

The paper certifies removal of one skill and preservation of another over continuous input regions, including on a softmax + LayerNorm transformer. It also shows why finite testing cannot establish removal and measures whether edits make a component independent of a forbidden input.

skills) can be proved over a whole input region on a transformer

  • 448 dimensions—about 9× the exact frontier—support sound bound-propagation certificates on a softmax + LayerNorm transformer, with removal and preservation radii bracketed by attacks.Removal: 0.0091 ≤ 0.03; preservation: 0.0079 ≤ 0.05 and 0.0098 ≤ 0.1; no attack succeeds below a certified radius.Source: skills) can be proved over a whole… · p. 6, Figure 2 · p. 6
  • The certified circuit spans attention and the MLP: disabling either alone leaves skill A firing, while ablating the whole circuit certifies removal and preservation.The circuit is found by greedy search over heads and MLP neurons while preserving skill B.Source: Figure 3 · p. 6

B. No finite test protocol can certify removal

  • A constructed edit passes a 40,401-point grid yet leaves skill A intact; naturally occurring survivor pockets occupied below 1.5 × 10^-6 of the domain.Three such edits arose in 160 models and also passed 1,000 random inputs plus preservation checks.Source: B. No finite test protocol can certify… · p. 6

C. Feature non-interference

  • A two-copy query bounds the worst-case change in skill-A output when only the forbidden input varies; certified influence of zero establishes feature non-interference.On the transformer, influence reaches zero for quote content throughout the region, out to a larger radius than removal itself.Source: Figure 4 · p. 7, C. Feature non-interference · p. 7

D. Removal is robust to input perturbation, up to a certified radius

Certified radii extend guarantees beyond the claimed region and, on toy models, track the edited model’s own decision boundary. The results distinguish surgical edits from steering, map the exact solver’s frontier and its sound extension, and delimit the scope of the guarantees.

D. Removal is robust to input perturbation, up to a certified radius

  • The certified radius inflates the region on which removal or preservation holds; toy-model certified edges approach the edited model’s decision boundary, with a worst gap of 0.0039.Across correctness claims, certified edges reach within 0.0012 of the 0.5 rule for skill A; the remaining gap reflects model decision margin, not prover slack.Source: D. Removal is robust to input… · p. 7, Figure 5 · p. 7

E. Surgical edits certify collateral-free removal, unlike steering

  • Ablation, weight editing, and targeted steering preserve skill B’s radius, whereas diff-of-means steering erodes it with dose until preservation is refuted.On the separated model, the radius falls from 0.0996 to 0.0908 at dose 4 and 0.0656 at dose 16; on the transformer, no dose both removes A and preserves B.Source: E. Surgical edits certify… · p. 7, Figure 6 · p. 8

F. The exact verification frontier and its sound extension

  • Bound propagation reaches roughly 9× the exact solver’s perturbation-dimension frontier and matches exact radii where both methods apply.The exact encoding’s cost is exponential in internal branching; bound-propagation results are sound lower bounds, and attacks bracket results beyond the exact frontier.Source: F. The exact verification frontier and… · pp. 7–8
  • Continuous embedding-space guarantees are not discrete prompt robustness: the smallest single-token swap moves the embedding about 324× the certified ball.Source: F. The exact verification frontier and… · p. 8

VI. LIMITATIONS AND SCOPE

  • The guarantees are demonstrated on small, standard-architecture networks, with exact verification limited by branching and sound bound propagation sometimes loose.The softmax-model edit is a position path-patch rather than a component circuit; the target skill must also have a decidable specification, which real harms may lack.Source: §VI · pp. 8–9

VII. CONCLUSION AND FUTURE WORK

The paper concludes that mechanistic edits can be certified over continuous input regions, while finite deterministic testing cannot guarantee removal. It identifies scaling and real-skill specifications as next steps and reports reproducibility, LLM-use, and ethical practices.

VII. CONCLUSION AND FUTURE WORK

  • The framework proves removal and preservation over continuous regions, proves finite deterministic black-box tests cannot certify removal, and extends soundly beyond the exact frontier on a softmax + LayerNorm transformer.Source: §VII · p. 9
  • The proposed next step is applying bound propagation to pretrained small language models with safety-relevant capabilities and real edits, alongside discrete edit-distance certificates.Applying the machinery to real harms also requires a deterministic or probabilistic way to decide whether an output exhibits the target capability.Source: §VII · p. 9

OPEN SCIENCE

  • Reported numbers are reproducible from committed code and fixed seeds, and the authors say code and reports will be publicly released with the final version.Source: OPEN SCIENCE · p. 9

LLM USAGE CONSIDERATIONS

  • The authors report using LLMs for editorial, coding, and writing assistance, while formal statements, proofs, designs, and numerical results were produced and verified by the authors and machine-checked witnesses.Source: LLM USAGE CONSIDERATIONS · p. 9

ETHICAL CONSIDERATIONS

  • The studied models and skills are toy or known-formula constructs, with no dangerous capability, human-subjects data, personal data, or deployed system involved.Source: ETHICAL CONSIDERATIONS · p. 9

APPENDIX A FULL PROOFS OF P1–P4

The proofs characterize certified regions and radii, then construct edits that pass finite tests despite leaving a skill alive in a small survivor region. They show why deterministic or random testing can miss that region.

A. Proposition 1 (region monotonicity and union closure)

B. Proposition 2 (the certified radius)

  • Certified radii form a downward-closed interval, and continuity attains its boundary for non-strict claims, while strict claims may lose that endpoint.The strict-claim counterexample has S = [0, 0.3), excluding ε* = 0.3.Source: B. Proposition 2 (the certified radius) · p. 10

C. Proposition 3 and its corollaries

  • Three ReLU neurons form a tent bump that vanishes at every finite test point yet creates a positive-measure survivor slab after the main pathway is ablated.The slab is |x0 − c| < w/2 and has relative volume w/(u0 − l0) < δ.Source: C. Proposition 3 and its corollaries · p. 10
  • A uniform test of m points wrongly approves the constructed edit with probability at least (1 − δ)^m ≥ 1 − mδ.The constructed pocket has exact volume; naturally trained illusions’ pocket sizes are estimated by sampling.Source: C. Proposition 3 and its corollaries · p. 10
  • A deterministic tester’s transcript is unchanged by adding the gadget, so even an approving protocol cannot certify removal over the region.The construction applies to adaptive deterministic protocols as well as fixed finite test sets.Source: C. Proposition 3 and its corollaries · pp. 10–11

D. Proposition 4 (edit-class separation)

For one-hidden-layer networks, the edit classes have distinct collateral effects: ablation and suppression admit exact comparisons, while steering can shift a preserved head’s margin with dose.

D. Proposition 4 (edit-class separation)

  • When the suppressed neurons’ outputs vanish across the input box, suppression and ablation produce identical edited models and therefore share every certificate and certified radius.It suffices that the suppression dose is at least each neuron’s maximum pre-activation on the box.Source: D. Proposition 4 (edit-class separation) · p. 11
  • On pattern-stable inputs, steering shifts a head’s logit linearly with dose; disjoint circuits cause zero collateral, while a heard direction can break preservation beyond the head’s margin.The required dose for ablation-style certification is attained and can increase as the certified region expands.Source: D. Proposition 4 (edit-class separation) · p. 11

APPENDIX B EXACT ENCODING DETAILS AND THE FLOAT GAP

The appendices describe the exact rational encoding and float-transfer boundary, alongside bound-propagation setup, reproducibility details, and machine-checked proof witnesses.

APPENDIX B EXACT ENCODING DETAILS AND THE FLOAT GAP

  • The encoding converts every weight to an exact rational and every ReLU to an ite term, proving claims by unsatisfiability of their negations; for our models, the float64 forward-error ceiling is approximately 10^-13.The toy model’s removal, preservation and control certificates re-prove with slack γ = 10^-9.Source: Appendix B · p. 11
  • A zero-margin claim can be exact yet fail in float execution by approximately 10^-16 on about a quarter of a region, marking the transfer argument’s boundary.The reported region-endpoint float differences are approximately 10^-17 and immaterial at the stated margins.Source: Appendix B · p. 11

APPENDIX C BOUND-PROPAGATION SETUP

  • CROWN certifies radii over balls of radius at least 10^-4, with each certified radius bracketed above by a projected-gradient attack.The setup uses chunked bounds with gradients disabled for memory safety.Source: Appendix C · p. 11

APPENDIX D REPRODUCIBILITY

  • Reported results are regenerated by commands with fixed seeds, and the appendix lists runnable checks for P2–P4, including the margin-curve dose sweep.The checks are reported to pass; the table caption identifies a mapping from each result to its script.Source: Appendix D · p. 11, Appendix E · p. 11, Table IV · p. 12

APPENDIX E MACHINE-CHECKED WITNESSES

  • The appendix scripts write result reports, with one script requiring a separate bound-propagation environment and the others requiring numpy and an SMT solver.The listed exceptions write collateral-sweep JSON and rung-two logs.Source: Appendix E · p. 12

Related papers

Loading 2610.03502v1…