Ai suggested changes to system rules need careful checking to stay safe
Protected Cores Are Not Enough: Certifying AI-Proposed Revisions of Temporal Specifications
Logic in Computer ScienceArtificial IntelligenceMachine LearningSoftware Engineering
Summary
Some computer systems use formal rules to decide how they should behave over time. The authors found that letting AI directly change these rules can cause problems, like hiding important failures. They designed a system where AI can suggest changes but a safety controller carefully checks them to keep protected parts safe. Their work shows how to safely let AI propose updates while avoiding hidden errors.
What this means in practice
- •For embedded system developers: Manage safe updates of time-based system rules when incorporating AI-driven revisions in critical devices.
- •For autonomous vehicle engineers: Ensure AI-proposed behavioral rules for vehicles are certified to avoid hidden failures or safety risks.
Tested on simulated data.
Authors
Ruggero Lanotte
Abstract
Runtime monitoring traditionally evaluates a specification that is fixed before execution or externally modified when requirements change. In learning-enabled and data-intensive systems, however, the temporal relationships represented by a specification may themselves evolve. Allowing an AI component to directly replace a formal specification is unsafe: it may overfit transient behavior, weaken protected requirements, or activate statistically unsupported revisions. We introduce an intersymbolic architecture in which an untrusted AI proposer suggests temporal specification revisions and a symbolic governor controls their activation. Two results organize the framework. First, origin-version semantics makes the outcome of each obligation invariant to later revisions. Second, aggregate certification can conceal systematic failures on protected triggers; simultaneous aggregate and core-conditional post-selection certification controls both targets. A structural invariant preserves designer-protected components, and a proposer-independent lifetime error bound supports repeated activation decisions. The statistical bound concerns the predictable means of completed certification samples; interpreting it as future operational validity requires an additional stability assumption. Controlled synthetic experiments use a frozen supervised AI proposer to illustrate the masked-core failure at one decision and across repeated governed revisions. The proposer is a supervised regressor trained offline on synthetic tasks and frozen before use; it ranks candidates by predicted aggregate margin and never observes the protected-trigger success rate, so the masked-core failure arises from optimising the aggregate rather than from an adversary constructed by hand.