Верифицированное обнаружение и предотвращение аномалий конкурентного доступа в многолетных системах на основе больших языковых моделей

Аннотация

Многоагентные системы LLM разделяют состояние через хранилища памяти, векторные индексы и реестры инструментов. Мы моделируем такое разделение как долгоживущие операции чтения-генерации-записи в рамках детерминированной семантики генерации — режима, обеспечиваемого механизмами долговечных вычислений посредством детерминированного воспроизведения — и формализуем четыре аномалии параллелизма в TLA+: устаревшая генерация, фантомный инструмент, причинно-следственный каскад и переупорядочивание эффектов инструмента, структурные аналоги классических аномалий изоляции, каждая с контрпримером в TLC. Решётка исключений для этих аномалий тривиальна; вклад заключается в механически верифицированной реализуемости и строгом разделении одной максимальной цепи внутри неё, L_0 subsetneq cdots subsetneq L_4, которая, насколько нам известно, является первой иерархией согласованности для таких сред выполнения, проверенной на машине. Разработка 274 обязательств Verus (ноль предположений, ноль допущений; база доверия: две структурные аксиомы и соответствие взаимного исключения) доказывает, что детекторы корректны и полны относительно спецификаций, а каждая среда выполнения — своё множество избегания. Три развёрнутые среды выполнения на Rust реализуют L0-L1 (пессимистическая блокировка, сериализуемая изоляция снимков, SI по умолчанию), каждая верифицирована относительно устаревшей генерации и уточнена до своей машины состояний; L2-L4 верифицированы в режиме выполнения с двойниками предотвращения, не требующими зависимостей (A3, A6, A2: 0/1000 против 1000/1000), а L2 работает в реальном времени для трёх семейств моделей (A3 предотвращено во всех 120 отозванных сеансах). Мы воспроизводим тихую потерю обновления в deer-flow от ByteDance, формализуя её исправление как верифицированное уточнение с L_0 до L_1, и демонстрируем переупорядочивание эффектов инструмента в ToolNode из LangGraph на неизменённом выходе, устранённое с помощью секвенсора порядка фиксации L3. Вкладом являются верифицированный детектор, уточнения и артефакты реализуемости; явления и решётка являются классическими.

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.