Прогресс в области доказуемого вывода для больших языковых моделей02.11.2026 03:00

Рой Ринберг (Anthropic), Алекс Аллейн (Anthropic); Алессандро Кьеза (EPFL, StarkWare), Миранда Крист (MIT, RESI), Рахул Далал (Anthropic STEM Fellows Program, Succinct), Джакомо Фенци (EPFL), Бен Майер (Anthropic Fellows Program, MIT), Гай Вайссенберг (EPFL)

Краткое изложение

Когда вы разговариваете с другом лично, у вас есть множество способов убедиться, что это действительно он: вы можете его видеть и слышать, пожать ему руку. Когда вы общаетесь с моделью ИИ, таких способов почти нет. Сегодня пользователь, отправляющий запрос модели, не может проверить, что ответ действительно получен от конкретной модели, которую, по словам разработчика, использует сервис, а не от модели, тайно подменённой маршрутизатором ради экономии или даже злоумышленником, изменившим поток токенов. Судить только по ответу модели ненадёжно, даже если она выдаёт качественные результаты. Криптографические доказательства инференса решают эту проблему: они позволяют поставщику модели зафиксировать модель, а затем доказывать, что каждый ответ создан именно ею. Такие доказательства могут найти применение в самых разных сферах — от потребительских продуктов до внутренней безопасности — и стать частью набора инструментов для проверки соблюдения требований по сдерживанию темпов развития ИИ.

В частности, мы добились прогресса в создании мощного типа криптографических доказательств, известного как «zkSNARK», особенно хорошо подходящего для доказуемого инференса благодаря свойствам сокрытия информации и высокой эффективности. В этой статье мы рассказываем о некоторых результатах, прежде всего о системе FlashProve. Краткое техническое описание выглядит так:

1. Claude усовершенствовала zkSNARK для инференса и создала систему, значительно более быструю, чем предыдущие системы с открытым исходным кодом.
   1. Для большой модели (Llama 4 Maverick — смеси экспертов с 400 млрд параметров) один графический процессор H100 генерирует доказательства со скоростью около 110 токенов в секунду; размер доказательства составляет примерно 19 МБ на запрос из 1 024 токенов при использовании 4-битных квантованных весов и целочисленной арифметики на этапе предварительной обработки. Это примерно в 70–95 раз больше времени работы графического процессора, чем занимает запуск самой модели с помощью vLLM — распространённой библиотеки с открытым исходным кодом.
   2. Предыдущие системы с открытым исходным кодом на порядки медленнее, о чём мы рассказываем в разделе 6. Claude нашла новые способы применять передовые инструменты из научных работ по криптографии и безопасности, опираясь при этом на хорошо зарекомендовавшие себя принципы проектирования систем криптографических доказательств. Фиксация модели и последующие доказательства инференса скрывают веса модели; сокрытие архитектуры модели не является целью этой системы.
2. Claude хорошо справляется с оптимизацией, но часто принимает решения, которые сложно оценить, особенно в больших сложных системах. Чтобы противодействовать этому, мы предоставляем аудируемые утверждения верхнего уровня на языке Lean (языке формальной верификации), описывающие заявленные гарантии безопасности.

Сегодня мы публикуем пять материалов:

• эту статью в блоге, в которой описывается наша система и её возможные применения;
• технический отчёт с подробным описанием системы;
• описание протокола;
• исполняемый код, включающий средство создания доказательств и два средства проверки: быстрое средство проверки на C++ и средство проверки с доказанной корректностью на Lean; и
• доказательства на Lean для математических утверждений верхнего уровня, а также интерактивный визуализатор теорем Lean, помогающий проводить аудит.

Мы публикуем код, доказательства на Lean и документацию на условиях лицензии Apache 2.0.1 Эта исследовательская статья призвана рассказать о промежуточных результатах, а не представить завершённую исследовательскую программу. Мы открыто делимся этой работой, чтобы другие могли изучить её, воспользоваться нашими наработками и развить их дальше.

Введение

