Постоянная память (Persistent Memory) в системах с LLM-агентами стала уязвимой поверхностью для атак типа «инъекция» и «отравление». Проблема усугубляется тем, что риски безопасности ограничивают возможность совместного использования памяти между агентами. Команда исследователей во главе с Танцю Цзяном (Tanqiu Jiang) представила архитектуру PerMIT, которая обеспечивает доказуемые гарантии целостности через формальную верификацию и механизм масштабируемого доверия сообщества.
Формальная верификация и Lean 4
В основе PerMIT лежит конечный интерфейс памяти, который медиаторизирует доступ к значениям, полученным из окружающей среды. Архитектура опирается на явное доверие: доверяются только пользовательские входные данные и значения, подтвержденные на «шлюзе» (gate). Исследователи доказали два теоремы целостности, которые были машинно проверены в Lean 4. Эти теоремы гарантируют, что данные из окружения достигают чувствительных действий только после подтверждения шлюзом, а влияние на поведение агента происходит исключительно через то, что отображает шлюз.
Механизм доверия сообщества
Каждая проверка в PerMIT фиксируется как логированное решение о точном содержимом. Это позволяет endorsements (одобрениям) накапливаться между пользователями. Элементы, набравшие достаточное количество одобрений, становятся «подтвержденными сообществом» и больше не требуют верификации. Исследователи доказали свойство совместного масштабирования (co-scaling): по мере роста сообщества риски продвижения отравленных данных и ошибочного исключения полезных знаний снижаются, при этом усилия по верификации на одного пользователя не растут.
Результаты тестирования
Эффективность PerMIT была протестирована на бенчмарке Trojan Hippo и $\tau^2$-bench. В условиях самопроверки и использования легких верификаторов PerMIT зафиксировал 0% успешных атак. На $\tau^2$-bench сообщества из до 90 автономных агентов использовали PerMIT для создания общих баз знаний. В результате не было зафиксировано ни одного случая продвижения прямой инъекции памяти, а созданные знания значительно улучшили показатели новых агентов на тестовых задачах, что открывает путь к безопасному самосовершенствованию агентов во время тестирования.
| Метрика / Параметр | Результат / Значение |
|---|---|
| Инструмент верификации | Lean 4 (машинно-проверяемые теоремы) |
| Успешность атак (Trojan Hippo) | 0% (при самопроверке и легких верификаторах) |
| Масштаб сообщества ($\tau^2$-bench) | До 90 автономных агентов |
| Инъекции памяти в общих базах | Отсутствуют (zero observed) |
| Влияние на новые агенты | Значительное улучшение на held-out задачах |
Источник: arXiv cs.AI ↗