Anthropic открыла FlashProve: протокол, доказывающий, какая именно модель ответила

Работая с ИИ через API, нельзя убедиться, что ответила именно выбранная модель: провайдер может незаметно направить запрос на более дешёвую, атакующий — подменить поток токенов. Anthropic 3 ноября опубликовала FlashProve — открытый прототип «доказуемого инференса» (provable inference), который решает эту задачу криптографически, а не репутационно.

Как это работает

Система построена на zkSNARK — разновидности криптографического доказательства с нулевым разглашением. Протокол делится на две фазы:

• Офлайн-фаза. Провайдер публикует обязательство (commitment) к весам модели — короткий «отпечаток», жёстко фиксирующий один конкретный набор весов. Сами веса остаются скрытыми.
• Онлайн-фаза. На каждый запрос провайдер вместе с ответом отдаёт файл доказательства утверждения: «зафиксированная модель на этом промпте выдаёт именно эти токены».

Проверяющий получает обязательство (около 6,5 МБ), промпт и ответ — и проверяет доказательство на обычном процессоре, без доступа к весам.

Цифры

Замеры проводились на Llama 4 Maverick — разреженной модели на 400 млрд параметров (около 17 млрд задействуется на токен) в 4-битном квантовании.

• Генерация доказательств: около 110 токенов в секунду на одном H100.
• Размер доказательства: 18,78 МБ на запрос в 1024 токена.
• Офлайн-фаза: около 39 минут один раз на модель; обязательство действует примерно на 16 млн запросов.
• Проверка: 17 секунд на 24 потоках, 21 секунда на одном потоке.
• Накладные расходы: в 66–77 раз больше времени GPU, чем у vLLM на той же партии из 24 запросов, и до 94 раз при максимальной загрузке.

Для сравнения: опубликованный ранее открытый прототип VerInf доказывал ту же модель со скоростью около 0,02 токена в секунду и выдавал доказательство на 93,6 ГБ, проверка которого занимала почти сутки.

Что внутри и чего пока нет

Код, доказательства на Lean и документация выложены под лицензией Apache 2.0. В репозитории три исполняемых компонента: генератор доказательств, быстрый верификатор на C++ и формально верифицированный верификатор на Lean. Свойства полноты, корректности и нулевого разглашения сформулированы и доказаны в Lean — это ответ на вопрос, почему криптографическому коду можно доверять. Спецификацию протокола написала сама Claude.

Ограничения авторы перечисляют прямо: доказательство относится к целочисленной версии модели при жадном декодировании, поддерживаются только MoE-архитектуры и контекст до 1024 токенов, побочные каналы вроде замера времени генерации в модель угроз не входят. Формального соответствия между быстрым C++-верификатором и Lean-верификатором не гарантируется. Планов внедрять систему у Anthropic нет — это исследовательский артефакт.

Почему это важно

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

Главный вывод из опубликованных цифр — накладные расходы упали с трёх-четырёх порядков до примерно двух. Это ещё не продукт, но уже инженерно осмысленная точка отсчёта.