Сегодня пользователь, отправляя запрос модели ИИ, никак не может достоверно знать, что ответ сгенерировала именно выбранная им модель. Для повседневных задач, где пользователей в основном интересует результат, а не конкретная модель, это не столь острая проблема. Однако есть ситуации, в которых такая уверенность была бы полезна. Например, независимым экспертам, тестирующим модели ИИ до и после выпуска, нужно знать, что им предоставлена именно та модель, которую они оценивают. Клиенты, обращающиеся к модели через сторонний сервис маршрутизации, хотят быть уверены, что токены получены от оплаченной ими модели. А если киберзлоумышленник изменит поток токенов, выдавая себя за определённую модель, пользователь не сможет обнаружить подмену, просто изучив ответ.

Однако обеспечить проверку ответов моделей непросто. Веса большинства передовых моделей не раскрываются, а даже если бы пользователь имел к ним доступ, проверка того, что конкретный ответ был получен от модели с этими весами, потребовала бы запустить модель. Для этого нужны вычислительные ресурсы, значительно превосходящие возможности обычного пользователя или даже эксперта.

Цель доказуемого инференса (PI) — дать пользователю с ограниченными вычислительными ресурсами возможность проверить, что ответ получен от запрошенной модели, не располагая никакой информацией о её весах. PI обусловлен стремлением укрепить доверие клиентов к поставщикам ИИ, а также — поскольку он позволяет давать гарантии независимым экспертам и помогает поставщикам подтверждать выполнение определённых обязательств и требований законодательства — имеет значение для сдерживания темпов развития передовых систем ИИ и регулирования ИИ.

Один из способов реализовать PI — использовать криптографический объект, называемый кратким аргументом с нулевым разглашением: поставщик модели вместе с заявленным ответом отправляет короткое доказательство (например, размером в несколько мегабайт), которое пользователь может проверить быстро (в идеале — за несколько секунд на центральном процессоре). Если заявленный ответ не соответствует указанной модели, проверка пользователя завершится неудачей. Важно, что криптографические методы гарантируют: доказательство не раскрывает ничего о весах модели.

Сегодня мы публикуем FlashProve — быстрый прототип доказуемого инференса с открытым исходным кодом. Для модели-смеси экспертов с 400 млрд параметров (Llama 4 Maverick, 4-битное квантование) мы показываем, что один графический процессор H100 генерирует доказательства со скоростью более 100 токенов в секунду, а размер доказательства составляет около 19 МБ на запрос из 1 024 токенов. Это примерно в 70–95 раз больше времени работы графического процессора, чем vLLM — распространённой библиотеки с открытым исходным кодом — требуется для обработки запросов той же длины.

Вместе с выпуском мы публикуем исполняемый код, формализацию на Lean и техническое описание протокола. У нас две цели: (i) ускорить и облегчить разработку доказуемого инференса и (ii) показать, что краткие аргументы с нулевым разглашением практически применимы для доказуемого инференса.

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

Проблемы доверия на фоне распространения ИИ

Развитие искусственного интеллекта и его растущая роль в цифровой инфраструктуре и экономике ставят перед поставщиками ИИ вопросы доверия, на которые им необходимо ответить. Решать эти и другие задачи помогают инструменты доказуемого инференса (PI).

Инструменты PI могут быть аппаратными, программными или сочетать оба подхода. Здесь мы сосредоточимся исключительно на программном решении — криптографическом инструменте под названием «zkSNARK» (краткий аргумент знания с нулевым разглашением). Если говорить упрощённо, zkSNARK — это система, позволяющая доказывающей стороне убедить проверяющую сторону с помощью короткого «сертификата» в том, что заданное вычисление было выполнено правильно. Важно, что сертификат обеспечивает нулевое разглашение: он не раскрывает никакой информации сверх той, что следует из корректности вычисления; кроме того, он краткий — проверка занимает экспоненциально меньше времени, чем выполнение доказуемого вычисления.

Ниже мы описываем несколько проблем и объясняем, как zkSNARK помогают их решать.

Проблема 1: сдерживание темпов развития

Некоторые предложения по регулированию и сдерживанию темпов развития ИИ предполагают контроль за оборудованием и его использованием. Например, поставщика могут обязать использовать оборудование для инференса, а не для обучения новой мощной модели. Поставщик может попытаться обойти это требование: запускать более дешёвые модели или использовать вычислительные ресурсы непредусмотренным образом, высвобождая мощности для обучения. Как регулирующий орган может надёжно убедиться, что оборудование действительно используется для инференса?

