Multi-agent LLM: верифицированная защита от четырех типов аномалий
Исследователи из Verus (группа верификации программного обеспечения) представили механически верифицированные детекторы и методы предотвращения аномалий параллелизма в multi-agent LLM системах. Работа опубликована на arXiv и описывает формализацию четырех типов аномалий, возникающих при совместном доступе агентов к памяти, векторным индексам и реестрам инструментов.
Как отмечается в статье, multi-agent системы LLM разделяют состояние через долгие операции чтения-генерации-записи. Авторы формализовали четыре аномалии на языке TLA+: stale-generation (устаревшая генерация), phantom-tool (инструмент-фантом), causal-cascade (причинный каскад) и tool-effect reordering (переупорядочивание эффектов инструментов). Эти аномалии являются структурными аналогами классических изоляционных аномалий в базах данных.
Разработана иерархия консистентности L0–L4, где строгое включение каждого уровня верифицировано. Это первая механически проверенная иерархия консистентности для таких runtime-сред. Для верификации использовались 274 обязательства в системе Verus (ноль предположений, ноль допущений; доверенная база — две структурные аксиомы и соответствие мьютексам).
Три реализованных Rust runtime реализуют уровни L0–L1 (пессимистическая блокировка, сериализуемая snapshot-изоляция, default-SI). Каждый из них проверен на аномалию stale-generation и уточнен до своей машины состояний. Уровни L2–L4 верифицированы в режиме исполнения с независимыми от зависимостей методами предотвращения (A3, A6, A2: 0/1000 против 1000/1000). Уровень L2 запущен в live-режиме на трех семействах моделей, где аномалия A3 предотвращена во всех 120 отозванных сессиях.
Практическая значимость работы подтверждена воспроизведением silent lost update в системе deer-flow от ByteDance. Исследователи формализовали исправление как верифицированное уточнение с L0 до L1. Кроме того, обнаружено переупорядочивание эффектов инструментов в ToolNode фреймворка LangGraph на неизмененном выходе; оно устранено с помощью секвенсора порядка коммитов на уровне L3.
По словам авторов, верифицированные детекторы, уточнения и артефакты реализуемости являются основным вкладом, в то время как сами явления и решетка консистентности носят классический характер. Работа открывает путь к более надежным multi-agent системам на основе LLM.
