AI inference and observability
WitProbe、4種類のアテンションメモリ向けにランタイム・リスク台帳を構築、1,240万回の読み出しで予算超過なし
新たな研究は、型付き誤差契約によってKV cache、latent cache、スパースセレクター、再帰状態の監視を統一し、形式化可能な合成規則をLeanで検証した。公開リポジトリでは論文の数値と67件の定理を再現できるが、アーキテクチャ固有のプローブと完全なサービス基盤は含まれていない。

モデルサービングにおける「メモリ」は、もはや従来のKV cacheと同義ではない。latent cache、圧縮KV、学習ベースのスパースセレクター、再帰状態にはそれぞれ異なる誤差形態があり、監視値を無条件に加算することもできない。WitProbeの研究は、3種類の操作で4種類のアテンションメモリをカバーするランタイム可観測性契約を提案した。各契約では誤差メトリクスを型に組み込み、メトリクスに互換性がある場合に限って合成できる。証明が一部のステップしか対象にできない場合、リクエスト全体の信頼レベルは自動的に「部分認証」または「実証」へ引き下げられ、形式化済みというラベルによって未証明の工程が覆い隠されることを防ぐ。
著者らは5つのアーキテクチャファミリーと6種類のモデル構成について段階別の境界を設定し、それらをリクエスト単位のリスク台帳へ統合した。システムは1,240万回のメモリエントリ読み出しをリプレイし、8-way並列、リクエストごとの独立した予算、ID帰属に失敗した場合はフェイルクローズする設定でテストされた。著者らによると、リスク予算の違反はなかった。常駐CUDA Graphプローブは、事前に宣言されたレイヤーのサブセットのみを観測し、そのコストはサービスノイズの範囲内に収まった。別の圧縮KVプロトタイプ実験では、サイレントデータ破損を構造上の境界まで特定した。エビクションがなく、リクエストスロットが分離されている場合は正確に判定でき、失敗はcache evictionまたはスロット再利用の状況に集中していた。
技術的な価値は、「cache圧縮後も一見正常に見える」という状態を、単なるオフラインの平均品質スコアではなく、実行可能で追跡可能なサービス条件へと置き換えた点にある。公開されたApache 2.0リポジトリには、固定済みの実験データ、数値と図表の再構築ツール、受け入れゲート、67件のLean定理が含まれる。低レベルの結果は、GPUやモデルの重みがない環境でも再現できる。一方、アーキテクチャ固有のhook、adapter、kernel、サービススタックのパッチは公開されておらず、完全な再実行には依然として非公開の8基のHGX GPUプラットフォームが必要となる。今後、エンジニアリングチームは、プローブを主要な推論エンジンへ移植できるか、またスロット再利用とcache evictionにおける失敗境界を独立して再現できるかに注目すべきだ。