发表机构
Koguan School of Law, China Institute for Smart Justice, School of Computer Science, Shanghai Jiao Tong University(上海交大凯原法学院,中国智能司法研究院,计算机学院,上海交通大学)
机构由 AI 辅助整理,请以论文原文为准。AI 中文总结
该研究针对语义透明缓存系统的前提擦除问题,推导了查询恢复的局部结构极限,提出共享模块缓存方案,其性能优于MDS奇偶校验缓存,为推导结构化内容的可靠恢复提供了理论支撑。
AI 中文摘要
我们研究语义透明缓存系统中独立前提擦除下的可靠查询恢复,其中每个缓存对象必须是前提库的逻辑推论。仅当查询仍可从幸存前提和缓存中推导时,恢复才成功。在确定性规范见证机制下,我们证明了查询局部投影定理和精确剩余叶定律:当被擦除的基叶保留到查询的无缓存路径时,恢复恰好失败。单查询设计成为加权部分路径拦截。对于共享工作负载,我们引入语义模块并推导联合和最大误差准则下的精确可靠性定律。在精确模块路由和同质成本下,共享模块缓存恰好最优,而在深度为2的一般有向无环图(DAG)中,最优选择是NP完全问题。与恢复工作负载相关叶有效载荷的编码基准相比,MDS奇偶校验缓存最多差1个数据包即为最优。仅叶透明性产生与擦除率成反比的一阶开销;共享模块将该逆擦除率缩放乘以模块到叶的成本比率,再除以受保护叶的数量。Datalog实例和蒙特卡洛检验验证了该理论。对于具有推导结构的内容,结果提供了函数校正存储的精确随机擦除对应物,以及最大可恢复性的精确分布量化。
英文摘要
We introduce partial path interception on derivation DAGs (directed acyclic graphs), a combinatorial optimization problem arising from proof-valid caching: stored objects must be logical consequences of a premise base whose premises are erased independently, a query is recovered only while derivable from surviving premises and stored objects, and the queried object itself may not be stored, so reliability must come from premises or intermediate consequences. An exact residual-leaf law pins the recovery probability to a closed form in the exposed-leaf count and reduces design to weighted partial path interception (PPI) on the witness DAG. We classify PPI across its canonical regimes: it is NP-complete already on depth-two DAGs with leaf out-degree two and fixed-parameter intractable in the budget, ruling out efficient approximation schemes; it contains smallest T-edge subgraph as a special case, hence admits no approximation within the square root of the optimum under the Strongish Planted Clique Hypothesis, matched there by trivial leaf-only caching; whereas unique-path instances admit an exact dynamic program, bounded-treewidth instances are fixed-parameter tractable, and individual coverage admits a tight logarithmic greedy guarantee. Semantic-module caches are exactly optimal for shared workloads under exact module routing. An appendix prices transparency against a coded erasure benchmark.