Anthropic publicou o FlashProve, um protótipo de investigação de código aberto dedicado à inferência provável. Este sistema, baseado num zkSNARK (uma prova criptográfica que permite demonstrar uma afirmação sem revelar os seus detalhes), permite provar que uma resposta provém de um modelo congelado, sem revelar nada sobre os seus pesos.
- A Anthropic publicou o FlashProve, um protótipo de código aberto que prova que uma resposta provém de um modelo comprometido.
- A prova não revela os pesos do modelo e funciona numa GPU H100 com o Llama 4 Maverick.
- O sistema custa cerca de 72 vezes mais tempo de GPU que o vLLM e está limitado a 1024 tokens e aos modelos MoE.
- Um verificador em Lean oferece garantias formais, enquanto o verificador em C++ serve para o uso diário sem essas garantias.
O problema visado diz respeito, em primeiro lugar, aos programadores. Atualmente, um utilizador que interroga um modelo não pode verificar qual modelo produziu realmente a resposta. Um serviço de encaminhamento poderia substituir o modelo solicitado por um modelo menos dispendioso, e um atacante poderia modificar o fluxo de tokens (as unidades de texto processadas pelo modelo). Julgar a qualidade de uma resposta não é suficiente, segundo a fonte, para detetar estas substituições.
Funcionamento e desempenho
O FlashProve opõe dois atores: o provador, ou seja, o fornecedor do modelo, e o verificador, ou seja, o utilizador. O sistema funciona em duas fases. Fora de linha, o fornecedor publica um compromisso, uma impressão digital curta que vincula um conjunto exato de pesos. Esta etapa demora cerca de 39 minutos e cobre aproximadamente 16 milhões de pedidos. Em linha, a GPU produz, para cada pedido, uma prova de que o modelo comprometido gerou efetivamente esses tokens.
A Anthropic afirma que este dispositivo oferece segurança pós-quântica e indica que pertence à mesma família das provas de validade utilizadas por redes de nível 2 como a Starknet. Segundo o guia de desempenho do repositório, a Anthropic mediu o sistema nos pesos públicos do Llama 4 Maverick, um modelo de 400B de parâmetros em mistura de peritos (MoE, arquitetura que ativa apenas uma parte dos parâmetros em cada token), com 4 bits de precisão, num único H100, uma GPU da Nvidia.
Para um lote de 24 pedidos, o débito anunciado é de 111,23 tokens por segundo. Um pedido isolado atinge apenas 17,41 tokens por segundo. O tamanho da prova é de 18,78 MB, e a sua verificação demora 17 segundos em 24 threads. Face ao vLLM, um sistema de inferência que executa o Maverick em FP8 em 8 H100, a prova custa cerca de 72 vezes mais tempo de GPU por lote, e cerca de 94 vezes ao débito máximo testado pelo vLLM.
Segurança e limitações
Sendo o código criptográfico frágil, a Anthropic diz ter formalizado o protocolo na linguagem Lean, para provar a sua completude, validade e divulgação zero de conhecimento. O README indica que um fornecedor fraudulento seria detetado, exceto com uma probabilidade de cerca de q/2^124 + 2^-101. O FlashProve inclui dois verificadores: um verificador rápido em C++, destinado a uso diário, mas que não beneficia de qualquer garantia formal, e um verificador mais lento em Lean, cuja aceitação se limita, segundo a Anthropic, ao que o teorema de validade admite.
O sistema também tem algumas restrições. Está limitado a 1024 tokens por pedido, à descodificação gananciosa e, por enquanto, aos modelos MoE. A Anthropic indica ainda que a sua equipa utilizou o Claude para otimizar o sistema. O código é publicado sob licença Apache 2.0 no repositório GitHub do FlashProve.
