Anthropic открыла FlashProve (v0.16.0, Apache 2.0) — исследовательский прототип доказуемого инференса на zkSNARK. Провайдер API один раз публикует commitment-отпечаток весов, не раскрывая сами веса, и снабжает каждый ответ доказательством, что токены выдала именно зафиксированная модель. Доказательство проверяется на обычном CPU за секунды без доступа к весам; сама система пока остаётся инструментом для исследований, а не готовым сервисом.

image

Что произошло

Команда Frontier Red Team опубликовала на GitHub репозиторий anthropics/FlashProve (v0.16.0) под лицензией Apache 2.0 с кодом, инструкциями и техническим отчётом; корректность протокола отдельно закрыта формальными доказательствами в Lean 4. Механика двухэтапная: провайдер один раз вычисляет и публикует commitment-отпечаток весов объёмом около 6,5 МБ, а затем на каждый ответ выдаёт zkSNARK-доказательство примерно на 19 МБ, привязанное к отпечатку и конкретному запросу. Проверяющей стороне достаточно отпечатка, запроса и ответа: верификатор работает на обычном CPU и укладывается примерно в 17 секунд на 24 ядрах (21 секунда на одном ядре), доступ к весам при этом не требуется.

Контекст

Доказуемый инференс долго оставался теорией: с помощью zkSNARK можно доказать, что вычисление выполнила именно заявленная программа, но на больших языковых моделях цена была запредельной. Предыдущая точка отсчёта VerInf генерировала доказательства со скоростью примерно 0,02 токена в секунду при размере доказательства 93,6 ГБ — для живого сервиса это не годилось. FlashProve сдвигает эту экономику: на тестовой модели Llama 4 Maverick (400B MoE, 4-битное квантование, 232 ГБ) подготовка commitment занимает около 39 минут на одном H100 плюс 24 CPU-ядра, один отпечаток амортизируется примерно на 16 млн запросов, а генерация идёт со скоростью около 110 токенов в секунду на H100. Устроен протокол вокруг асимметрии «дорого доказать — дёшево проверить»: доказательства стали в тысячи раз быстрее и легче, поэтому тема впервые переходит из академической плоскости в инженерную.

Почему это важно для индустрии

Для индустрии появляется инструмент доверия, которого раньше не было: провайдер LLM-API может криптографически доказать клиенту, что ответ сгенерировала именно заявленная модель, а не подменённая более дешёвая версия, — актуальная для маршрутизации LLM-трафика проблема, где внутренний выбор модели скрыт за одним интерфейсом. Регуляторы получают способ проверить, что на выделенном железе инферится одобренная модель, а не обучается и не запускается другая. Проверочная сторона уже готова к продуктизации: CPU-верификатор, несколько секунд на проверку ответа. Препятствие на стороне доказательства: генерация несёт GPU-оверхед порядка 70–95x против обычного инференса на vLLM, поэтому сегодня это проектное направление, а не внедряемая фича. Разумный шаг для команд, строящих API-клиенты на критичных процессах, — заранее заложить в архитектуру опциональный слот для проверки происхождения ответа, чтобы включить его, когда стоимость доказательств упадёт.

Почему это важно для пользователей

Готового сервиса нет, но всё нужное для собственной проверки уже открыто: репозиторий anthropics/FlashProve собирается на Linux (g++ 13 и новее, менее 2 ГБ RAM, компиляция 1–2 минуты), после чего можно проверить приложенные доказательства и разобрать формат commitment и файла с доказательством. Доступны также спецификация протокола и формальные доказательства корректности в Lean 4. Для тех, кто строит на LLM-API критичные процессы — безопасность, одобрение документов, аудит, — это задел на то, как в будущем будет доказываться происхождение ответа; реалистичный рубеж на сегодня — эксперимент и подготовка архитектуры, а не боевое применение.

Что пока неизвестно / ограничения

Гарантия узкая по построению: она действительна только для целочисленной версии модели и greedy decoding, поэтому типичные прод-конфигурации с сэмплированием (temperature>0) остаются вне доказанной зоны. Контекст ограничен 1024 токенами, доказательство весит около 19 МБ на запрос, а генерация доказательств несёт GPU-оверхед 70–95x против обычного vLLM-инференса — в продакшен с такими параметрами система не разворачивается. Формальные доказательства в Lean 4 относятся к протоколу, а не автоматически к реализации, поэтому разрыв между спецификацией и кодом нужно проверять отдельно. Аналогии с TLS преждевременны: проверка TLS не зависит от содержимого вычислений, а здесь гарантия привязана к целочисленной арифметике, так что корректная формулировка на сегодня — проверяемый инференс в заданных рамках. Опубликованные цифры получены на собственных тестах команды на Llama 4 Maverick, независимых воспроизведений пока нет.

Источники

Автор

Look at AI, редакция