Provably Safe Model Updates

TL;DR

This paper introduces a formal framework for certifying the safety of model updates in dynamic, safety-critical environments, ensuring models meet specifications despite distribution shifts.

Contribution

It formalizes the problem of safe model updates as computing the largest locally invariant domain and develops a tractable primal-dual approach for certification.

Findings

Efficient certification of model updates independent of data or algorithms

Matches or exceeds heuristic baselines in continual learning and foundation model fine-tuning

Provides formal safety guarantees for model updates

Abstract

Safety-critical environments are inherently dynamic. Distribution shifts, emerging vulnerabilities, and evolving requirements demand continuous updates to machine learning models. Yet even benign parameter updates can have unintended consequences, such as catastrophic forgetting in classical models or alignment drift in foundation models. Existing heuristic approaches (e.g., regularization, parameter isolation) can mitigate these effects but cannot certify that updated models continue to satisfy required performance specifications. We address this problem by introducing a framework for provably safe model updates. Our approach first formalizes the problem as computing the largest locally invariant domain (LID): a connected region in parameter space where all points are certified to satisfy a given specification. While exact maximal LID computation is intractable, we show that relaxing the problem to parameterized abstract domains (orthotopes, zonotopes) yields a tractable primal-dual formulation. This enables efficient certification of updates - independent of the data or algorithm used - by projecting them onto the safe domain. Our formulation further allows computation of multiple approximately optimal LIDs, incorporation of regularization-inspired biases, and use of lookahead data buffers. Across continual learning and foundation model fine-tuning benchmarks, our method matches or exceeds heuristic baselines for avoiding forgetting while providing formal safety guarantees.