S-Bus: マルチエージェントLLMの状態調整のための自動リードセット再構築

要旨

可変な自然言語状態を共有する並行LLMエージェントは、構造的競合状態（SRC）を引き起こす。すなわち、書き込み-書き込み競合およびシャード間の古い読み取り競合であり、これらはエージェントの出力を静かに破損させる。既存のマルチエージェントフレームワーク（LangGraph、CrewAI、AutoGen）は、共有状態に対する書き込み所有権のセマンティクスを提供しない。本稿ではS-Busを提案する。これはHTTPミドルウェアであり、その中心的なメカニズムはサーバーサイドのDeliveryLogである。DeliveryLogはエージェントごとのHTTP GET操作のログであり、HTTP/1.1のもとでエージェントSDKの変更なしに、コミット時に各エージェントの読み取りセットを自動的に再構築する。DeliveryLogが提供する一貫性特性、すなわち観測可能読み取り分離（ORI）は、読み取りセットのHTTP観測可能な射影に対する部分的な因果的一貫性であり、エージェントが共有シャードを介して協調する際の構造的競合状態を防ぐ。本稿の3つの貢献：（C1）HTTPトラフィックに基づく自動的な読み取りセット再構築のためのDeliveryLog機構。3層の機械的証拠を伴う：ReadSetSoundnessとORICommitSafetyはTLAPSで機械検証済み（1つの型公理を除く）；N=3での徹底的なTLC検証（20,763,484の異なる状態、違反ゼロ）；Dafnyは9つの帰納的音響性補題を証明。（C2）共有シャード競合スイープにおけるPostgreSQL 17 SERIALIZABLEおよびRedis 7 WATCH/MULTIに対する実証的な構造的競合防止同等性：427,308件のアクティブなHTTP-409競合において、3つのバックエンドすべてでタイプI破損がゼロ。（C3）ORIの動作範囲はトポロジーに依存する：専用シャードワークロードでは意味的に中立；単一シャードの協調書き込みでは有害である。なぜなら、保存が同時矛盾を伝播させるからである。ソースコード：https://github.com/sajjadanwar0/sbus

English

Concurrent LLM agents sharing mutable natural-language state produce Structural Race Conditions (SRCs): write-write and cross-shard stale-read conflicts that silently corrupt agent output. Existing multi-agent frameworks (LangGraph, CrewAI, AutoGen) provide no write-ownership semantics over shared state. We present S-Bus, an HTTP middleware whose central mechanism is a server-side DeliveryLog: a per-agent log of HTTP GET operations that automatically reconstructs each agent's read set at commit time without agent SDK changes under HTTP/1.1. The consistency property the DeliveryLog provides -- Observable-Read Isolation (ORI), a partial causal consistency over the HTTP-observable projection of the read set -- prevents structural race conditions when agents collaborate via shared shards. Three contributions: (C1) The DeliveryLog mechanism for automatic HTTP-traffic-based read-set reconstruction, with three-tier mechanised evidence: ReadSetSoundness and ORICommitSafety machine-checked in TLAPS (modulo one retained typing axiom); exhaustive TLC at N=3 (20,763,484 distinct states, zero violations); Dafny discharges 9 inductive soundness lemmas. (C2) Empirical structural-conflict prevention parity against PostgreSQL 17 SERIALIZABLE and Redis 7 WATCH/MULTI on shared-shard contention sweeps with 427,308 active HTTP-409 conflicts: zero Type-I corruptions across all three backends. (C3) ORI's operating envelope is topology-conditional: semantically neutral in dedicated-shard workloads; harmful in single-shard collaborative writing because preservation propagates concurrent contradictions. Source code: https://github.com/sajjadanwar0/sbus