Anthropic lanca o FlashProve: uma prova de que foi mesmo a sua LLM que gerou a resposta

Voce pagou por um modelo de primeira linha, mas um servico intermediario o trocou por outro mais barato no caminho. Detectar isso pelo texto da resposta e quase impossivel: a qualidade ainda pode ser perfeitamente aceitavel. A Anthropic publicou um prototipo de pesquisa que tenta fechar essa lacuna com criptografia.

O que foi criado exatamente

O sistema se chama FlashProve. A ideia e a seguinte: o provedor do modelo publica antecipadamente um compromisso, uma especie de impressao digital, dos seus pesos. Os pesos propriamente ditos continuam secretos. Depois, o provedor anexa a cada resposta uma prova zkSNARK curta, demonstrando que aqueles pesos comprometidos, diante daquele prompt, produziram exatamente aqueles tokens. O usuario verifica a prova em uma CPU comum, sem os pesos e sem hardware potente.

Imagine um selo reconhecido em cartorio em cada resposta do modelo. O selo nao pode ser falsificado, enquanto o tabeliao nao ve o conteudo do cofre onde estao os pesos.

Os numeros

O sistema foi testado no Llama 4 Maverick: 400 bilhoes de parametros, arquitetura mixture of experts e quantizacao de 4 bits. Uma unica H100 gera provas a aproximadamente 110 tokens por segundo. A prova ocupa cerca de 19 MB para uma solicitacao de 1.024 tokens. Isso consome de 70 a 95 vezes mais tempo de GPU do que executar o proprio modelo com vLLM. Segundo os autores, os sistemas abertos anteriores sao varias ordens de grandeza mais lentos.

O proprio Claude realizou parte do trabalho ao otimizar o sistema. No entanto, solucoes desse tipo sao dificeis de verificar em codigo complexo, por isso as principais garantias de seguranca foram formalizadas como proposicoes em Lean, uma linguagem de verificacao formal. Elas podem ser auditadas separadamente, e ha um visualizador para essa finalidade. Foram publicados cinco artefatos: um post, um relatorio tecnico, uma descricao do protocolo, o codigo —incluindo o prover, um verificador rapido em C++ e outro verificado em Lean— e as proprias provas. A licenca e Apache 2.0.

Por que isso e necessario

Os autores apontam quatro casos de uso:

• Ritmo de desenvolvimento da IA: um regulador verifica se o hardware esta realmente executando a inferencia do modelo declarado, em vez de treinar outra coisa em paralelo.
• Protecao contra substituicao: uma empresa confirma que os mesmos pesos estao sendo executados em seus servidores, mesmo que um servidor tenha sido comprometido ou que o modelo tente substituir a si proprio.
• Proveniencia do texto: torna-se possivel provar que o codigo foi revisado por um modelo potente especifico. Por exemplo, uma “Proof-of-Failure” poderia demonstrar que o modelo gastou pelo menos um milhao de tokens e nao encontrou bugs em um patch.
• Aprovacao de modelos: um regulador verifica se apenas modelos autorizados estao em execucao em producao.

Separadamente, a Anthropic menciona a meta do seu Frontier Safety Roadmap de criar um prototipo ate 30 de setembro de 2026. Essa meta foi cumprida por outro projeto relacionado: o trafego e assinado, enquanto a inferencia e recalculada em um servidor confiavel. O FlashProve avanca rumo ao mesmo objetivo por outro caminho.

Limitacoes

A solucao, por si so, nao esta pronta para producao. Uma sobrecarga de dezenas de vezes no tempo de GPU torna seu uso inviavel em cada solicitacao de um chat convencional. A arquitetura do modelo nao fica oculta; apenas os pesos ficam. A prova tambem nao demonstra que o hardware nao esta sendo usado simultaneamente para treinamento. Os proprios autores descrevem o trabalho como um resultado intermediario, e nao como um programa concluido.

Ha ainda uma alternativa: ambientes de execucao confiavel (TEEs) dependem do fabricante do chip, enquanto esta abordagem baseia a seguranca na dificuldade computacional de problemas criptograficos. Os autores consideram as duas abordagens complementares.

O que fazer na pratica

Se voce esta criando um roteador, um agregador de modelos ou um proxy de API, acompanhe essa area: dentro de alguns anos, os clientes poderao exigir uma comprovacao verificavel da autenticidade do modelo. Se voce realiza auditorias ou avaliacoes de seguranca de modelos, ja vale examinar como especificacoes em Lean ajudam a verificar alegacoes. Para os demais, a conclusao e mais simples: a inferencia verificavel saiu da teoria e chegou ao estagio de um prototipo funcional e de codigo aberto, que agora pode ser testado e aprimorado.