Détection et prévention vérifiées des anomalies de concurrence dans les systèmes multi-agents de grands modèles de langage

Résumé

Les systèmes multi-agents basés sur des LLM partagent leur état via des mémoires persistantes, des index vectoriels et des registres d'outils. Nous modélisons ce partage comme des opérations de lecture-génération-écriture de longue durée sous une sémantique de génération déterministe – le régime imposé par les moteurs d'exécution durables via le rejeu déterministe – et formalisons quatre anomalies de concurrence en TLA+ : génération obsolète, outil fantôme, cascade causale et réordonnancement d'effets d'outils, analogues structurels des anomalies d'isolation classiques, chacune accompagnée d'un contre-exemple TLC. Le treillis d'exclusion sur ces anomalies est trivial ; la contribution réside dans la réalisabilité vérifiée mécaniquement et la séparation stricte d'une chaîne maximale à l'intérieur de celui-ci, L_0 subsetneq cdots subsetneq L_4, à notre connaissance la première hiérarchie de cohérence vérifiée par machine pour de tels environnements d'exécution. Un développement de 274 obligations Verus (zéro assume, zéro admit ; base de confiance : deux axiomes structurels et une correspondance de mutex) prouve que les détecteurs sont corrects et complets par rapport aux spécifications, et que chaque environnement d'exécution évite son ensemble d'anomalies. Trois environnements d'exécution Rust déployés réalisent L0-L1 (verrouillage pessimiste, isolation par instantané sérialisable, SI par défaut), chacun vérifié contre la génération obsolète et raffiné jusqu'à sa machine d'état ; L2-L4 sont vérifiés en mode d'exécution avec des jumeaux de prévention sans dépendance (A3, A6, A2 : 0/1000 contre 1000/1000), et L2 est exécuté en direct sur trois familles de modèles (A3 empêché dans les 120 sessions rétractées). Nous reproduisons une perte silencieuse de mise à jour dans deer-flow de ByteDance, formalisant sa correction comme un raffinement vérifié de L_0 à L_1, et mettons en évidence un réordonnancement d'effets d'outils dans le ToolNode de LangGraph sur une sortie non modifiée, supprimé par un séquenceur d'ordre de validation L3. Les artéfacts de détection vérifiée, les raffinements et la réalisabilité constituent la contribution ; les phénomènes et le treillis sont classiques.

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.