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 и разработку. Для продукта мой практический вывод прост: показывать пользователю политику и покрытие результата, не подменяя их обещанием истины или выполненной задачи.