arXiv preprint ·
Protected Cores Are Not Enough: Certifying AI-Proposed Revisions of Temporal Specifications
- Published
- Source
- arXiv preprint, posted before peer review
- Original
- Read it at arXiv
- Topics
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.
The authors’ abstract, as arXiv lists it. arXiv’s listings, abstracts included, are free for anyone to reuse.
Read it on ReadSearch
Each opens after you create an account, and brings you back to this paper.
More in Logic in Computer Science
More than 83.69% of the zeros of the Riemann zeta function are distinct
When Does Structured Knowledge Help Neural Theorem Proving?
Zero-Storage Procedural Neural Synthesis via Boundary Dynamics: Formal Verification in Lean 4 and Bare-Metal Gauntlet Validation
Jev thinks "I don't know'', but doesn't say it: Introducing Sys1Cal-v1 Dataset for Probability Calibration
Irene: Equivalence Checking of Hybrid Quantum Programs via Structure-Preserving Symbolic Reduction
Get the few papers worth your time in Logic in Computer Science every morning.
ReadSearch reads the new papers in your field each day and brings you the few worth reading, each with its key finding in a sentence.