Verifizierte Erkennung und Verhinderung von Nebenläufigkeitsanomalien in Multi-Agenten-Systemen mit großen Sprachmodellen

Zusammenfassung

Mehr-Agenten-LLM-Systeme teilen Zustände über Speicher-Repositorys, Vektorindizes und Werkzeugregister. Wir modellieren diese gemeinsame Nutzung als langlaufende Lese-Generiere-Schreibe-Operationen unter deterministischer Generierungssemantik – dem Regime, das dauerhafte Ausführungs-Engines durch deterministische Wiederholung erzwingen – und formalisieren in TLA+ vier Parallelitätsanomalien: Veraltete-Generierung (stale-generation), Phantom-Werkzeug (phantom-tool), Kausalkaskade (causal-cascade) sowie Werkzeug-Effekt-Umordnung (tool-effect reordering), strukturelle Analoga klassischer Isolationsanomalien, jeweils mit einem TLC-Gegenbeispiel. Das Exklusionsgitter über diesen Anomalien ist trivial; der Beitrag ist die mechanisch verifizierte Realisierbarkeit und strikte Trennung einer maximalen Kette darin, L_0 subsetneq cdots subsetneq L_4, nach unserem Wissen die erste maschinengeprüfte Konsistenzhierarchie für solche Laufzeitsysteme. Eine Entwicklung von 274 Verus-Obligationen (null assume, null admit; Vertrauensbasis: zwei strukturelle Axiome und eine Mutex-Korrespondenz) beweist die Detektoren als korrekt und vollständig gegenüber den Spezifikationen und jede Laufzeitumgebung als ihre Vermeidungsmenge. Drei eingesetzte Rust-Laufzeitsysteme realisieren L0–L1 (pessimistisches Sperren, serialisierbare Snapshot-Isolation, Default-SI), jedes verifiziert gegen Veraltete-Generierung und verfeinert auf seinen Zustandsautomaten; L2–L4 sind ausführungsmodus-verifiziert mit abhängigkeitsfreien Präventionszwillingen (A3, A6, A2: 0/1000 gegenüber 1000/1000), und L2 wird live über drei Modellfamilien ausgeführt (A3 in allen 120 zurückgezogenen Sitzungen verhindert). Wir reproduzieren einen stillen verlorenen Update in ByteDances Deerflow, formalisieren dessen Behebung als verifizierte L_0- zu L_1-Verfeinerung und zeigen Werkzeug-Effekt-Umordnung im ToolNode von LangGraph bei unveränderter Ausgabe, entfernt durch einen L3-Commit-Order-Sequenzer. Die verifizierten Detektoren, Verfeinerungen und Realisierbarkeitsartefakte sind der Beitrag; die Phänomene und das Gitter sind klassisch.

English

Multi-agent LLM systems share state through memory stores, vector indices, and tool registries. We model such sharing as long-running read-generate-write operations under deterministic-generation semantics -- the regime durable-execution engines enforce by deterministic replay -- and formalize four concurrency anomalies in TLA+: stale-generation, phantom-tool, causal-cascade, and tool-effect reordering, structural analogues of classical isolation anomalies, each with a TLC counter-example. The exclusion lattice over these anomalies is trivial; the contribution is the mechanically verified realizability and strict separation of one maximal chain within it, L_0 subsetneq cdots subsetneq L_4, to our knowledge the first machine-checked consistency hierarchy for such runtimes. A development of 274 Verus obligations (zero assume, zero admit; trust base: two structural axioms and a mutex correspondence) proves the detectors sound and complete against the specifications and each runtime its avoidance set. Three deployed Rust runtimes realize L0-L1 (pessimistic locking, serializable snapshot isolation, default-SI), each verified against stale-generation and refined to its state machine; L2-L4 are exec-mode-verified with dependency-free prevention twins (A3, A6, A2: 0/1000 versus 1000/1000), and L2 is run live across three model families (A3 prevented in all 120 retracted sessions). We reproduce a silent lost update in ByteDance's deer-flow, formalizing its fix as a verified L_0 to L_1 refinement, and exhibit tool-effect reordering in LangGraph's ToolNode on unmodified output, removed by an L3 commit-order sequencer. The verified detector, refinements, and realizability artifacts are the contribution; the phenomena and lattice are classical.