解决多智能体共享状态时的并发冲突问题，无需修改智能体即可自动重建读取集合。
S-Bus: Automatic Read-Set Reconstruction for Multi-Agent LLM State Coordination
- 通过服务器端日志重构每个智能体的读集，实现读操作的可观测隔离。
- 在88万次提交中零类型一错误，安全性能媲美数据库串行化级别。
- 适用于专用分片场景，但需注意在协作写作中可能传播矛盾信息。
我们解决多智能体通过HTTP共享可变状态时的并发控制问题，这些智能体无法被修改以声明其读集。S-Bus是一种HTTP中间件，其核心机制是服务端的DeliveryLog，可在提交时从观察到的HTTP GET流量重建每个智能体的读集。其提供的一致性属性——可观测读隔离（ORI），一种基于HTTP可观测读投影的部分因果一致性——可防止专用分片拓扑中的结构竞争条件。三项贡献：(C1) DeliveryLog机制配备三层形式化验证：TLAPS证明读集完整性与ORI提交安全性（依赖一个类型公理）；TLC在N=3时穷尽探索20,763,484个状态且无违规；Dafny完成9个归纳引理的验证。(C2) 实验表明其安全性与PostgreSQL 17 SERIALIZABLE和Redis 7 WATCH/MULTI持平：在884,110次提交中（含427,308次活跃竞争）零类型一损坏。(C3) ORI在专用分片工作负载中语义中立，但在单分片协作写作中有害，因其会传播并发矛盾。v2更新：PH-3 LLM评判者经独立人工标注者（Zahid Hussain，Mindgigs Peshawar）在400对（步骤，分片）上验证，严格kappa=0.93（n=93，原始一致率96.8%）。跨智能体评判者间一致性kappa=0.46（边界差异）。智能体自述过度声明分片使用量达32%（LLM评判者）至49%（人工标注者）。SJ-v4语义质量评分标准仍为单模型评判者。源代码、形式化证明、测试框架、标注数据：https://github.com/sajjadanwar0/sbus
原文摘要 · Abstract (English)
We address concurrency control for LLM agents sharing mutable state over HTTP, where agents cannot be modified to declare read sets. S-Bus is an HTTP middleware whose central mechanism, a server-side DeliveryLog, reconstructs each agent's read set at commit time from observed HTTP GET traffic. The consistency property it provides -- Observable-Read Isolation (ORI), a partial causal consistency over the HTTP-observable read projection -- prevents Structural Race Conditions in dedicated-shard topologies. Three contributions. (C1) DeliveryLog mechanism with three-tier mechanised evidence: TLAPS proves ReadSetSoundness and ORICommitSafety (modulo one typing axiom); exhaustive TLC at N=3 explores 20,763,484 states with zero violations; Dafny discharges 9 inductive lemmas. (C2) Empirical safety parity against PostgreSQL 17 SERIALIZABLE and Redis 7 WATCH/MULTI: zero Type-I corruptions across 884,110 commit attempts (427,308 under active contention). (C3) ORI is semantically neutral in dedicated-shard workloads but harmful in single-shard collaborative writing because preservation propagates concurrent contradictions. v2 update: the PH-3 LLM judge is now independently validated against a human annotator (Zahid Hussain, Mindgigs Peshawar) on 400 (step, shard) pairs at strict kappa=0.93 (n=93, 96.8% raw agreement). Inter-LLM-judge agreement is kappa=0.46 (boundary variance). Agent self-reports over-claim shard usage by 32% (LLM judge) to 49% (human annotator). The SJ-v4 semantic-quality rubric remains single-judge LLM-only. Source code, formal proofs, harness, annotation data: https://github.com/sajjadanwar0/sbus
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。