Machine unlearning is needed when data must be removed because of deletion requests, outdated records, or data-quality concerns, while retraining from scratch can be costly. Certified machine unlearning methods provide mathematical guarantees, while deployed systems release concrete finite-precision artifacts produced by software. To bridge the gap between mathematical guarantees and practical deployment, we introduce Executable Release Certification (ExecCert), a release-time layer that certifies the candidate artifact considered for release. ExecCert either closes a method's native certificate for the executed candidate or applies Retraining-Reference Release Verification (RRV) to certify fidelity to current retain-set retraining. Sequential deletion makes the latter nontrivial because the exact retain-set reference and the stored numerical state evolve separately. For frozen representations with a mutable ridge head, we develop an incremental realization of RRV that maintains certified evidence across deletion requests rather than reconstructing it at each release. On four published unlearning implementations, ExecCert preserves valid certificates, changes release decisions, tightens conservative bounds, and identifies the retraining-reference fidelity supported by concrete outputs. In sequential-service experiments, RRV eliminates false releases caused by stored-equation verification while closely tracking realized error, and incremental certification remains cheaper than both fresh and maintained verified-factor alternatives once release checks become sufficiently frequent.
Figures & tables
Figure 1: ExecCert certifies a concrete unlearning artifact before release. The generator’s finite-precision output is checked against a predeclared contract through native-certificate closure or retraining-reference verification (RRV). Only certified artifacts pass the policy gate; an inconclusive candidate is withheld or repaired and then recertified.
Figure 2: RRV certificates closely track realized error. Incremental componentwise RRV and independent retained-row reconstruction evaluate the same fixed FP32 deletion outputs at every tolerance. Coverage gap is the conforming fraction minus the certified fraction; certificate inflation is τcert/τtrue−1 . No rebuild or producer remediation changes the population.
Method
Certified release states
Med./P95 (s)
State (MiB)
On-demand RRV (fresh factor)
21/21
2.611/3.593
286.5
Maintained verified factor
21/21
2.453/3.678
358.6
Incremental RRV (norm-ball)
0/21
0.801/0.859
360.3
Incremental RRV (directional)
21/21
1.056/1.163
430.6
Table 1: Verification of the same frozen 3B safety-head outputs. Latency summarizes 10 repetitions at each of 21 states. No method scans retained rows; state excludes those rows.
Method
Release-time outcome
Newton removal
Native closure shifts the retraining boundary by 0–4 requests ; direct recertification also identifies conservative source stops.
Newton direct perturbation
At FP32, the median direct bound is 2.28 × tighter than composition; paired FP64 results retain an absolute gap.
ScaleGUN
All 15/15 cheap-update certificates remain valid.
CEU
Median realized error is 8.9% ; the median certified upper bound is 14.1% .
Table 2: Executable certification on published unlearning methods. ExecCert is applied to the emitted candidate without changing the underlying update rule.
Figure 3: Deployment choices affect certification cost and feasibility. (a) Full-stream maintenance measurements combined with matched release-check timings produce the lifecycle curves. The maintained-factor crossover with fresh construction lies beyond the plotted low-frequency region, at about 214 checks per 1,000 requests. (b) The horizontal axis is the minimum achievable relative error τmin . A format is ruled out when its certified lower bound exceeds the declared contract τpar ; BF16 is unreachable, while equal-size FP16 remains reachable.
Appendix figures & tables5 assets
Supplementary material from the paper’s appendix.
Appendix
Seed
Native
ExecCert
Δ
Direct upper
0
251
249
−2
.00304
1
232
232
0
.00324
2
277
273
−4
.00421
Appendix
Table 3: Detailed published-method application results. Newton-perturbation bounds are normalized by the nominal radius; ScaleGUN ratios report the source budget consumed. Newton ratios are formed per state before aggregation; FP64 uses an absolute gap because its direct bound can be near zero.
Construction
Build at release
Retained rows
Reuse inverse
Readout
On-demand RRV: retained residual
✓
✓
✗
Norm-ball
On-demand RRV: corrected residual
✓
✓
✓ a
Error-centered
On-demand RRV: fresh verified factor
✓
✗
✗
Error-centered
Maintained verified factor
✗
✗
✗
Error-centered
Incremental RRV: norm-ball
✗
✗
✓
Norm-ball
Incremental RRV: directional
✗
✗
✓
Error-centered
Appendix
Table 4: Verification constructions in the guarantee-matched comparison.
Path
Total
Conforming
Certified conforming
False release
FP32 stored equation
9,000
7,293
7,293
1,703
FP32 + Incremental RRV
9,000
7,293
4,838
0
FP64 + Incremental RRV
9,000
9,000
9,000
0
Appendix
Table 5: Matched-output conformance on nine workload configurations per precision. Coverage is conditional on a conforming output. The incremental row reports the first check, before any proof-only rebuild. Four FP32 reference intervals remain unresolved and are not counted as conforming or nonconforming.
Verification method
Retain scan
Certified release states
Med. (s)
P95 (s)
State (MiB)
On-demand RRV (retained residual)
Yes
0/21
5.163
5.410
72.1
On-demand RRV (corrected residual)
Yes
21/21
5.341
5.696
286.5
On-demand RRV (fresh verified factor)
No
21/21
2.611
3.593
286.5
Maintained verified factor
No
21/21
2.453
3.678
358.6
Incremental RRV (norm-ball)
No
0/21
0.801
0.859
360.3
Incremental RRV (directional)
No
21/21
1.056
1.163
430.6
Appendix
Table 6: Complete guarantee-matched results on 21 fixed states. Latency summarizes 10 repetitions per state; stored state excludes retained rows.
On-demand RRV
Incremental RRV
Producer
Certified (%)
Life (s)
State (MiB)
Certified (%)
Life (s)
State (MiB)
FP32
99.97
444.7
11.4
67.24
502.1
20.4
FP64
100.00
378.4
9.1
100.00
413.5
18.2
Appendix
Table 7: Producer precision and certificate construction. Rows change the emitted candidate; within each row, columns compare the same candidates. Coverage is conditional on conformance and uses the final post-rebuild decision; proof-only rebuilds do not change candidates.
Machine unlearning removes the influence of selected data or concepts from trained models while preserving useful behavior and avoiding full retraining.