Anthropic випускає FlashProve для криптографічного доведення інференсу ШІ

Anthropic випустила FlashProve 2 листопада 2026 року: це дослідницький прототип із відкритим кодом, який використовує криптографічні докази, щоб підтвердити, що відповідь мовної моделі отримано на основі зафіксованих ваг, не розкриваючи їх. Компанія повідомила, що для Meta’s Llama 4 Maverick генерує докази зі швидкістю 110 токенів за секунду.

Ця розробка допомагає усунути прогалину у верифікації ШІ, що працює на хостованих платформах. Висока якість відповіді не доводить, яка саме модель її згенерувала: служба маршрутизації може підставити іншу систему, оцінювач може отримати для тестування не ту модель, яку було заплановано, або зловмисник може змінити потік токенів. Користувачам недоцільно перевіряти результат, повторно запускаючи модель, якщо її ваги закриті, а вимоги до апаратного забезпечення значні.

Прив’язування відповідей до прихованих ваг

FlashProve використовує короткий аргумент знання з нульовим розголошенням, або zkSNARK, у програмній реалізації, яка не залежить від довіреного обладнання. Під час офлайн-етапу провайдер публікує короткий комітмент, що ідентифікує один точний набір ваг, зберігаючи їх у таємниці. Для вже сформованих пар «запит — відповідь» система створює доказ того, що вихідні токени є результатом роботи моделі, зафіксованої в комітменті. Будь-хто, хто має комітмент, запит і відповідь, може перевірити доказ, не маючи доступу до ваг.

Очікується, що система забезпечуватиме повноту, надійність, нульове розголошення та лаконічність. Чесно сформований доказ має бути прийнятий, тоді як підтвердження хибного твердження має вимагати порушення загальновизнаних криптографічних припущень. Перевірка доказу не має розкривати ні ваги, ні проміжні значення обчислень. Архітектура також приховує, які підмережі суміші експертів виконували обчислення для кожного токена, хоча сама архітектура моделі залишається видимою.

У реалізації використано структуру Maverick із сумішшю експертів. Обчислювальні витрати на створення доказу залежать від приблизно 17 мільярдів параметрів, активних для одного токена, а не від усіх 400 мільярдів, і водночас вибір експертів залишається прихованим. Сегментовані ваги потоково зчитуються з пам’яті хоста, тож для роботи системи достатньо одного графічного процесора з 80 GB пам’яті та приблизно 290 GB пам’яті хоста.

Anthropic описує можливі сфери застосування: перевірки доброчесності для клієнтів, незалежні оцінювання, інструменти регулювання та забезпечення вимог щодо використання схвалених моделей. Сертифікати інференсу можуть підтвердити, що запити обслуговувала заявлена модель, але не доведуть, що те саме обладнання водночас не використовувалося для навчання іншої моделі. Це обмежує те, що такі сертифікати можуть засвідчити щодо дотримання вимог, які залежать від способу використання обчислювальних ресурсів.

Продуктивність доведення та накладні витрати на інференс

Для оцінювання Anthropic використала загальнодоступну 4-бітну конвертацію моделі. Сервер з одним H100 і 24 ядрами процесора сформував докази для пакета з 24 запитів приблизно за 223 секунди; розмір доказу для кожного запиту становив 18.78 MB. Офлайн-етап створення комітменту тривав приблизно 39 хвилин.

На боці верифікації клієнт завантажує комітмент розміром приблизно 6.5 MB і перевіряє докази на процесорі без графічного процесора. За вимірюваннями Anthropic, верифікація тривала 17 секунд із 24 потоками та 21 секунду з одним потоком; ці показники включають перевірки офлайн-етапу.

Ці вимірювання показують різницю між перевіркою лише на процесорі та значно ресурсомісткішою операцією створення доказів. У порівнянні Anthropic з інференсом FP8 на восьми H100 під керуванням vLLM на створення доказів для того самого пакета потрібно було приблизно у 72 рази більше часу на один графічний процесор, а за найвищого навантаження vLLM, яке тестували, — приблизно у 94 рази більше. Отже, така пропускна здатність досягається ціною значних витрат порівняно з обслуговуванням моделі без доказів.

Формальна верифікація та практичні обмеження

У репозиторії FlashProve є засіб створення доказів, швидкий верифікатор на C++, повільніший верифікатор на Lean, доведення основних математичних тверджень у Lean та інтерактивний візуалізатор теорем; усі вони поширюються за ліцензією Apache 2.0. Версію 0.16.0 позначено як непідтримуваний дослідницький артефакт, внески до якого не приймаються.

Робота з Lean охоплює повноту, надійність і нульове розголошення в моделі випадкового оракула. Щоб установити, чи справді формальні твердження виражають передбачені гарантії, їх іще потрібно перевірити вручну. Верифікатор на Lean формально пов’язаний із теоремою надійності, однак верифікатор на C++, призначений для регулярного використання, не має формальних гарантій; натомість його протестували, порівнявши результати з верифікатором на Lean.

У документації про відомі обмеження проєкту зазначено, що системи ШІ під керівництвом людей написали майже все програмне забезпечення, доведення на Lean і документацію, а також виконали описані тести. Незалежного аудиту безпеки не проводили, а перевірки приховування ваг і стійкості до зловмисних доказів залишаються обмеженими.

Докази охоплюють точну цілочислову версію ваг за жадібного декодування. Інференс із рухомою комою або декодування зі семплюванням можуть відрізнятися від обчислень, які доводяться, а загальне тестування помилок не охоплює запити, спеціально розроблені для зловмисного впливу. Контекст обмежений 1,024 токенами, а атаки за сторонніми каналами, зокрема за часом виконання, не покриваються гарантіями. Створення доказів постфактум також потребує повторних обчислень, затримує надання гарантій і призводить до недетермінованості порівняно зі створенням доказів одночасно з інференсом.

Щоб доказовий інференс став звичайною перевіркою запитів, що обслуговуються, подальша робота зосередиться на прогалинах, виявлених у цьому релізі: зниженні вартості доведення, підтримці менш обмежувального декодування та довших контекстів, а також тіснішому зв’язку швидкої реалізації з формальним протоколом.