PaperlayerView exact revision on arXiv

Source-linked AI summary

From Mathematical to Executable Certificates for Machine Unlearning

Ziyu Zhao, Xinyu Wang, Xiaowen Chang, Yixuan He

arXiv:2610.02268v1cs.LGcs.CR

TL;DR

Machine unlearning needs to remove records without the cost of retraining, but mathematical guarantees concern updates while deployed systems release finite-precision artifacts. ExecCert certifies the artifact through native-certificate closure or retraining-reference verification, and experiments show changed release decisions and fewer false releases from stored-equation checking.

  • Problem

    Mathematical unlearning guarantees concern analyzed updates, while deployed systems release finite-precision artifacts, leaving whether the actual release meets its intended contract unresolved.

    Source: §1 · p. 1

  • Method

    ExecCert certifies the executed candidate through native-certificate closure or RRV against current retain-set retraining, with Incremental RRV maintaining evidence across sequential deletion for ridge heads.

    Source: §1 · p. 2, §3.1 · p. 3

  • Results

    Across four published implementations and sequential services, ExecCert changes release decisions and tightens or preserves certificates, while RRV prevents stored-equation false releases and closely tracks realized error.

    Source: §1 · p. 2

  • Takeaways & Limitations

    Release strategy depends on the contract and schedule: native closure checks a source guarantee, while RRV checks current retain-set fidelity and incremental evidence amortizes frequent certification.

    Source: §6 · p. 10

    Incremental RRV covers frozen representations with moderate-dimensional mutable ridge heads and does not establish semantic forgetting or multi-round adaptive privacy.

    Source: §6 · p. 10

Abstract

from arXiv · show

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.

1 INTRODUCTION

Deletion makes full retraining costly, yet mathematical certificates concern analyzed updates rather than the finite-precision artifacts deployed. ExecCert certifies the executed candidate through native-certificate closure or retraining-reference verification, with an incremental ridge-head realization for sequential deletion.

1 INTRODUCTION

  • Machine unlearning seeks lower-cost alternatives to costly retraining, but deployed software releases finite-precision artifacts rather than the mathematical objects analyzed by guarantees.In sequential deletion, the exact retain-set system and rounded service state can diverge, so solving the stored equation accurately—even with zero residual—may not satisfy the intended contract.Source: §1 · p. 1
  • ExecCert checks the concrete executed artifact against a predeclared contract through native-certificate closure or retraining-reference verification (RRV).Native closure bounds a method’s own certificate quantity; RRV certifies fidelity to retraining on the current retain set.Source: §1 · pp. 1–2
  • Incremental RRV maintains certified relations between finite-precision service statistics and exact retain-set statistics, updating proof state through guarded rank-one transitions in O(d^2) work.At release, the maintained evidence is composed into a retraining-reference certificate; On-demand RRV constructs the evidence when certification is requested.Source: §1 · p. 2
  • Across four published implementations, ExecCert changes release decisions, tightens or preserves certificates, and characterizes fidelity; sequential RRV prevents false releases while tracking realized error.On frozen 3B representations with a mutable ridge head, Incremental RRV is cheaper than fresh and maintained verified-factor alternatives once checks become sufficiently frequent.Source: §1 · p. 2

2 RELATED WORK

Prior work studies certified removal, external evidence that deletion was carried out, and verified numerical computation. ExecCert complements these lines by checking whether the concrete artifact meets a release contract against the intended reference.

2 RELATED WORK

  • Certified approximate-removal analyses bound mathematical updates while assuming the deployed artifact realizes them (Guo et al., 2020; Sekhari et al., 2021; Gupta et al., 2021; Chien et al., 2024; Koloskova et al., 2025; Pandey et al., 2026).Exact unlearning targets the same output distribution as retraining but need not literally rerun the original training algorithm.Source: §2 · p. 2
  • Audits, probes, and cryptographic proofs address whether a prescribed computation ran, whereas ExecCert internally checks the artifact against an exact-arithmetic contract; the approaches can compose, since execution evidence does not establish accumulated rounding behavior.The external-verification line includes Thudi et al. (2022); Weng et al. (2024); Eisenhofer et al. (2025); Zhang et al. (2024a); Maheri et al. (2026).Source: §2 · p. 3
  • Verified numerics bounds solutions and updates for fixed systems, but sequential deletion changes the retain-set system, motivating certified transfer from rounded service state to the current reference.Factor validation and residual enclosures remain part of a release certificate even when a numerical factor is maintained.Source: §2 · p. 3

