S-Bus：面向多智能体 LLM 状态协调的自动读-写集重构
摘要
我们解决 LLM 智能体在 HTTP 环境下共享可变状态的并发控制问题，智能体无法修改以声明读写集。S-Bus 是一种 HTTP 中间件，其核心机制服务器端 DeliveryLog 在提交时从观察到的 HTTP GET 流量中重构每个智能体的读写集。它提供的一致性属性——可观测读隔离（Observable-Read Isolation, ORI），是 HTTP 可观察读投影上的一种部分因果一致性，可防止专用分片拓扑中的结构竞争条件。三项贡献。（C1）DeliveryLog 机制配合三级机械证据：TLAPS 证明了ReadSetSoundness和ORICommitSafety（除一个类型公理外）；TLC 穷举于N=3探索20,763,484个状态并无违例；Dafny 归约9个归纳引理。（C2）与PostgreSQL 17 SERIALIZABLE和Redis 7 WATCH/MULTI的经验安全性平等性：在884,110次提交尝试中（包括427,308次主动争用）零类型I损坏。（C3）ORI 在专用分片工作负载中语义中性，但在单分片协作写入中有害，因为保存会传播并发矛盾。v2 更新：PH-3 LLM 判官现已独立验证于人类标注员（Zahid Hussain，Mindgigs Peshawar）对400个（步骤、分片）配对进行严格Kappa=0.93（n=93，96.8%原始一致性）。LLM 间判官一致性为Kappa=0.46（边界方差）。智能体自报告将超报分片使用率，从32%（LLM 判官）到49%（人类标注员）。SJ-v4 语义质量标尺保持单判官 LLM-only。源代码、形式证明、测试套件、标注数据：https://github.com/sajjadanwar0/sbus
引用
@article{arxiv.2605.17076,
title = {S-Bus: Automatic Read-Set Reconstruction for Multi-Agent LLM State Coordination},
author = {Sajjad Khan},
journal= {arXiv preprint arXiv:2605.17076},
year = {2026}
}
备注
v2: LLM judge validated against human annotator (Zahid Hussain, Mindgigs Peshawar) on PH-3 at strict kappa=0.93 (n=93, 96.8% agreement); over-claim refined to 32% (LLM) / 49% (human). Adds Exp.PG-Comparison Rust-Native and Workload-B chi2=1094.98. 24 pages, 23 tables. Annotation data attached as arXiv ancillary files