Как могут помочь zkSNARK: регулирующий орган может запросить у поставщика сертификаты для запросов инференса, обработанных за определённый период. Сертификаты должны подтверждать, что запросы были обработаны заявленной моделью. Недобросовестный поставщик не сможет выполнить это требование, если его оборудование действительно не обслуживало нужную модель. С помощью zkSNARK регулирующий орган сможет проверить достоверность заявлений поставщика, не прибегая к сложной аппаратной инфраструктуре, которая может быть у самого поставщика. При этом поставщик будет уверен, что регулирующий орган не узнает конфиденциальные сведения о модели.2 Отметим, что такая проверка подтверждает использование оборудования для инференса, но не устанавливает, что это же оборудование, например, параллельно не используется для обучения.

Проблема 2: обнаружение подмены

По мере роста ценности моделей ИИ серверы, на которых они работают, становятся особенно привлекательными целями. Злоумышленник или недобросовестный сотрудник может скомпрометировать сервер инференса, чтобы похитить веса, выдавать пользователям вредоносные ответы (например, заражать их компьютеры вредоносным ПО) и совершать другие действия, при этом маскируясь под настоящие ответы. Злоумышленник не обязательно должен быть внешним. По мере того как модели учатся совершенствовать и развёртывать себя, более продвинутая модель может подменить собой разрешённую и выдать себя за более слабую, чтобы избежать классификаторов и мониторинга, которые применялись бы к ней. В обоих случаях возникает один и тот же вопрос: как компании убедиться, какие именно веса фактически используются на её серверах? В нашей дорожной карте безопасности передовых ИИ-систем Anthropic поставила публичную цель создать прототип для проверки трафика инференса:»К 30 сентября 2026 года мы разработаем прототип доказуемого инференса — метода, позволяющего надёжно и доказуемо «подписывать» выходные данные моделей ИИ так, чтобы их можно было связать с конкретным набором весов модели.» Как сообщалось в обновлениях нашей Политики ответственного масштабирования (RSP), мы выполнили эту цель в рамках отдельного, но связанного проекта, который подписывает наш трафик инференса и повторно вычисляет результаты инференса на доверенном сервере. Работа, описанная в этой статье, преследует ту же цель, но использует другой метод.3

Как могут помочь zkSNARK: поставщик может требовать от сервера действительный zkSNARK для каждого ответа. Доказательство связано с конкретной фиксацией весов, поэтому оно подтверждает не просто то, что ответ сгенерировала какая-то модель, а то, что его сгенерировала именно зафиксированная модель. Злоумышленнику, скомпрометировавшему сервер, или модели, подменившей другую, придётся создавать действительные доказательства для ожидаемых весов, чтобы избежать обнаружения, но сделать это они не смогут. Пользователь тоже может получать доказательства: они не раскрывают внутреннюю информацию благодаря нулевому разглашению и быстро проверяются благодаря краткости. Это ограничивает возможности злоумышленника при использовании API инференса.

Проблема 3: подтверждение происхождения текста

Иногда требуется доказать, что на изучение или анализ чего-либо были потрачены значительные усилия. Например, разработчик может заявить, что его программная библиотека прошла проверку на уязвимости с помощью передовой модели для кибербезопасности, или компания может утверждать, что её бизнес-план одобрила подходящая модель. Как пользователь может проверить такие заявления? Возможно, у него нет ресурсов для самостоятельного запуска модели или необходимого допуска. Даже публикация журналов переписки не даёт абсолютных гарантий: теоретически разработчик может подделать их, сгенерировав не передовой моделью, а более дешёвой или урезанной версией. В целом, как пользователям проверить, что им отвечает выбранная ими модель?

Как могут помочь zkSNARK: поставщик может прикладывать к каждому ответу zkSNARK, доказывающий, что результат был получен заявленной моделью на основе заданного ввода. Благодаря краткости пользователь сможет быстро проверить сертификат без специального оборудования, а нулевое разглашение гарантирует поставщику, что пользователь ничего не узнает о конфиденциальных весах. Этот подход дополняет существующие механизмы проверки того, какая модель создала ответ.

