Anthropic detalha avanços em provable inference para modelos de linguagem de grande porte

O problema de partida é simples de enunciar. Quem consulta um modelo hoje não consegue checar que a resposta veio do modelo que o provedor diz estar servindo. Pode ter havido troca por um modelo mais barato num serviço de roteamento, ou adulteração do fluxo de tokens por um atacante. A Anthropic propõe resolver isso com um zkSNARK: o provedor se compromete com um modelo e anexa a cada resposta uma prova curta, verificável em segundos numa CPU, sem revelar os pesos.

O sistema se chama FlashProve. Num modelo de 400B de parâmetros com mistura de especialistas (Llama 4 Maverick, pesos quantizados em 4 bits, aritmética inteira no prefill), uma única GPU H100 gera provas a cerca de 110 tokens por segundo. Cada requisição de 1.024 tokens produz uma prova de ~19 MB. O custo é de 70 a 95 vezes o tempo de GPU do próprio modelo rodando no vLLM. Ou seja, é viável como protótipo, mas está longe de ser barato. A Anthropic afirma que os sistemas open-source anteriores são ordens de magnitude mais lentos. Os pesos ficam ocultos, mas esconder a arquitetura não é objetivo.

Como parte do código foi produzido com ajuda do Claude, a empresa publica enunciados de segurança auditáveis em Lean. Foram liberados cinco artefatos sob Apache 2.0: o post, um relatório técnico, uma especificação do protocolo, o código (prover, verificador rápido em C++ e verificador em Lean) e as provas em Lean com visualizador. A própria Anthropic diz que é progresso intermediário, não uma agenda de pesquisa concluída. O texto também lembra um limite: a prova mostra que o hardware serve inferência, mas não que ele não treina um modelo em paralelo.

O texto cita uma meta pública da Frontier Safety Roadmap: um protótipo de provable inference até 30 de setembro de 2026. Segundo a Anthropic, essa meta foi cumprida por um projeto separado, que assina o tráfego de inferência e recomputa a inferência em servidor confiável. O FlashProve persegue o mesmo objetivo por via criptográfica. A cobertura anterior do CEVIU não acompanhou essa meta, então não há comparação direta de versões.

Há ligação temática com a Lean. Em 23 de outubro de 2026, o CEVIU noticiou "LLMs ampliam a escala da verificação formal de software", e em 8 de setembro de 2026, "IA da Anthropic Gera Prova do Último Teorema de Fermat, Mas Desafia Adoção Ampla", ambas com provas validadas em Lean. Agora a mesma linguagem serve para auditar as garantias de segurança do FlashProve.

Para quem opera inferência em escala, a leitura é que verificar o modelo servido deixa de ser só confiança contratual e passa a ter um caminho técnico. O custo de 70 a 95 vezes em GPU ainda pesa, então o uso inicial tende a ser em casos pontuais, como avaliação independente ou auditoria. Para times de conformidade, o interessante é provar o modelo usado sem expor pesos.