FlashProve от Anthropic: zkSNARK-пруфы инференса LLM на H100 за 110 токенов/с

⚡ Главное за 5 секунд

• Anthropic выпустила FlashProve — систему zkSNARK-доказательств того, что ответ выдала именно заявленная модель.
• На Llama 4 Maverick (400B, смесь экспертов) один H100 генерирует пруфы со скоростью ~110 токенов/с, размер доказательства — ~19 МБ на запрос в 1 024 токена.
• Код, Lean-доказательства и документация лежат под Apache 2.0, но это промежуточный результат, а не готовый продукт.

🔍 Что случилось

Anthropic выложила исследовательский пост «Progress on provable inference for large language models» и систему FlashProve. Под материалом подписались Roy Rinberg и Alex Allain из Anthropic, Alessandro Chiesa (EPFL, StarkWare), Miranda Christ (MIT, RESI), Rahul Dalal, Giacomo Fenzi (EPFL), Ben Mayer и Guy Weissenberg (EPFL). На Hacker News пост набрал 185 баллов и 87 комментариев.

Проблема, которую решают авторы, звучит просто. Вы платите за конкретную модель, а проверить, что токены пришли от неё, нельзя. Роутинг-сервис мог подменить модель ради экономии, атакующий — переписать поток токенов по дороге. По тексту ответа это не отловить, даже если ответ хороший. Схема такая: провайдер «коммитится» к весам модели, а потом доказывает, что каждый ответ породили именно эти веса. Выбрали zkSNARK — за свойства сокрытия и эффективности. На Llama 4 Maverick (400B-параметр, MoE, 4-битные квантованные веса, целочисленная арифметика на префилле) один H100 выдаёт ~110 токенов/с доказательств при размере пруфа ~19 МБ на запрос в 1 024 токена. Это ~70–95x к GPU-времени самого инференса на vLLM. Открытые системы до этого отставали на порядки. В комплекте — код (прувер, быстрый верификатор на C++, «доказуемо корректный» верификатор на Lean), Lean-доказательства верхнеуровневых утверждений, техотчёт и спецификация протокола, которую написал сам Claude. Он же, по словам авторов, улучшил zkSNARK-схемы для инференса.

🧠 Наш разбор

Меня здесь цепляет не криптография, а признание в тексте: Claude «хорош в оптимизации, но часто принимает решения, которые трудно оценить». Поэтому верхнеуровневые гарантии безопасности выписали на Lean — чтобы человек мог проверить их формально, а не на слово. Это, наша оценка, куда важнее красивых цифр: команда заранее строит клетку для собственного ИИ-ассистента в исследовании.

Что это меняет. Для обычного чата — почти ничего, честно говоря. 70–95x сверху по GPU-времени никто не станет платить за ответ про рецепт борща. А вот независимым оценщикам моделей, аудиторам и корпоративным заказчикам через посредника-роутера — вполне. Мы считаем, что рынок тут не про «доверие к Anthropic», а про аргумент в переговорах: «докажи, что это твоя модель, а не дешёвая подмена». И ещё один слой — требования к «AI pacing», то есть к подтверждению, что провайдер держит ту версию, о которой договорились регуляторы.

Кто выигрывает. Инфраструктурные провайдеры с собственным железом и большие заказчики, которым нужна бумажка. Кто проигрывает — не спешил бы говорить. Открытые системы догонят часть разрыва, а сам FlashProve открыт под Apache 2.0, так что им можно пользоваться. Скорее проигрывают серые роутеры, чей бизнес держится на том, что подмену не видно.

⚠️ Чего мы не знаем

Замеры даны для одной модели и одной конфигурации — Llama 4 Maverick в 4-битном квантовании. Как схема ведёт себя на плотных моделях другого размера и на нестандартных движках, в посте нет. Нет и сравнения с закрытыми промышленными системами: «на порядки быстрее открытых» — это про открытые. Lean-доказательства покрывают верхнеуровневые утверждения, а не весь код. И главное: система прячет веса, но не архитектуру — это прямо оговорено. Проверять цифры стоит по техотчёту, а не по пересказу в комментариях на HN.

Прогноз: в течение двух кварталов появится минимум один внешний форк или независимый бенчмарк FlashProve на другой модели — при условии, что техотчёт даст достаточно деталей для воспроизведения.