3 FROM MATHEMATICAL TO EXECUTABLE CERTIFICATES

ExecCert models release as checking a candidate against a deployment-declared admissible set. It offers native-certificate closure and retraining-reference verification, with the resulting RRV bound supporting multiple release contracts.

3 FROM MATHEMATICAL TO EXECUTABLE CERTIFICATES

  • The deployment declares admissible set A independently of the candidate; ExecCert certifies only candidates in A, while the policy may repair, recompute, re-encode, or withhold others.Evaluation calls a candidate conforming when it belongs to A and a nonconforming candidate returned as CERTIFIED a false release.Source: §3 · p. 3

3.1 TWO EXECCERT PATHS

  • Native-certificate closure rigorously upper-bounds the source certificate quantity for the executed candidate and certifies it when that bound meets the source threshold.The admissible condition remains the source method’s q(θ; I) ≤ b.Source: §3.1 · p. 3
  • RRV certifies a candidate’s distance to a uniquely specified exact-real retraining target by constructing a rigorous upper bound rather than computing the target exactly.For SPD ridge heads, RRV can be on-demand or incremental; on-demand RRV also uses post-update gradient certificates for strongly convex logistic and softmax heads.Source: §3.1 · pp. 3–4

3.2 CONTRACTS DERIVED FROM THE RRV BOUND

  • For relative parameter fidelity, the absolute RRV bound is translated using the reverse triangle inequality, and certification requires the resulting bound to meet τ_par.The passage states the condition in terms of F > C and the right-hand side being at most τ_par.Source: §3.2 · p. 4
  • For fixed input representations Z, the parameter certificate implies an output-error bound of ∥Z∥_2 C, while an error-centered certificate can be tighter by preserving error direction.Under the stated margin conditions, the certificate also implies per-row decision agreement.Source: §3.2 · p. 4

4 RETRAINING-REFERENCE RELEASE VERIFICATION

Retraining-Reference Release Verification (RRV) certifies an executed candidate against the exact current retain-set reference without explicitly computing that reference. Incremental RRV maintains evidence across deletions and applies it at transactional release checkpoints.

4 RETRAINING-REFERENCE RELEASE VERIFICATION

  • RRV is the main technical route when native certificate closure is unavailable, and Incremental RRV reuses maintained numerical state instead of rebuilding evidence at each request.On-demand RRV constructs evidence when certification is requested; for differentiable strongly convex heads it uses a post-update gradient certificate.Source: §4 · p. 4

4.1 RELEASE-TIME RRV CERTIFICATES

  • RRV bounds a release candidate’s distance to the exact retraining reference without computing that reference, using ridge residual-and-inverse-defect or strongly convex gradient certificates.For fixed readouts, an error-centered refinement preserves the estimated error direction and bounds only the remaining uncertainty.Source: §4.1 · p. 5

4.2 MAINTAINING REFERENCE-TRANSFER EVIDENCE

  • Incremental RRV tracks stored-statistic discrepancies and reusable inverse evidence across deletions, then transfers them to exact retain-set quantities at release.Guarded rank-one transitions cost O(d^2), versus O(d^3) for dense inverse reconstruction; failed guards invoke the configured rebuild.Source: §4.2 · pp. 5–6

4.3 TRANSACTIONAL RELEASE CONFORMANCE

  • Transactional release exposes a candidate only after every declared contract certifies, and any repair, recomputation, or re-encoding that changes it requires recertification.Proof-state rebuilds change verifier evidence without changing the candidate.Source: §4.3 · p. 6
  • With valid initialization, guarded transitions, contract checks, and atomic release, Incremental RRV ensures every released artifact satisfies its declared retraining-reference contracts.Candidate-changing remediation requires recertification.Source: §4.3 · pp. 6–7

