Материал подготовлен автоматически по первоисточникам: ссылки на них — в конце статьи.
Запрещённые политикой вызовы инструментов ИИ-агента можно отсекать до того, как они изменят данные во внешней системе. В не прошедшем рецензирование препринте, где все числа получили сами авторы, LeanGuard не исполнил ни одного вызова, который запрещала его формальная политика на τ2-bench. Для продукта это отделяет способность модели рассуждать от её права отправлять платежи, менять заказы или обновлять учётные записи.
Проверка стоит между моделью и инструментом
LeanGuard не меняет интерфейс агента. Модель получает обычные схемы инструментов и формирует структурированный вызов, но сервер перехватывает его до исполнения. Отдельный адаптер читает актуальное состояние системы, проверяет аргументы и собирает факты, которые нужны политике.
Текст от модели и содержимое ответа инструмента считаются недоверенными. Если в найденной заметке написано, что клиент уже подтвердил перевод, это не становится разрешением. Подтверждение должно поступить из доверенного канала, относиться к конкретному действию и версии данных, а после использования перестать действовать.
Политику пишут на Lean 4. Она включает проверки текущего состояния и правила по истории: например, ресурс нужно сначала прочитать, клиент должен ранее подтвердить именно эту операцию, а одноразовое действие нельзя повторять. Историю можно ограничить конкретным пользователем, диалогом или ресурсом, чтобы действие с одним заказом не разрешало изменение другого.
Для каждого вызова политика задаёт разрешения, обязательные условия и прямые запреты. Наличие общего разрешения не отменяет невыполненное условие. Если данных не хватает, аргумент разобран неправильно или проверка завершилась ошибкой, LeanGuard запрещает вызов: отсутствие свидетельства не превращается в разрешение.
Исполняемый алгоритм проверки сопоставили с независимым описанием политики в темпоральной логике — логике условий, зависящих от последовательности событий. Lean проверяет доказательство при сборке политики, а не строит его заново для каждого запроса. Гарантия относится к границе исполнения: если адаптер верно передаёт состояние, политика описана правильно, а все значимые инструменты проходят через монитор, запрещённый переход не попадёт во внешнюю систему.
Разрешённый вызов сначала записывается в журнал как зарезервированный, а затем отправляется инструменту. Это закрывает промежуток, в котором агент мог бы повторить одноразовую операцию, пока результат первой ещё неизвестен.
Отказ помогает модели исправить действие
После блокировки LeanGuard может вернуть не только сообщение об отказе, но и идентификатор нарушенного правила, факты проверки и подсказку обычным языком. Например, агент узнает, что перед обменом товара нужно запросить подтверждение клиента. Формальную часть определяет политика; текстовая подсказка лишь объясняет её модели и сама не считается доказательством.
Есть и второй путь: Lean перебирает заранее заданные допустимые изменения аргументов. Если агент пытается потратить больше остатка бюджета, поиск может уменьшить сумму, но только когда такое изменение сохраняет намерение пользователя. Исправленный вызов возвращается вместе с доказательством, что политика его допускает, а перед исполнением всё равно проходит обычную проверку с актуальным состоянием.
На DTap доля успешных прямых атак через подсказки снизилась с 57,9% до 5,9%. Для отказов, вызванных значениями аргументов, поиск доказал допустимое исправление в 88 из 252 случаев; медианное время составило 2 мс. Однако исправления проверяли на ранее записанных отказах: действующая среда пока не передаёт их агенту во время задачи.
Проверка охватила пять моделей Qwen на задачах τ2-bench для розницы, авиаперевозок и связи, а также семь прикладных областей DTap. Сравнивали работу без защиты, простой запрет и запрет с объяснением; задачи были англоязычными, а пользователей имитировала программа. В DTap использовали режим без разрешений на запись, поэтому эти результаты лучше отражают защиту систем, где агенту в основном разрешено читать данные.
Архитектура меняет планы для агентов с правом записи
Работа предлагает не улучшать системную подсказку, а вынести право на действие из модели. Такой слой имеет смысл планировать отдельно от агента: схема доверенных фактов, журнал событий, версия состояния и перехват всех вызовов становятся частью серверной архитектуры. Без них доказанная политика не контролирует фактический переход.
Для прототипа, который только ищет информацию, LeanGuard добавит формализацию и поддержку адаптеров без явной пользы. Для агента, который меняет бронирования, проводит возвраты или управляет доступом, подход даёт более жёсткую границу: модель может ошибиться в рассуждении, но её ошибка не обязана стать операцией во внешней системе.
Цена этой границы — ручная работа над спецификацией. Доказательство подтверждает соответствие исполняемой проверки записанным правилам, но не замечает пропущенное бизнес-условие, неверный адаптер или инструмент, который обходит монитор. Ответы модели в свободной форме также остаются вне контроля: LeanGuard управляет вызовами инструментов, а не содержанием текста.
Поэтому работу пока стоит рассматривать как архитектурный образец, а не готовую замену прикладной авторизации. Практический порядок выглядит так: сначала определить критичные переходы и доверенные источники фактов, затем поставить запрет по умолчанию на границе инструментов, после этого добавить объяснения отказов. Поиск доказанных исправлений имеет смысл подключать последним, когда команда ограничила набор допустимых изменений и научилась проверять, что они сохраняют намерение пользователя.
Источники
Похоже на вашу задачу?
Расскажите, что собираете. За полчаса разложим на этапы и назовём сроки — это бесплатно и ни к чему не обязывает.
