用逻辑编程方法解决模型能力安全的验证难题
Capability Safety as Datalog: A Foundational Equivalence
- 将能力安全问题转化为命题逻辑程序求解
- 实现高效增量维护和审计面包含判断
- 适合关注模型安全验证的研究者
我们证明能力安全可精确表示为命题逻辑程序（Datalogprop：一阶逻辑的单元、无函数、无变量片段）的求值，实现了算法与结构结果的迁移。该等价性解决了Spera [2026] 能力超图框架的两个结构性缺陷：缺乏高效的增量维护机制，以及缺少审计面包含的判定过程。等价关系严格成立：能力超图恰好对应该逻辑片段，不多不少。
原文摘要 · Abstract (English)
We prove that capability safety admits an exact representation as propositional Datalog evaluation (Datalogprop: the monadic, ground, function-free fragment of first-order logic), enabling the transfer of algorithmic and structural results unavailable in the native formulation. This addresses two structural limitations of the capability hypergraph framework of Spera [2026]: the absence of efficient incremental maintenance, and the absence of a decision procedure for audit surface containment. The equivalence is tight: capability hypergraphs correspond to exactly this fragment, no more.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。