4.4 DERIVED RELEASE CONTRACTS

  • Derived release bounds compose with Gaussian and Laplace guarantees, including executable closure of Newton direct-perturbation radii.A final representation can be infeasible when it cannot satisfy the declared contract.Source: §4.4 · p. 7

5 EXPERIMENTS

The experiments test whether release-time certification prevents false releases, reuses evidence efficiently, and changes decisions for published methods and constrained outputs. They compare certification against retraining references and assess when producer precision or output format limits the contract.

5.1 REFERENCE-TRANSFER SOUNDNESS AND TIGHTNESS

  • RRV produces no false releases where stored-equation verification admits nearly all nonconforming candidates, and its certificates stay within about 1% of the independent reference for 95% of outputs.On a separate fixed population, RRV encloses every realized error across the tolerance sweep.Source: §5.1 · p. 7, Figure 2 · p. 8

5.2 EVIDENCE REUSE IN SEQUENTIAL SERVICES

  • Directional Incremental RRV uses roughly 40% of fresh-factor latency at matched coverage, while the norm-ball variant fails because reuse alone does not retain contract-relevant error direction.The maintained factor matches fresh-factor coverage; replacing the readout-norm upper bound with a certified lower bound does not bring norm-ball certificates below tolerance.Source: Table 1 · p. 8, §5.2 · p. 8
  • Directional Incremental RRV crosses fresh construction at about 22 checks per 1,000 requests and cuts lifecycle cost by 42.7% against maintained factor under every-request checking.The crossover is workload-specific, trading continuous proof maintenance against release-time construction.Source: §5.2 · p. 8

5.3 PUBLISHED-METHOD APPLICATIONS

  • Across four published methods, release-time checks preserve or tighten certificates, change release decisions, and identify the fidelity supported by emitted outputs.CEU’s declared tolerance is unsupported, but post-update RRV certifies weaker fidelity for its emitted heads.Source: §5.3 · pp. 8–9, Table 2 · p. 9

5.4 PRECISION AND REPRESENTATION BOUNDARIES

  • BF16 cannot represent an artifact satisfying the declared tolerance, whereas FP16 and FP32 remain feasible, so some failures require changing the producer or encoding rather than tightening verification.Figure 3(b) compares minimum achievable relative error with the declared contract.Source: Figure 3 · p. 9, §5.4 · p. 9
  • With FP32 statistics, fresh-factor on-demand RRV covers materially more conforming candidates than Incremental RRV after proof-only rebuilds, while both achieve complete coverage with FP64 producers.Changing precision also changes the emitted candidate, so this compares producer policies, not certification alone.Source: §5.4 · p. 9

6 DISCUSSION AND CONCLUSION

The discussion distinguishes failures in closing a mathematical certificate, verifier weakness or cost, and limits imposed by the producer or output format. It also sets the scope of incremental certification and the guarantees ExecCert does not establish.

6 DISCUSSION AND CONCLUSION

  • Release-time failure can arise from a certificate that does not close for the executed artifact, a verifier that is too weak or costly, or a producer or format that precludes the contract.ExecCert identifies whether remediation should target verification or the released artifact.Source: §6 · p. 9
  • ExecCert supplements upstream guarantees: parameter or fixed-readout fidelity does not establish semantic forgetting or multi-round adaptive privacy.Incremental RRV covers frozen representations with moderate-dimensional mutable ridge heads.Source: §6 · p. 10

AI USE STATEMENT

  • The authors report using generative AI for code, figure and LaTeX editing, and language polishing, with review and verification of the final content.The authors take responsibility for the final work.Source: AI USE STATEMENT · p. 10

REPRODUCIBILITY STATEMENT

  • The appendix provides proofs, verification details, provenance, protocols, and independent reference construction; the artifact includes implementation, configurations, patches, and canonical records.Source: REPRODUCIBILITY STATEMENT · p. 10

A SCOPE AND LIMITATIONS

