The authors formally define a certified edit with a certified radius, prove composability and computability (propositions P1–P2), and prove that no finite deterministic black-box test can certify removal (proposition P3), with a constructive witness.
Formal proofs verify skill removal and preservation in neural networks
The authors introduce certified mechanistic edits, providing guarantees over continuous input regions that no finite test can match.
Academic
Md Sazid Uddin · Md. Khairul Alam Mazumder · M. F. Mridha
American International University-Bangladesh (AIUB)
Research Digest··3 min read
The authors formalize and demonstrate certified mechanistic edits: mathematical proofs that a model edit removes a targeted skill while preserving another, for every input in a continuous region.
Why this paper
From American International University-Bangladesh (AIUB)
In one line
Mechanistic edits can be certified via formal proof to remove and preserve skills over continuous input regions, a guarantee no finite test can provide.
What we could check
- ·No code link found
- ·No weights link found
- ·No dataset link found
- ·No compute details found
- ✓Limitations stated by the authors (2 noted)
- ✓Reports numbers on named benchmarks
Observed from the paper text and links we have. Absence here means we did not find it, not that it does not exist.
§