← 研踪 PaperTrailarXiv:2607.09489 · v3
Ceci n'est pas une pipe: A semantics of justified reliance for AI systems
首次提交 2026-07-10 23:05
版本更新 2026-11-10 00:07
雷达观测 2026-11-10 15:22
摘要
An AI agent may keep a successful check in context after an edit has invalidated its evidence. We give a semantics for specifying when a system may rely on a message and act on it. Reliability checks an asserted claim against accepted domain knowledge, sources, and messages in the selected context. Justified reliance additionally checks current evidence, authority, and the proposed world change. Relational component semantics and event traces represent nondeterministic outputs, iteration, and external changes. We characterise when merging claims preserves derivable conclusion classes, then construct the coarsest permitted quotient whose rules preserve the exact statuses of designated concrete claims. Construction is polynomial for unary rules; deciding even one permitted merge is coNP-complete for acyclic binary rules. This applies completeness and strong-preservation methods to the execution of quotiented rules. We also relate transition safeguards to runtime enforcement. Relative to a supplied set of possible worlds, a sound guard accepts an observation only when every matching world passes the checks. Exact acceptance requires observations that distinguish opposite-decision worlds; choosing sufficient services is NP-complete on explicit finite tables. A complete finite passport-renewal instance, Lean theorem encodings, Z3 instance checks, and an OCaml harness exercise the semantics. Domain knowledge, interpretation, source licenses, and policy remain application inputs.
观测到的版本
相邻记录可能跳过中间版本;首次发现 v2 及以上也会标为版本更新。
v3 · 2026-11-10 00:07 · 最新观测版本
Ceci n'est pas une pipe: A semantics of justified reliance for AI systems
An AI agent may keep a successful check in context after an edit has invalidated its evidence. We give a semantics for specifying when a system may rely on a message and act on it. Reliability checks an asserted claim against accepted domain knowledge, sources, and messages in the selected context. Justified reliance additionally checks current evidence, authority, and the proposed world change. Relational component semantics and event traces represent nondeterministic outputs, iteration, and external changes. We characterise when merging claims preserves derivable conclusion classes, then construct the coarsest permitted quotient whose rules preserve the exact statuses of designated concrete claims. Construction is polynomial for unary rules; deciding even one permitted merge is coNP-complete for acyclic binary rules. This applies completeness and strong-preservation methods to the execution of quotiented rules. We also relate transition safeguards to runtime enforcement. Relative to a supplied set of possible worlds, a sound guard accepts an observation only when every matching world passes the checks. Exact acceptance requires observations that distinguish opposite-decision worlds; choosing sufficient services is NP-complete on explicit finite tables. A complete finite passport-renewal instance, Lean theorem encodings, Z3 instance checks, and an OCaml harness exercise the semantics. Domain knowledge, interpretation, source licenses, and policy remain application inputs.
查看此版本解读 →查看此版本原文 ↗