ExecCert’s certificates are limited to their declared reference and scope. The incremental proof state currently targets moderate-dimensional mutable heads, and fixed-readout claims cover only representations declared in advance.

A SCOPE AND LIMITATIONS

  • Native closure inherits the source method’s certificate scope, whereas RRV certifies distance only to its uniquely specified retraining reference.Source: A SCOPE AND LIMITATIONS · p. 13
  • Fixed-readout claims cover only representations declared before candidate inspection, and randomized-release calibration assumes a predeclared common noise scale.Adaptive policies that change the scale in response to the candidate require separate analysis.Source: A SCOPE AND LIMITATIONS · p. 13
  • Incremental proof state targets moderate-dimensional mutable heads; extending it to larger trainable blocks requires additional structure because dense inverse evidence does not scale there.A failed guard triggers certified rebuilding at higher cost, with proof-state lifetime governed by conditioning rather than a fixed deletion limit.Source: A SCOPE AND LIMITATIONS · p. 13

B PROOFS OF MAIN RESULTS

The appendix establishes release-time certificates and a guarded incremental verifier, then specifies their arithmetic scope and cost. It also identifies a finite-format condition under which no representable candidate can satisfy the declared relative contract.

B.1 RELEASE-TIME RRV CERTIFICATES

  • Residual–inverse-defect bounds certify parameter error, while an error-centered refinement can tighten fixed-readout bounds and sufficient margins preserve linear decisions.For differentiable strongly convex objectives, a post-update gradient enclosure provides a separate parameter-error certificate.Source: §B.1 · pp. 13–14

B.2 RANDOMIZED RELEASE INTERFACES

  • With a common predeclared noise scale, Gaussian and isotropic radial Laplace interfaces provide release comparisons, with the stated Gaussian parameter not itself a conventional (ε, δ)-DP guarantee.The Laplace comparison uses C = rnom + Cexec when executable closure adds Cexec to an upstream radius.Source: §B.2 · p. 14

B.3 NONSYMMETRIC DEFECT RECURRENCE

  • The nonsymmetric inverse-defect recurrence supports arbitrary stored P when α ≠ 0 and requires O(d^2) arithmetic and O(d^2) state.Source: §B.3 · pp. 14–15

B.4 TRANSACTIONAL CONFORMANCE AND COST

  • Guarded transitions commit only after numerical guards and invariant checks pass, and release checkpoints expose an artifact only after every declared contract certifies.If remediation changes the candidate, it must be certified separately; per-request updates, releases, and rebuilds incur the stated distinct costs.Source: §B.4 · p. 15

B.5 FINITE-FORMAT IMPOSSIBILITY

  • Under Equation (11), the certified numerator lower bound exceeds τpar times the denominator upper bound, so every representable tensor violates the declared relative contract.Source: §B.5 · p. 16

C SOUNDNESS OF INCREMENTAL RRV

  • Incremental RRV’s transactional protocol maintains statistics and inverse-defect evidence, then transfers that evidence to construct release certificates for the concrete candidate.The protocol may rebuild after a failed guard and withholds release when any declared contract remains inconclusive.Source: C SOUNDNESS OF INCREMENTAL RRV · p. 16

C.1 FLOATING-POINT CONVENTIONS AND NOTATION MAP

  • The verifier uses binary64 outward endpoints and explicit arithmetic-scope guards; TF32 and mixed-precision accumulation are outside the certified model.Overflow, nonfinite values, unsafe subnormals, or failed scope checks return INCONCLUSIVE.Source: §C.1 · p. 17

C.2 RETAIN-SET STATISTICS PROOF STATE

Incremental RRV maintains enclosures for retain-set statistics and inverse defects, transfers them into release-time certificates, and uses guarded updates with certified rebuilding when needed.

C.2 RETAIN-SET STATISTICS PROOF STATE

  • Signed rank-one updates maintain enclosures for the retain-set statistics, adding local outer-product and storage-rounding errors after each committed update.Shared FP32/FP64 initialization can hold the exact data target fixed while varying subsequent storage precision.Source: §C.2 · p. 18

