文章背景与核心概要

随着现代人工智能模型的不断演进，其架构已经超越了标准的键值（KV）缓存，整合了潜在缓存（latent caches）、学习型稀疏选择器（learned sparse selectors）以及循环状态（recurrent states）等复杂的内存架构。然而，在压缩状态下，这些新型内存架构中的每一类都极易受到独特失效模式的影响。

为了解决这一问题，本文提出了一种跨越所有四种内存类的形式化运行时可观测性契约（runtime observability contract），并通过三个核心算子来实现。该框架的核心亮点包括：通过严格的验证实现错误指标的类型检查（type-check），并利用机器证明定理自动拒绝或桥接无效组合；在真实世界的规模下，在八路并发下经受了 1240 万条目读取的测试，在 CUDA 图操作保持在服务延迟底噪内的同时，严格维持风险预算且零违约；成功应用于配备压缩 KV 原型的生产级 DeepSeek-V4 技术栈中，将静默损坏精准定位到具体的结构边界；同时，所有工件、防护机制以及完整的 Lean 4 形式化开发均已公开。

Runtime Observability for Heterogeneous Attention Memory

arXiv ID: arXiv:2608.05863 [cs.AI]
Submitted: August 6, 2026
Authors: Fanzhe Wei, Li Liu, Ziyang Wang, Chenyu Wang
Links: View PDF | GitHub Repository & Lean 4 Development

arXiv ID: arXiv:2608.05863 [cs.AI]
Submitted: August 6, 2026
Authors: Fanzhe Wei, Li Liu, Ziyang Wang, Chenyu Wang
Links: View PDF | GitHub Repository & Lean 4 Development

Abstract Summary

Modern AI models have evolved beyond standard Key-Value (KV) caches, incorporating complex memory architectures such as latent caches, learned sparse selectors, and recurrent states—each susceptible to unique failure modes under compression.

This paper introduces a formal runtime observability contract spanning all four memory classes through three core operators. Key highlights of the framework include: * Rigorous Verification: Contracts type-check error metrics. Invalid compositions are automatically rejected or bridged via machine-proved theorems, grading claims into certified, partially certified, or empirical tiers. * Real-World Scale: Tested across \(12.4\text{M}\) entry reads under eight-way concurrency, the system maintains strict risk budgets with zero violations while operating within the serving latency noise floor using CUDA graphs. * Structural Localization: Applied to a served DeepSeek-V4 stack featuring a compressed-KV prototype, the framework successfully localizes silent corruptions to precise structural boundaries. * Reproducibility: All artifacts, guards, and the complete Lean 4 formal development are publicly released.

Abstract Summary

Modern AI models have evolved beyond standard Key-Value (KV) caches, incorporating complex memory architectures such as latent caches, learned sparse selectors, and recurrent states—each susceptible to unique failure modes under compression.

This paper introduces a formal runtime observability contract spanning all four memory classes through three core operators. Key highlights of the framework include: * Rigorous Verification: Contracts type-check error metrics. Invalid compositions are automatically rejected or bridged via machine-proved theorems, grading claims into certified, partially certified, or empirical tiers. * Real-World Scale: Tested across \(12.4\text{M}\) entry reads under eight-way concurrency, the system maintains strict risk budgets with zero violations while operating within the serving latency noise floor using CUDA graphs. * Structural Localization: Applied to a served DeepSeek-V4 stack featuring a compressed-KV prototype, the framework successfully localizes silent corruptions to precise structural boundaries. * Reproducibility: All artifacts, guards, and the complete Lean 4 formal development are publicly released.