Например, в мире, где уязвимости обнаруживаются регулярно, перед выпуском нового кода поставщик модели мог бы предоставить разработчику кода доказательство неудачи, подтверждающее, что поставщик потратил на определённую модель не менее X токенов и не добился конкретного результата (например, что эта модель не обнаружила ошибок в определённом исправлении, хотя на попытки было потрачено не менее 1 млн токенов).

Проблема 4: одобрение моделей

Регулирование может обязывать поставщиков предоставлять только модели, одобренные как безопасные, а не модели, признанные угрозой кибербезопасности или безопасности в целом. У поставщика может быть стимул обходить это требование, поскольку рискованные модели могут превосходить конкурентов или обходиться дешевле. Как регулирующий орган может гарантировать, что используются только одобренные модели?

Как могут помочь zkSNARK: регулирующий орган может требовать, чтобы поставщик прикладывал zkSNARK к своим ответам, тем самым обеспечивая использование одобренных моделей. Доказательство связывает каждый запрос с использованной моделью, поэтому проверка не пройдёт, если поставщик использует неодобренную модель. Благодаря краткости регулирующий орган сможет легко проверить это, не выполняя каждый запрос повторно.

Несколько слов о PI на основе доверенного оборудования. В предыдущих работах для реализации PI часто используют доверенные среды исполнения. Это аппаратные решения, обеспечивающие конфиденциальность и аттестацию, которые полагаются на то, что производитель выпускает защищённое от взлома оборудование. В этом исследовании мы сосредоточились исключительно на программных криптографических решениях, безопасность и конфиденциальность которых основаны на вычислительной сложности математических задач. Даже в случае скомпрометированной среды (оборудования, операционной системы и прочего) злоумышленник не сможет создать недействительное доказательство, не решив задачу, вычислительно недоступную для него. Доверенное оборудование и криптография — взаимодополняющие подходы с разными гарантиями и компромиссами. Оба будут важны для решения описанных выше проблем доверия.

Наша система: FlashProve

FlashProve — это система доказуемого инференса для крупных языковых моделей типа «смесь экспертов» (MoE). Подробнее о ней рассказано в нашем техническом отчёте; здесь мы кратко опишем систему.

В работе FlashProve участвуют две стороны: поставщик модели (доказывающая сторона) и пользователь (проверяющая сторона). Система состоит из двух этапов:

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

При вычислении зафиксированная модель выдаёт эти выходные токены.

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

Гарантии

Файл доказательства обладает свойствами «полноты» и «неподделываемости»:

• Если файл доказательства создан добросовестно, он принимается (полнота). Проверяющая сторона принимает доказательство добросовестной доказывающей стороны.
• Файл доказательства невозможно подделать (неподделываемость). Создать действительное доказательство ложного утверждения фактически невозможно (это равносильно нарушению широко признанных криптографических предположений), поэтому проверяющей стороне не нужно доверять доказывающей.

Полноты и неподделываемости можно добиться и с помощью вычислительно мощной проверяющей стороны, которой известны веса модели: достаточно применить модель к запросу и проверить, совпадает ли результат с ответом. Следующие два свойства и делают систему нетривиальной.

• Файл доказательства не раскрывает ничего, кроме самого утверждения (нулевое разглашение). Проверяющая сторона не узнаёт ничего о весах, промежуточных значениях вычислений или о том, какие эксперты работали на каждом слое. Архитектура модели (за исключением весов) не скрывается.
• Файл доказательства мал и быстро проверяется (краткость). Проверяемое вычисление — это запуск модели с 400 млрд параметров (около 232 ГБ для квантованной версии) на графическом процессоре H100, тогда как проверяющая сторона получает файл доказательства размером около 19 МБ, проверка которого занимает несколько секунд на центральном процессоре с 24 ядрами. Аудитор или пользователь, располагающий гораздо менее мощным оборудованием, чем поставщик, может проверять файлы доказательств без доступа к сложной инфраструктуре.

Оценка производительности

Мы измерили производительность реализации протокола на модели Llama 4 Maverick (смеси экспертов с 400 млрд параметров, из которых на каждый токен используется около 17 млрд), используя общедоступные 4-битные веса. Каждый запрос проверяющей стороны — это окно из 1 024 токенов, а каждое доказательство проверяет один токен. Доказывающая сторона работает на сервере с одним H100 и 24 ядрами ЦП, а проверяющая — на центральном процессоре.

