Anthropic lança FlashProve para provas criptográficas de inferência de IA

Anthropic lançou o FlashProve em 2 de novembro de 2026: um protótipo de pesquisa de código aberto que usa provas criptográficas para demonstrar que uma resposta de um modelo de linguagem veio de pesos previamente comprometidos, sem revelá-los. A empresa informou uma geração de provas de 110 tokens por segundo para o Llama 4 Maverick, da Meta.

O trabalho aborda uma lacuna de verificação na IA hospedada. Uma resposta de alta qualidade não permite determinar qual modelo a produziu: um serviço de roteamento poderia substituí-lo por outro sistema, um avaliador poderia receber um modelo diferente daquele previsto para o teste ou um invasor poderia alterar o fluxo de tokens. Para os usuários, verificar o resultado executando novamente o modelo é impraticável quando os pesos são privados e os requisitos de hardware são substanciais.

Vinculação de respostas a pesos ocultos

O FlashProve usa um argumento sucinto de conhecimento de conhecimento zero, ou zkSNARK, em um projeto baseado exclusivamente em software, sem depender de hardware confiável. Durante uma fase offline, o provedor publica um compromisso curto que identifica um conjunto exato de pesos, mantendo-os em segredo. Para pares de solicitação e resposta já concluídos, o sistema produz uma prova de que os tokens de saída são o resultado do modelo comprometido. Qualquer pessoa que tenha o compromisso, a solicitação e a resposta pode verificar a prova sem ter acesso aos pesos.

As propriedades pretendidas são completude, solidez, conhecimento zero e concisão. Uma prova honesta deve ser aceita, enquanto certificar uma afirmação falsa deve exigir a quebra de pressupostos criptográficos amplamente considerados válidos. A verificação de uma prova não deve revelar os pesos nem os valores intermediários do cálculo. O projeto também oculta quais sub-redes da arquitetura de mistura de especialistas foram executadas para cada token, embora a arquitetura do próprio modelo permaneça visível.

A implementação aproveita a estrutura de mistura de especialistas do Maverick. O trabalho do provador é proporcional aos cerca de 17 bilhões de parâmetros ativos para cada token, em vez de aos 400 bilhões de parâmetros totais, mantendo ocultas as escolhas de especialistas. Os pesos segmentados são transmitidos da memória do sistema, permitindo que o provador funcione com uma única GPU de 80 GB e cerca de 290 GB de memória do sistema.

A Anthropic descreve possíveis usos em verificações de integridade para clientes, avaliações independentes, ferramentas regulatórias e aplicação de requisitos relativos a modelos aprovados. Os certificados de inferência poderiam atestar que as solicitações foram atendidas pelo modelo declarado, mas não comprovariam que o mesmo hardware não foi usado também para treinar outro modelo. Essa distinção limita o que tais certificados poderiam demonstrar sobre requisitos de conformidade baseados no uso da capacidade computacional.

Desempenho das provas e sobrecarga da inferência

A avaliação da Anthropic usou uma conversão de 4 bits do modelo disponível publicamente. Um servidor com uma H100 e 24 núcleos de CPU gerou provas para um lote de 24 solicitações em cerca de 223 segundos, produzindo uma prova de 18,78 MB para cada solicitação. A etapa offline de geração do compromisso levou cerca de 39 minutos.

Na etapa de verificação, o cliente baixa um compromisso de aproximadamente 6,5 MB e verifica as provas em uma CPU, sem GPU. A Anthropic mediu um tempo de verificação de 17 segundos com 24 threads e de 21 segundos com uma thread, incluindo as verificações da fase offline.

Essas medições distinguem um processo de verificação que usa apenas CPU de uma operação de geração de provas muito mais pesada. Na comparação da Anthropic com a inferência FP8 em oito H100 executando o vLLM, a geração de provas exigiu cerca de 72 vezes mais tempo por GPU para o mesmo lote e cerca de 94 vezes mais no nível de carga mais alto testado com o vLLM. Portanto, essa taxa de processamento tem um custo substancial em relação ao atendimento de solicitações pelo modelo sem provas.

Verificação formal e limites práticos

O repositório do FlashProve contém um provador, um verificador rápido em C++, um verificador mais lento em Lean, provas em Lean de afirmações matemáticas de alto nível e um visualizador interativo de teoremas, sob a licença Apache 2.0. A versão 0.16.0 é identificada como um artefato de pesquisa sem manutenção que não está aceitando contribuições.

O trabalho em Lean aborda completude, solidez e conhecimento zero no modelo de oráculo aleatório. Ainda é necessário revisar manualmente as afirmações formais para determinar se expressam as garantias pretendidas. O verificador em Lean está formalmente ligado ao teorema de solidez, mas o verificador em C++, destinado ao uso rotineiro, não oferece garantias formais; em vez disso, foi testado para confirmar que seus resultados coincidem com os do verificador em Lean.

A documentação sobre limitações conhecidas do projeto registra que sistemas de IA sob direção humana escreveram quase todo o software, as provas em Lean e a documentação, além de executarem os testes relatados. Não houve auditoria de segurança independente, e os testes de ocultação dos pesos e de provas adversariais continuam limitados.

As provas abrangem uma versão inteira exata dos pesos, sob decodificação gulosa. A inferência em ponto flutuante ou a decodificação por amostragem podem divergir do cálculo comprovado, e os testes genéricos de erro não abrangem solicitações concebidas de forma adversarial. O contexto é limitado a 1.024 tokens, enquanto ataques temporais e outros ataques por canais laterais estão fora do escopo da garantia. Em comparação com a geração de provas durante a inferência, a geração posterior introduz recálculo, garantias tardias e não determinismo.

Para que a inferência comprovável se torne uma verificação rotineira do tráfego em produção, o trabalho restante concentra-se nas lacunas reveladas por este lançamento: reduzir o custo da geração de provas, abranger modalidades de decodificação menos restritivas e contextos mais longos e conectar mais firmemente a implementação rápida ao protocolo formal.