C.3 EXACT-DYADIC RETAIN-SET-STATISTICS REBUILD

  • Exact-dyadic accumulation rebuilds retained statistics independently of accumulated update errors, after which successful inverse-state initialization and recertification permit release.Reconstruction does not change the candidate; producer remediation creates a new candidate that must be certified separately.Source: §C.3 · pp. 18–19

C.4 STORED-TO-RETAIN-SET TRANSFER

  • The stored-to-retain-set transfer combines a residual enclosure with inverse-defect evidence, retaining componentwise arrays to preserve directional residual interaction without a dense matrix product.The release path’s row and column norm bounds cost O(d^2), with residual products costing O(d^2c).Source: §C.4 · p. 19

C.5.1 PARAMETER CERTIFICATE

  • The transferred bounds supply the hypotheses for an absolute parameter certificate and, when finite with δret < 1, a relative contract certificate.Source: §C.5.1 · p. 20

C.5.2 FIXED-READOUT ERROR CENTER

  • For a fixed readout, applying the readout to an approximate parameter-error center preserves directional information before bounding remaining uncertainty.Preprocessing the readout is rigorous, and evaluating m readout rows adds O(mdc) work.Source: §C.5.2 · p. 20

C.6.1 STATE INVARIANT AND STRICT INITIALIZATION

  • The maintained inverse state tracks a defect bound for the stored system, initialized strictly before rank-one transitions and transferred to the exact retain-set matrix using the statistics-error bound.Each accepted transition adds local budgets for algorithmic, stored-state, and tracker-evaluation error.Source: §C.6.1 · pp. 20–21

C.6.2 LOCAL ARITHMETIC BOUNDS

  • Local arithmetic bounds check computed intermediates, stored-state updates, tracker evaluation, and denominators before a guarded transition can proceed.A certified denominator guard establishes α > 0 before division; a policy floor may route fragile positive denominators to rebuilding.Source: §C.6.2 · pp. 21–22

C.6.3 RADIUS PROPAGATION THEOREM

  • The propagated-radius theorem combines local error bounds with the previous certified radius, and all three local bounds can be evaluated in O(d^2) work per rank-one update.Strict initialization supplies the base case, and induction establishes the invariant for every guarded tracker update.Source: §C.6.3 · p. 24

D PUBLISHED-METHOD APPLICATIONS

ExecCert is applied post hoc to unchanged candidates from published methods. Across the applications, certificates assess native quantities or retraining-reference fidelity; in the Newton calibration, direction-free composition remains looser than direct bounds at both precisions.

D.1 APPLICATION DETAILS

  • For Newton-update removal, strict native closure can move retraining earlier, while tighter direct recertification can expose a conservative source action without changing the update rule.Source: §D.1 · p. 24
  • CEU’s emitted head is evaluated against a predeclared τpar = 10^-3 retraining-reference contract, characterizing fidelity supported by snapshots alongside its native randomized guarantee.The reference is the unique retained-node mean softmax cross-entropy minimizer with an L2 penalty.Source: §D.1 · p. 24
  • ScaleGUN native closure checks the same aggregate gradient quantity used by its propagation and optimization budget, while leaving the candidate unchanged.Source: §D.1 · pp. 24–25

D.2 NEWTON DIRECT-PERTURBATION CALIBRATION

  • Newton direct perturbation compares native closure around exact-real Newton centers with on-demand RRV against a verified retained-set reference across 100 leave-one-out states.Source: §D.2 · p. 25
  • Direction-free composition remains looser than direct bounds under both execution precisions on the evaluated Newton-perturbation population.FP64 uses an absolute composition–direct gap because its direct bound is near zero in some states.Source: §D.2 · p. 25, Table 3 · p. 25

E.1 EXPERIMENTAL SYSTEMS AND COMMON PROTOCOLS

The experiments compare verification methods under matched protocols, test whether certificates track the exact retain-set reference, and measure how evidence reuse and producer precision affect release decisions and cost. They also examine whether output formats can express artifacts meeting a selected contract.

