AI inference and observability
WitProbe Builds a Runtime Risk Ledger for Four Types of Attention Memory, With 12.4 Million Reads Staying Within Budget
A new study uses typed error contracts to unify monitoring across KV caches, latent caches, sparse selectors, and recurrent states, while using Lean to verify formalizable composition rules. The public repository can reproduce the paper’s figures and 67 theorems, but excludes architecture-specific probes and the complete serving platform.
Model-serving “memory” is no longer synonymous with the conventional KV cache. Latent caches, compressed KV, learned sparse selectors, and recurrent states each have distinct forms of error, and their monitoring values cannot simply be added together. The WitProbe study proposes a set of runtime observability contracts that use three operations to cover four types of attention memory. Each contract encodes its error metric in the type system and can be composed only with contracts that use compatible metrics. If a proof covers only some stages, the confidence level for the entire request is automatically downgraded to “partially certified” or “empirical,” preventing a formal label from obscuring unproven steps.
Across five architecture families and six model configurations, the authors establish per-stage bounds and then compose them into a risk ledger for each request. The system replayed 12.4 million memory-item reads and was tested with eight-way concurrency, independent per-request budgets, and fail-closed behavior when identity attribution failed. The authors report no risk-budget violations. A resident CUDA Graph probe observes only a predeclared subset of layers, with overhead remaining within the range of normal serving noise. A separate compressed-KV prototype experiment localized silent data corruption to structural boundaries: detection was exact when there was no eviction and request slots were isolated, while failures were concentrated in cache-eviction and slot-reuse scenarios.
The technical contribution is to turn “the cache still appears to work after compression” into an executable, traceable serving condition rather than merely an offline average quality score. The public Apache 2.0 repository includes frozen experimental data, tools for reproducing figures and numerical results, acceptance gates, and 67 Lean theorems. Low-level results can be reproduced without GPUs or model weights. However, the architecture-specific hooks, adapters, kernels, and serving-stack patches have not been released, so a complete rerun still depends on a private eight-GPU HGX platform. Engineering teams should next watch whether the probes can be ported to mainstream inference engines and whether the reported failure boundaries under slot reuse and cache eviction can be independently reproduced.