AI 中文总结
研究针对大语言模型智能体通过共享内存协调时内存写入问题，提出事务性信念提交协议MemTX，通过携带多种信息、在事务中暂存写入等方式，经机器检查确保不变量，在多主干上领先基线且无下游危害。
AI 中文摘要
大语言模型智能体越来越多地通过持久共享内存进行协调：一个智能体的写入成为另一个智能体的前提，最终导致具有实际副作用的工具调用。当前的智能体内存系统将每个接受的写入都视为可立即执行的事实，因此受污染的工具结果、过时的更新或队友未完成的记录可能会默默驱动不可逆转的行动。我们认为内存写入不是信念提交。我们提出了MemTX，一种事务性信念提交协议。每个记录都携带证据、权限、来源和有效性。写入在快照隔离事务中暂存，并由验证和提交管道接受，不可逆转的工具调用根据正在进行的信念状态进行控制，撤回信念会触发对其派生记录和工具副作用的类型化级联修复。通过基于属性的测试和对550万个协议状态的有界穷举枚举对两个不变量（动作安全控制和级联修复完整性）进行机器检查，未发现违规情况。在来自三个模型家族的五个主干上，MemTX在四个主干上以配对麦克纳玛显著性领先所有八个基线，在第五个也是最强的主干上与最佳基线在统计上持平，同时仍然是唯一在每个主干上对下游没有危害的方法。主干能力不能替代提交规则。
英文摘要
LLM agents increasingly coordinate through persistent shared memory: one agent's write becomes another agent's premise, and eventually a tool call with real side effects. Current agent memory systems treat every accepted write as immediately actionable truth, so a polluted tool result, a stale update, or a teammate's half-finished note can silently drive an irreversible action. We argue that a memory write is not a belief commit. We present MemTX, a transactional belief-commit protocol. Each record carries evidence, permissions, provenance, and validity. Writes are staged inside snapshot-isolated transactions and admitted by a validate-and-commit pipeline, irreversible tool calls are gated on in-flight belief state, and retracting a belief triggers typed cascading repair of its derived records and tool side effects. Two invariants, action-safety gating and cascade-repair completeness, are machine-checked by property-based testing and bounded exhaustive enumeration of 5.5 million protocol states, with zero violations. Across five backbones from three model families, MemTX leads all eight baselines with paired-McNemar significance on four backbones and statistically ties the best baseline on the fifth and strongest, while remaining the only method with zero downstream harm on every backbone. Backbone capability does not substitute for commit discipline.
CommentsPreprint
