Hoje, quem envia um pedido a um modelo de IA alojado na nuvem tem de confiar na palavra do fornecedor: nada garante que o modelo escolhido foi realmente o que respondeu. A Anthropic quer mudar isso. A 2 de novembro de 2026, a empresa divulgou o FlashProve, um protótipo de investigação em código aberto que gera uma prova criptográfica de que determinada resposta saiu de um conjunto específico de pesos, previamente comprometido, sem os revelar.
O trabalho é assinado pelos investigadores Roy Rinberg e Alex Allain, da Anthropic, com colaboradores da EPFL, do MIT, da StarkWare e da Succinct, entre eles Alessandro Chiesa, da EPFL e da StarkWare. Segundo a empresa, foi o próprio Claude a desenvolver as melhorias em que o sistema assenta, combinando de forma nova técnicas já conhecidas na literatura criptográfica. Como este tipo de otimização feita por máquina é difícil de auditar, a equipa especificou o protocolo e as respetivas garantias de segurança em Lean, uma linguagem de prova formal, para que possam ser verificadas automaticamente.
Na base está um zkSNARK, ou argumento sucinto de conhecimento zero. Numa fase inicial, que demora cerca de 39 minutos, o fornecedor publica um compromisso: uma impressão digital curta que fixa um único conjunto de pesos. A cada pedido posterior, gera uma prova de que esse modelo, aplicado àquele texto de entrada, devolve exatamente aqueles tokens. A prova não revela nada sobre os pesos nem sobre os especialistas ativados dentro da rede, e é compacta, pelo que um utilizador com equipamento modesto a consegue confirmar depressa. A arquitetura do modelo, essa, fica visível.
Os números de referência foram obtidos com o Llama 4 Maverick, o modelo de mistura de especialistas da Meta com 400 mil milhões de parâmetros, numa versão pública de 4 bits. Num servidor com uma GPU H100 e 24 núcleos de CPU, o provador processou um lote de 24 pedidos de 1.024 tokens em cerca de 223 segundos, perto de 110 tokens por segundo, e cada prova ocupa uns 18,8 MB. Para verificar não é preciso GPU: a confirmação levou 17 segundos em 24 fios de execução. Face à execução dos mesmos pedidos no vLLM, gerar provas custa entre 70 e 95 vezes mais tempo de GPU, segundo a Anthropic.
A sobrecarga continua a ser grande, mas a comparação com sistemas anteriores mostra a rapidez do avanço. No levantamento de trabalhos prévios, a Anthropic cita o VerInf, que provou o mesmo Maverick a uns 0,02 tokens por segundo, precisou de 14,3 horas para mil tokens e produziu uma prova de 93,6 GB. A empresa refere ainda que a startup Attestable anuncia 53 a 77 tokens por segundo para um modelo Gemma denso de 31 mil milhões de parâmetros, embora sem ter publicado código aberto.
A Anthropic enquadra a ferramenta em problemas de confiança que crescem à medida que a IA se espalha. Um cliente que recorra a um serviço intermediário poderia confirmar que recebeu o modelo pelo qual pagou. Um operador poderia detetar um servidor de inferência comprometido, ou um modelo que se faz passar por outro para escapar à monitorização. Em teoria, um regulador poderia verificar se um fornecedor só serve modelos aprovados, ou se o hardware destinado à inferência não está a ser usado para treinar outro sistema. A publicação inclui o código, um verificador em C++ e outro, mais lento, escrito em Lean, as provas formais e um relatório técnico, tudo sob licença Apache 2.0.
As limitações são assumidas. As provas dizem respeito a uma versão do modelo em aritmética inteira e com descodificação gulosa, pelo que respostas amostradas ou em vírgula flutuante podem divergir. O contexto está limitado a 1.024 tokens, muito abaixo das conversas reais, e a prova é feita em lotes, depois do facto, e não em tempo real. O código rápido em C++ não tem garantia formal de corresponder à especificação em Lean, fugas por canais laterais como o tempo de execução ficam de fora e o compromisso tem de ser renovado ao fim de uns 16 milhões de pedidos. A Anthropic apresenta o trabalho como um progresso intermédio, e os valores de desempenho ainda não foram reproduzidos por terceiros.