FlashProve: що доказ інференсу залишає продукту

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

Це огляд публічних джерел від 5 листопада 2026 року. Я не збирав верифікатор, не запускав доказ і не орендував GPU. Репозиторій називає себе дослідницьким артефактом без супроводу та приймання внесків. Для виробничої залежності це істотна межа.

Яку модель фіксує зобов'язання

Публікація Anthropic описує доказ інференсу без розкриття ваг. Провайдер публікує зобов'язання до набору ваг, GPU створює доказ, CPU перевіряє його щодо запиту й очікуваного ідентифікатора.

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

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

Політика прийняття визначає твердження

Точний збіг стосується токенів визначеної цілочислової моделі. М'якша політика clipped gap приймає вартості токенів у встановлених межах і не доводить, що кожен токен був точним вибором моделі.

Точне прийняття та WITHIN LIMITS можуть завершуватися нульовим кодом. Якщо обгортка показує для кожного нуля "правильна відповідь моделі", вона викидає важливу частину результату. Проєкт не рекомендує готових меж. Поріг, що пропускає звичайні відповіді, ще треба перевірити на змістовних підмінах.

Очікуване зобов'язання + запит + покриття + політика
                         |
                  Перевірка доказу
                         |
              Результат за цією політикою

Факти, дозвіл людини та завершення завдання
потребують окремих свідчень.

Теорема й виконуваний код

Опис доведених властивостей стосується верифікатора Lean і визначень протоколу за вказаних припущень. C++-верифікатор та CUDA-prover написані за протоколом і тестуються щодо нього, але їхня формальна еквівалентність визначенням Lean не доведена.

Йдеться про квантовану цілочислову модель із фіксованою точкою. Зв'язок із вихідною моделлю з рухомою точкою є предметом вимірювань. Моя оцінка: специфікація, реалізація та сервісна обгортка потребують доказів для власних меж.

Що рахує показник швидкості

Документ продуктивності уточнює приблизно 110 токенів за секунду: сталий prefill, 1024 токени контексту, 24 запити в пакеті, один H100. Кожен доказ у цих вимірюваннях стверджує наступний токен. Запуск, фіксація зобов'язання та перевірка сервісною обгорткою не входять до цього числа.

Це не швидкість генерації 110 токенів відповіді за секунду. Повні збережені відповіді з м'якшою політикою описані окремим експериментом. Так само треба врахувати очікування пакета, CPU-перевірку й пам'ять хоста. Результати повідомляє проєкт; записи запусків у репозиторії відсутні. Я їх не відтворював.

Запис із чесними межами

Це навчальний JSON, не формат FlashProve і не виконаний тест:

{
  "expected_commitment": "reviewed-registry-entry",
  "request_fixture": "synthetic-question-07",
  "expected_output_positions": [0, 1, 2],
  "acceptance_policy": "exact-match",
  "proof_status": "not-run",
  "factual_answer_check": "separate-fixture-required",
  "external_action_permission": "none"
}

Запропонований тест змінює зобов'язання чи запит і вимагає відмови; скорочує покриття й вимагає явної невідповідності. Непідтримувана політика має залишатися непідтримуваною, а таймаут не стає прийняттям. Ці перевірки тут не виконані.

Відповідь після цього все одно слід перевірити окремим синтетичним прикладом із відомим підсумком. Дозвіл на повідомлення чи зміну акаунта також не виникає з доказу обчислення.

Apache 2.0 стосується коду проєкту, тоді як ваги й компоненти мають свої умови. Відкритість не скасовує витрат на GPU та інженерну роботу. У продукті варто показувати політику й покриття, а не перетворювати результат на загальну обіцянку правди чи виконаного завдання.