• Создание доказательств. Доказывающая сторона работает на сервере с одним H100 и 24 ядрами ЦП. Автономный этап выполняется один раз для каждой модели и занимает около 39 минут. (По техническим причинам, описанным в техническом отчёте, полученная фиксация действительна примерно для 16 млн запросов, после чего поставщику нужно зафиксировать веса заново.) Этап обработки запросов для пакета из 24 запросов занимает у доказывающей стороны около 223 секунд, что соответствует 110 токенам в секунду; размер каждого доказательства — 18,78 МБ.
• Проверка. Проверяющая сторона работает на центральном процессоре клиента. Ей не нужен графический процессор, и у неё есть доступ только к фиксации весов. Клиент загружает фиксацию общим размером около 6,5 МБ, а затем получает по одному доказательству на каждый запрос. Проверка одного доказательства занимает 17 секунд на 24 потоках (и 21 секунду на одном потоке), включая проверки автономного этапа.

Сравнение с обычным инференсом: мы запустили vLLM — широко используемый движок инференса — с FP8-версией той же модели на восьми графических процессорах H100 и выяснили, что в расчёте на один графический процессор создание доказательств для пакета из 24 запросов занимает примерно в 72 раза больше времени, чем обработка тех же 24 запросов vLLM за один раз (в разных запусках — от 66 до 77 раз). При максимальной нагрузке, которую мы тестировали для vLLM, разница составляет около 94 раз.

Как устроена система. В основе FlashProve лежит zkSNARK того же типа, что используется в одноранговых системах (например, сетях второго уровня, таких как Starknet или Mantle, для блокчейнов вроде Ethereum). Наш zkSNARK построен по хорошо зарекомендовавшей себя схеме: лежащий в его основе информационно-теоретический объект, называемый интерактивным оракульным доказательством (IOP), преобразуетсяв криптографическое доказательство с помощью хеш-функций (при этом система обеспечивает даже постквантовую безопасность). Наш IOP собран из передовых компонентов с использованием таких инструментов, как тесты близости кода с линейными ограничениями и аргументы поиска, основанные на методах теории кодирования и теории сложности вычислений. Объединить эти компоненты в специализированный IOP для инференса — непростая задача; подробнее о конструкции рассказано в техническом отчёте.

Разработка системы

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

• Объём работы доказывающей стороны пропорционален количеству экспертов, которые действительно участвовали в вычислении. В модели MoE для обработки одного токена используются около 17 млрд из 400 млрд параметров, поэтому объём работы доказывающей стороны для каждого токена пропорционален этим примерно 17 млрд параметров, а не всем параметрам модели (при этом доказательство по-прежнему скрывает, какие именно эксперты были выбраны).
• Запросы объединяются в пакеты, и доказательства для них создаются постфактум. Доказывающая сторона за один параллельный проход считывает уже готовый текст (как при предварительной обработке), а фиксацию весов раскрывает один раз на пакет, а не для каждого запроса.
• Система спроектирована для работы на одном графическом процессоре. Веса модели на каждом слое разбиваются на сегменты, и доказательство строится по одному сегменту слоёв за раз. Веса хранятся в обычной памяти и загружаются по мере необходимости, поэтому достаточно одного графического процессора с 80 ГБ памяти и около 290 ГБ оперативной памяти хост-системы.

Постфактум или в процессе

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

Надёжность благодаря формальной верификации

Криптографический код печально известен своей хрупкостью и склонностью к ошибкам. Как пользователи могут доверять коду, который мы публикуем сегодня?

Ответ — формальная верификация: мы используем систему автоматизированного доказательства теорем Lean, чтобы задать протокол и требуемые свойства безопасности. Мы доказываем эти свойства в форме, которую можно проверить машинным способом и корректность которой гарантирована (за исключением ошибок компилятора). Мы проверяем три свойства верхнего уровня:

1. Полнота: если утверждение верно, проверяющий принимает полученное доказательство.
2. Надёжность: проверяющий отклоняет любое поддельное доказательство (за исключением случаев с пренебрежимо малой вероятностью).
3. Нулевое разглашение: доказательство не раскрывает никакой информации о весах модели сверх той, которую проверяющий может вывести из самого ответа.4

