受保护核心并不足够：认证AI提出的时序规范修订
Protected Cores Are Not Enough: Certifying AI-Proposed Revisions of Temporal Specifications
浏览论文内容
中文总结 AI 辅助
针对AI提议时序规范修订可能削弱受保护需求的问题，提出符号间架构，通过起源版本语义和聚合与核心条件认证确保安全，实验证明聚合优化可掩盖核心失败。
中文摘要 AI 辅助
运行时监控传统上评估一个在执行前固定或在需求变化时外部修改的规范。然而，在基于学习和数据密集的系统中，规范所代表的时序关系本身可能演化。允许AI组件直接替换形式规范是不安全的：它可能过拟合瞬时行为、削弱受保护的需求，或激活统计上不支持的修订。我们引入了一种符号间架构，其中不受信任的AI提议者建议时序规范修订，而符号治理者控制其激活。两个结果组织了该框架。首先，起源版本语义使每个义务的结果对后续修订不变。其次，聚合认证可能掩盖受保护触发器上的系统性失败；同时进行聚合和核心条件后选择认证可控制这两个目标。结构不变量保护设计者保护的组件，提议者无关的生命周期错误界支持重复激活决策。统计界涉及已完成认证样本的可预测均值；将其解释为未来操作有效性需要额外的稳定性假设。受控合成实验使用冻结的监督AI提议者来说明在单个决策和跨重复治理修订中的掩蔽核心失败。提议者是在合成任务上离线训练并在使用前冻结的监督回归器；它按预测聚合边际对候选进行排序，并且从未观察到受保护触发器的成功率，因此掩蔽核心失败源于优化聚合而非手工构建的对手。
英文摘要
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.
发表机构
- University of Insubria（因苏布里亚大学）
机构由 AI 辅助整理，请以论文原文为准。
