Prompt injection искажает вердикт солверов в LLM-петлях

Формальные инструменты, такие как SAT и SMT солверы, всё чаще встраиваются в пайплайны языковых моделей для обеспечения достоверности выводов в критических задачах. Однако новое исследование, опубликованное на arXiv (ID 2606.19588), показывает, что даже при корректной работе солвера пользователь может получить искажённый ответ.

Гибридная система состоит из трёх этапов: формализация вопроса, решение и наррация — перевод результата солвера в читаемый ответ. Ранее изучались первые два этапа, но наррация оставалась пробелом. Исследователи смоделировали LLM-солвер петлю как верифицированную процедуру принятия решений и провели эксперименты с пятью открытыми моделями.

Тесты показали, что применение сертификатных ворот (certificate gating) делает вердикт солвера корректным. Однако при prompt injection злоумышленник может инвертировать подтверждённый вывод, меняя его смысл через разные формулировки и каналы ввода.

В качестве защиты авторы попробовали ужесточённый промпт, который значительно снижает эффективность injection, но не устраняет её полностью. При адаптивной атаке, подстроенной под защиту, обход всё равно возможен.

Комбинация формального анализа и эмпирических данных показывает, что в LLM-солвер петле робастность не распространяется на ответ, который в итоге видит пользователь. Это означает, что даже при формально правильном решении вывод может быть искажён на этапе наррации.

Для практического применения это создаёт риски в системах, где критически важны корректные ответы, например, в безопасности или управлении. Исследователи подчёркивают необходимость дополнительных мер верификации этапа наррации.