Открытый FlashProve доказывает, какая модель написала ответ

Anthropic 3 ноября открыла код FlashProve. Система прикладывает к ответу языковой модели криптографическое доказательство того, что его выдала модель с заранее зафиксированными весами, и сами веса при этом не раскрывает. Главную цифру работы, 110 токенов в секунду на одной H100, надо читать как скорость прогона промпта: при ней в режиме точного совпадения каждое доказательство подтверждает один выданный токен. А проверка полноразмерного доказательства на нашей двухъядерной машине без GPU заняла чуть больше двух минут.

Замеры в исследовательском посте Anthropic сделаны на Llama 4 Maverick, MoE-модели на 400 млрд параметров, в 4-битной квантизации и с целочисленной арифметикой на префилле. Доказательство для запроса в 1 024 токена весит около 19 МБ. Веса оно скрывает, а архитектуру модели система скрывать не пытается. Прувер, два верификатора (быстрый на C++ и доказуемо корректный на Lean) и Lean-доказательства главных утверждений лежат на GitHub под лицензией Apache 2.0. Anthropic делала работу вместе с исследователями из EPFL и MIT, называет её промежуточным прогрессом и прямо просит других взять код и доработать.

Примеры применения Anthropic приводит такие: независимые оценщики убеждаются, что тестируют ту же модель, которую отдают клиентам; клиент сервиса-маршрутизатора проверяет, что токены пришли от оплаченной модели; подмену потока токенов атакующим видно по проваленной проверке. По словам компании, улучшения zkSNARK для инференса нашёл Claude, и раз его решения в большой системе трудно оценивать, ключевые гарантии безопасности записаны на Lean. Цель из своего Frontier Safety Roadmap, прототип к 30 сентября, Anthropic закрыла отдельным проектом, который подписывает её инференс-трафик и пересчитывает инференс на доверенном сервере. FlashProve решает ту же задачу другим методом.

Что значат 110 токенов в секунду

В техническом отчёте 110-111 токенов в секунду - устойчивая скорость префилла. Считаются все 1 024 токена промпта в каждом окне, а в режиме exact match доказательство покрывает прогон по всему промпту и проверяет один токен, который идёт следом. На одно окно уходит около 9,2 секунды. Если проверять ответы целиком под более мягкой политикой clipped gap, с допуском на расхождение, выходит 39,1 токена ответа в секунду (три прогона, разброс ±1,0).

Множитель 70-95 из поста тоже собран из двух разных сравнений с vLLM по GPU-времени: 71,4 раза против префилла 24 окон сразу и 93,0 раза против префилла при самой высокой испробованной нагрузке. На декодировании при 512 потоках разница 20,1 раза. vLLM при этом обслуживал FP8-чекпойнт на восьми H100 и на других машинах.

Прежние открытые системы, по словам Anthropic, медленнее на порядки. Технический отчёт ставит FlashProve рядом с четырьмя из них (VerInf, zkLLM, DeepProve и Attestable), но коэффициентов сознательно не приводит: машины, модели и доказываемые утверждения у всех разные.

Exact match или допуск

В режиме exact match ответ проходит, только если каждый его токен совпадает с выбором целочисленной версии модели, которую и доказывает FlashProve. По документации репозитория, ни один из 96 ответов стокового vLLM в 16 битах и ни один из 96 в FP8 такую проверку бы не прошёл: в одном замере топ-токен целочисленной модели расходился с 16-битной в 6,81% позиций. Эти цифры Anthropic получила Python-реализацией модели, а не выпущенными программами, и мы их не перемеряли. Поэтому ожидаемый режим - clipped gap, и для него теорема на Lean утверждает только, что вывод укладывается в политику; что его выдала модель, она не доказывает.

Гарантии Lean относятся к верификатору и протоколу на Lean, в режиме exact match и в модели случайного оракула, где хеш-функция считается идеально случайной. Верификатор на C++, который пользователи и запускают, и CUDA-прувер в README названы протестированными, но не верифицированными. Положительный ответ, по разделу об ограничениях, значит лишь, что вывод соответствует зафиксированным весам: чьи это веса и какая это реальная модель, он не говорит. Свои 128 бит стойкости C++-верификатор считает с 32 битами proof of work, без них остаётся 96,23 бита. По собственной проверке Anthropic (один прогон на одной машине), все 592 112 объявлений Lean-библиотеки опираются только на три стандартные аксиомы Lean; эту сборку мы не повторяли.