Bit-Exact AI Inference Verification Without Performance Tradeoffs

Resumo Técnico: Verificação de Inferência de IA Bit-Exata Sem Trocas de Desempenho

Definição do Problema
O artigo aborda o desafio de verificar computações de IA realizadas por "adversários ocultos" (covert adversaries) — entidades que cumprem a monitoração apenas quando a probabilidade de detecção é alta. Os métodos de verificação atuais enfrentam um obstáculo significativo: o aparente não-determinismo da aritmética de ponto flutuante em GPUs. Devido à soma não-associativa em reduções paralelas e aproximações específicas de hardware, os auditores são frequentemente forçados a aceitar correspondências de saída aproximadas. Essa ambiguidade cria "graus de liberdade não verificáveis" que adversários podem explorar para esteganografia, modificações de software não relatadas ou computação oculta (por exemplo, elementos de lote ocultos). Embora as provas de conhecimento zero (ZKP) ofereçam um caminho a seguir, elas tipicamente exigem um determinismo estrito como um pré-requisito, o que historicamente exigiu flags de desempenho degradante ou bibliotecas de kernels customizados.

Metodologia
Os autores investigam as causas raízes da variância de saída em motores de inferência modernos (vLLM, HuggingFace Transformers) executando em GPUs NVIDIA (L40, L40S, A100, H100) sem habilitar flags de determinismo que prejudiquem o desempenho. A abordagem deles envolve:

1. Análise de Causa Raiz: Distinguir entre não-determinismo real (causado por funções atômicas como atomicAdd, onde o escalonamento de warps varia) e não-invariância (determinística, mas com árvores de redução variáveis devido ao software stack, tamanho de lote ou topologia de hardware).
2. Testes Empíricos: Executar inferência através de vários SKUs de hardware, versões de software, tamanhos de lote e formatos de quantização (BF16, FP8, INT8, INT4) para medir distâncias L2 de vetores de sinal (log-probabilidades, estados ocultos).
3. Emulação Apenas de Software: Desenvolver um emulador C/Python que roda inteiramente na CPU para prever a saída exata nível de bit da inferência de LLM acelerada por GPU. Este emulador modela:
   • Aritmética de Tensor Core: Replicando as janelas específicas de alinhamento de Ponto Fixo, truncamento e lógica de acumulação dos Tensor Cores (ex: a janela de 26 bits do A100) e instruções MMA.
   • Unidades de Função Especial (SFUs): Armazenando em cache as saídas exatas de hardware para funções transcendentais (exponencial, raiz quadrada recíproca), que divergem do IEEE 754, mas são determinísticas.
   • Reduções Específicas de Kernel: Espelhando as árvias de redução exatas, limites de tiles e ordens de acumulação ditadas por configurações específicas de kernel (ex: lógica de despacho de CUTLASS, FlashAttention-2, cuBLAS).
   • Limites de Dados: Forçando limites precisos de quantização BF16 entre estágios de pipeline para corresponder ao comportamento do hardware.

Principais Resultados

• Determinismo sem Flags: O estudo demonstra que motores de inferência modernos produzem saídas bit-idênticas quando o software stack, o SKU de hardware e as formas de entrada (incluindo o tamanho do lote) são fixos. O aparente não-determinismo é, em grande parte, uma função de mudanças nas ordens de redução baseadas nesses parâmetros, não de ruído aleatório.
• Fonte de Variância: A única fonte genuína de não-determinismo identificada foi o uso de atomicAdd em kernels específicos de desquantização INT (ex: o kernel exllama padrão para GPTQ no vLLM). Quando estes são evitados ou substituídos (ex: usando o kernel marlin), as saídas são determinísticas.
• Invariância de Tamanho de Lote: Os autores observaram "classes de equivalência" onde a mudança nos tamanhos de lote não alterava a saída do primeiro elemento do lote, particularmente em comprimentos de sequência mais longos (>4.000 tokens), onde a seleção de kernel se estabiliza.
• Precisão da Emulação: O emulador baseado apenas em software alcançou 0 diferenças de bits (acumuladores BF16 e FP32) contra a execução em GPU de referência para blocos FFN completos e blocos complexos de FlashAttention-2 em múltiplas arquiteturas de GPU. Isso confirma que erros de arredondamento acumulados podem ser precisamente previstos e auditados sem acesso ao hardware original.

Principais Contribuições

1. Reenquadramento de Erros de Arredondamento: O artigo argumenta que erros de arredondamento não devem ser vistos como uma restrição à verificabilidade, mas como uma "assinatura auditável" da configuração específica de software e hardware utilizada.
2. Protocolo de Verificação Bit-Exata: Estabelece que a recomputação bit-precisa é possível sem hardware idêntico, desde que o verificador conheça os fatores estáticos chave (SKU de hardware, versões de software, pesos do modelo, topologia de paralelismo) e o tamanho de lote dinâmico.
3. Emulação Apenas de Software: A demonstração de um emulador baseado em CPU capaz de modelar a aritmética específica de GPU (incluindo árvores de redução de Tensor Core e aproximações de SFU) para prever saídas de inferência de LLM bit a bit.
4. Preservação de Desempenho: O método de verificação não exige as trocas de desempenho associadas ao uso de flags de determinismo ou ao uso de kernels invariantes customizados; ele depende da natureza determinística existente dos motores de inferência padrão quando as condições são fixas.

Significância e Alegações
O artigo conclui que a "negação plausível" nas saídas de inferência de IA pode ser removida. Ao reportar o tamanho de lote concorrente e os detalhes de configuração junto com a saída, o provador pode colapsar a verificação em uma simples checagem de passar/falhar contra uma recomputação bit-exata. Os autores afirmam que a sensibilidade numérica das saídas serve como uma impressão digital de alta fidelidade do stack de hardware e software do provador. Isso permite a governança credível de adversários ocultos, garantindo que qualquer desvio da computação declarada (ex: esteganografia oculta ou modificações de software não autorizadas) resulte em uma incompatibilidade de bits detectável, desde que a configuração de verificação leve em conta os fatores de configuração específicos identificados. O trabalho sugere que o "não-determinismo" frequentemente citado como uma barreira à verificação de IA é, na verdade, um artefato determinístico e reproduzível do ambiente de computação.