E.1 EXPERIMENTAL SYSTEMS AND COMMON PROTOCOLS

  • The experiments use a frozen Llama-3.2-3B-Instruct backbone with a 3,073-dimensional binary ridge head, plus DINOv2/CIFAR-10 and RoBERTa/AG-News ridge heads.The service replays seven 1,000-request streams under a 10^-3 release tolerance; controlled studies use 14,000 outputs and 18 stress trajectories.Source: §E.1 · p. 25

E.3 EVIDENCE REUSE AND LIFECYCLE COST

  • The guarantee-matched comparison varies certificate-evidence construction while holding the candidate, fixed readout, release contract, and conformance labels constant.It compares on-demand residual or fresh-factor constructions, a maintained-factor baseline, and two Incremental RRV variants sharing inverse-defect proof state.Source: §E.1 · p. 26, §E.3 · p. 26

E.2 REFERENCE-TRANSFER SOUNDNESS AND TIGHTNESS

  • Every one of 14,000 outputs has τcert ≥ τtrue across the 10^-5–10^-2 tolerance sweep.The independent retained-set audit computes τtrue, while RRV computes the certified threshold τcert.Source: §E.2 · p. 26
  • Stored-equation checking admits nearly all nonconforming candidates, while RRV produces no false release on the matched stress population.The stress experiment varies statistics storage precision across 18 trajectories and labels conformance using independent retained-row reconstruction.Source: §E.2 · p. 26, Table 5 · p. 26

E.3 EVIDENCE REUSE AND LIFECYCLE COST

  • Across 56 checkpoints, margin certificates cover 95.0–95.8% of declared decisions, while the independent audit reports 99.96% mean observed agreement.The audit agreement is not certificate coverage.Source: §E.3 · p. 27
  • 21.5 checks per 1,000 requests mark the directional Incremental RRV/fresh-factor crossover, versus 214.3 for maintained-factor/fresh-factor; no route falsely releases matched states.The routes share candidate-generation work; fresh factor has no per-request proof maintenance, while maintained factor and directional Incremental RRV do.Source: §E.3 · p. 27

E.4 PRECISION AND REPRESENTATION BOUNDARIES

  • Lower-precision proof refreshes occur when a bound exceeds tolerance; every committed refresh restores certification without changing the candidate.Across 4,162 refreshes, the median bound moves from 1.014τ before a committed refresh to 0.830τ afterward; all attempts consume 4.39% of the FP32 lifecycle.Source: §E.4 · p. 27, Table 7 · p. 27
  • The format-compatibility protocol exhaustively evaluates BF16 and FP16 encodings from the same master head to enclose the minimum feasible tolerance τmin.The resulting frontier is shown in Figure 3(b).Source: §E.4 · p. 27

F.1 OFFLINE VERIFIED REFERENCE AND EVALUATION LABELS

Offline labels are grounded in independently reconstructed retained-set references and rigorous error bounds. For the Newton direct-perturbation route, the verifier bounds replay error relative to the exact-real Newton iterate under stated Hessian assumptions.

F.1 OFFLINE VERIFIED REFERENCE AND EVALUATION LABELS

  • Offline labels use retained-row reconstruction, a verified inverse-defect certificate for the retraining solution, and high-precision dyadic reconstruction to confirm classifications.Directed norm bounds and triangle inequalities yield a rigorous relative-error interval, with precision increased until each classification is resolved.Source: §F.1 · p. 28

F.2 NEWTON DIRECT-PERTURBATION REFERENCE CONSTRUCTION

  • The Newton direct-perturbation construction bounds replay-center distance from the exact-real Newton iterate using directed evaluation of a residual formed from exact-real iterate differences.On a convex region containing the exact-real and replay iterates, the Hessian is assumed bounded between mI and MI and L-Lipschitz; TWOSUM represents the exact difference of stored binary64 iterates.Source: §F.2 · p. 28
  • This direct route closes the execution error for the compositional Laplace interface without a retraining reference, unlike the route that encloses a candidate against a verified retained-set reference.Source: §F.2 · p. 28
Loading 2610.02268v1…