Эти свойства формулируются в так называемой модели случайного оракула — информационно-теоретическом подходе к анализу криптографических протоколов, использующих хеш-функции.

Формальная верификация оставляет два важных пробела в доверии. Во-первых, формальные утверждения необходимо проверять, чтобы убедиться, что они соответствуют своему замыслу. Это нужно делать вручную (хотя такая проверка несравненно проще проверки доказательств); для этого мы предоставляем интерактивный визуализатор.

Во-вторых, необходимо проверить исполняемый код, чтобы убедиться, что он соответствует формально определённому протоколу, для которого доказаны свойства безопасности. Оптимальный способ такой проверки зависит от свойства: надёжность зависит исключительно от проверяющего, нулевое разглашение — исключительно от доказывающего, а полнота — от их взаимодействия.

• Для обеспечения надёжности достаточно корректности кода проверяющего (вся ценность «доказательств» в том, что доказывающему можно полностью не доверять, если вы доверяете проверяющему). Мы предоставляем исполняемый верификатор на Lean наряду с верификатором на C++. Верификатор на Lean работает медленнее, но Lean доказывает, что он принимает только то, что принимает верификатор в нашей теореме о надёжности. Тем не менее для повседневного использования следует выбрать верификатор на C++: он не имеет формальных гарантий, но во всех наших тестах согласуется с верификатором на Lean.
• Для обеспечения полноты модель угроз не предполагает атак со стороны злоумышленников (доказывающий и проверяющий действуют честно). Поэтому верификатор на Lean позволяет нам укрепить уверенность с помощью стандартного тестирования ПО: честный доказывающий создаёт принимаемые доказательства. Для этого нужно запустить доказывающий на верном утверждении, а затем проверить полученное доказательство с помощью верификатора на Lean.
• Для обеспечения нулевого разглашения достаточно корректности доказывающего. Однако, в отличие от верификатора, доказывающий выполняет ресурсоёмкую процедуру, и запускать доказывающий на Lean было бы непрактично. Здесь мы не предоставляем никаких вспомогательных средств: мы рассчитываем, что любой доказывающий, стремящийся скрыть веса обслуживаемой им модели, располагает достаточными ресурсами для тщательной проверки безопасности с помощью автономных агентов и/или специалистов, чтобы подтвердить эквивалентность доказывающему на Lean.

Предыдущие работы

Доказуемый инференс — цель целого направления исследований, которое неформально называют «zkML». В ранних работах, например в SafetyNets (2017), проверялась свёрточная нейронная сеть MNIST с двумя свёрточными слоями и небольшая полносвязная модель распознавания речи; в работе zkCNN (2021) проверка VGG-16 (15 млн параметров) занимала 88,3 с на одно доказательство, а Канг и соавторы (2022) доказали работу MobileNet v2 на изображениях ImageNet полного разрешения.

Затем появились доказательства для трансформеров: на проверку одного токена в GPT-2 от ZKML с 117 млн параметров уходило около 159 с (≈0,006 токена/с), а для GPT-2 XL от Modulus Labs с 1,5 млрд параметров требовалось более 90 часов. Производительность постепенно росла: в работе zkLLM (2024) доказательство для LLaMA-2–13B на входе длиной 2 048 токенов строилось примерно за 15 минут на GPU — это ≈0,001 токена/с на каждый новый токен, или около 2,5 токена/с в пакете. В 2025 году zkGPT сократил время для GPT-2 до 21,8 с (≈0,05 токена/с), zkPyTorch доказал работу Llama-3 8B примерно за 150 с на токен на одном ядре CPU (≈0,007 токена/с), а ZKTorch доказал работу GPT-J (6B) примерно за 20 минут (≈0,001 токена/с). VerInf доказал работу Llama 4 Maverick — той же MoE-модели с 400 млрд параметров, что и в нашей работе, — со скоростью ≈0,02 токена/с. DeepProve, современный лидер среди прошедших рецензирование решений, сертифицирует всю сгенерированную последовательность за один прямой проход. Он обеспечивает скорость около 2,9 токена/с для GPT-2 и 1,4 токена/с для Gemma 3 на одной машине и 31 токена/с при распределённых вычислениях.

