Detecção e Prevenção Verificadas de Anomalias de Concorrência em Sistemas Multiagente de Modelos de Linguagem de Grande Escala

Resumo

Sistemas multiagente baseados em LLM compartilham estado por meio de repositórios de memória, índices vetoriais e registros de ferramentas. Modelamos tal compartilhamento como operações de longa duração do tipo leitura-geração-escrita sob semântica de geração determinística — o regime que motores de execução durável impõem por meio de replay determinístico — e formalizamos quatro anomalias de concorrência em TLA+: geração obsoleta, ferramenta fantasma, cascata causal e reordenação de efeito de ferramenta, análogos estruturais de anomalias clássicas de isolamento, cada uma com um contraexemplo do TLC. O reticulado de exclusão sobre essas anomalias é trivial; a contribuição reside na realizabilidade verificada mecanicamente e na separação estrita de uma cadeia maximal dentro dele, L_0 ⊊ ... ⊊ L_4, até onde sabemos a primeira hierarquia de consistência verificada por máquina para tais runtimes. Um desenvolvimento de 274 obrigações de Verus (zero assume, zero admite; base de confiança: dois axiomas estruturais e uma correspondência de mutex) prova que os detectores são corretos e completos em relação às especificações e que cada runtime possui seu conjunto de prevenção. Três runtimes Rust implantados realizam L0-L1 (bloqueio pessimista, isolamento de instantâneo serializável, SI-padrão), cada um verificado contra geração obsoleta e refinado para sua máquina de estados; L2-L4 são verificados em modo de execução com gêmeos de prevenção sem dependência (A3, A6, A2: 0/1000 versus 1000/1000), e L2 é executado ao vivo em três famílias de modelos (A3 prevenido em todas as 120 sessões retratadas). Reproduzimos uma atualização perdida silenciosa no deer-flow da ByteDance, formalizando sua correção como um refinamento verificado de L_0 para L_1, e exibimos reordenação de efeito de ferramenta no ToolNode do LangGraph sobre saída não modificada, removida por um sequenciador de ordem de commit L3. O detector verificado, os refinamentos e os artefatos de realizabilidade constituem a contribuição; os fenômenos e o reticulado são clássicos.

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.