В последнее время коммерческие разработки также демонстрируют впечатляющие результаты: Attestable доказывает работу Gemma 4 31B со скоростью 53–77 токенов/с на одном H100; на момент написания статьи Attestable ещё не выпустила соответствующую библиотеку с открытым исходным кодом.

Эти показатели свидетельствуют о стремительном прогрессе в области доказуемого инференса за последние годы. Они должны изменить наши исходные представления о том, что можно доказать с нулевым разглашением.

• В 2024 году zkLLM доказал работу модели с 13 млрд параметров со скоростью около 2,5 токена/с на одном A100. Единственная известная нам более ранняя работа с доказательством для Llama 4 Maverick — VerInf — сообщает о 14,3 часа на 1 000 токенов на DGX Spark; размер доказательства составил 93,6 ГБ, а его проверка заняла почти сутки.
• FlashProve доказывает работу той же модели со скоростью 110 токенов/с на одном H100; размер доказательств составляет 19 МБ, а их проверка занимает несколько секунд. Attestable независимо сообщает о скорости 53–77 токенов/с для плотной модели с 31 млрд параметров.

Мы полагаем, что этот прогресс можно распространить на другие модели и архитектуры, получив гибкий и мощный инструмент, накладные расходы которого по сравнению с нативными вычислениями составят примерно два порядка величины (по нашим замерам — от 70 до 95 раз), что намного меньше прежних ожиданий.

Ограничения

Этот выпуск представляет собой исследовательский прототип со следующими техническими ограничениями:

• Для быстрого исполняемого кода нет формальных гарантий. Мы предоставляем реализацию протокола на Lean (включая исполняемый «медленный» верификатор на Lean), а также доказанные на Lean свойства безопасности. Статья и быстрый исполняемый код основаны на протоколе на Lean, но мы не гарантируем, что все три версии (Lean, статья и код) согласуются друг с другом.
• Доказательство относится к целочисленной модели с жадным декодированием. Мы доказываем точную целочисленную версию опубликованных весов; доказательство утверждает, что каждый проверенный токен является выбором этой модели при жадном декодировании. Ответ, полученный в реализации с плавающей точкой или при декодировании с выборкой, может в какой-то позиции отличаться и перестать точно соответствовать доказанному вычислению. Обычно ожидается, и эмпирические тесты подтверждают, что целочисленная версия в целом отличается от настоящего инференса с плавающей точкой лишь с небольшой частотой ошибок (даже с учётом недетерминированности вычислений с плавающей точкой), однако это не относится к промптам, специально созданным для атаки.
• Сокрытие архитектуры. Наша система предполагает, что обслуживаемая модель использует архитектуру «смесь экспертов» (MoE), в которой блок прямого распространения каждого слоя трансформера заменён несколькими экспертными подсетями и маршрутизатором, активирующим для каждого токена лишь небольшую подгруппу экспертов; наша система использует структуру MoE для повышения эффективности. Широко применяются и другие архитектуры, например плотные модели, описание которых может содержать интеллектуальную собственность, которую поставщик модели предпочёл бы сохранить в тайне. Можно представить и систему, которая дополнительно скрывает архитектуру модели: доказывающий с помощью скрывающего коммитмента фиксирует и веса, и архитектуру (то есть «исполняемый код» для инференса), а утверждение проверяющего касается проверки выполнения этого зафиксированного кода над зафиксированной моделью.
• Атаки по побочным каналам. Текущая гарантия протокола состоит в том, что само доказательство ничего не раскрывает о весах зафиксированной модели. Однако «атаки по побочным каналам», например измерение времени, необходимого для создания доказательства, потенциально могут раскрыть информацию о весах. В рамках этого выпуска мы не рассматриваем такие атаки.
• Более длинные контексты. Сейчас система доказывает инференс для контекстов длиной до 1 024 токенов. Это довольно мало по сравнению с контекстами, накапливаемыми в чатах. В идеале длину контекста можно было бы увеличить до размера контекстного окна передовых моделей, которое обычно составляет от сотен тысяч до миллионов токенов.

Сноски