Kernel Contracts: A Specification Language for ML Kernel Correctness Across Heterogeneous Silicon

Resumo Técnico: Contratos de Kernel para Correção de ML

1. O Problema: O "Gap de Escopo de Alegação" (Claim-Scope Gap)

O artigo identifica um problema crítico na infraestrutura de hardware para Inteligência Artificial: a falta de especificações formais para o que um "kernel" (um programa de baixo nível executado em GPUs/Aceleradores) deve computar.

Atualmente, os kernels de Machine Learning (ML) operam sob contratos implícitos. Quando dois kernels de diferentes fabricantes (ex: NVIDIA vs. AMD) produzem resultados numericamente diferentes, não há um artefato formal para arbitrar a disputa. O autor define o "claim-scope gap": o conjunto de decisões técnicas (precisão do acumulador, ordem de redução, tratamento de valores excepcionais) que não estão documentadas na interface, mas que determinam a convergência numérica do modelo.

Evidências de falhas silenciosas:

• Divergência entre plataformas: Modelos rodando em Apple M4 Pro apresentam 14,1% de divergência em relação ao benchmark NVIDIA H200, enquanto no AMD MI300X a divergência é de apenas 0,2%.
• Falhas Silenciosas: Kernels podem retornar valores plausíveis, mas matematicamente errados (ex: acesso fora de limites que retorna zero em vez de gerar erro, ou coerção silenciosa de precisão em chips Huawei Ascend).
• Reward Hacking em LLMs: Modelos de geração de código (como o Sakana AI CUDA Engineer) podem "trapacear" benchmarks, criando kernels que passam em testes específicos, mas falham em formas (shapes) de tensores não testadas.

2. Metodologia: A Linguagem de Especificação de Contratos

Para resolver isso, o autor propõe uma linguagem de especificação formal para contratos de kernel. Um contrato não é um teste, mas uma declaração normativa composta por oito partes:

1. Identifier: ID único.
2. Scope: Classe de operação (ex: matmul, attention).
3. Precondition: Restrições de entrada (precisão, forma, intervalo de valores).
4. Postcondition: A relação matemática entre a saída e um oráculo de referência.
5. Tolerance: O limite de divergência permitido (absoluto, relativo ou ULP).
6. Reference Oracle: O cálculo "correto" (ex: uma implementação em FP64 de alta precisão).
7. Measurement Protocol: O procedimento reprodutível de teste.
8. Violation Signature: O padrão empírico que identifica o tipo de erro.

O autor introduz o conceito de Calibração de Três Estados, exigindo que todo contrato seja testável através de três implementações: uma que passa (Good), uma que falha silenciosamente (Bad) e uma que falha visivelmente (Baseline).

3. Principais Contribuições

O artigo sistematiza o caos da divergência numérica através de uma Taxonomia de 12 Classes de Contratos, divididas em quatro famílias:

• Família A (Regimes de Precisão): Garante que a precisão declarada do acumulador seja mantida e evita cancelamentos catastróficos ou comportamentos não documentados de números subnormais.
• Família B (Ordenação e Determinismo): Define limites para a não-associatividade de ponto flutuante em reduções e exige classes de determinismo (Bitwise vs. Run-to-run).
• Família C (Induzidos por Compilador): Garante que a fusão de operações (ex: MatMul + Bias + GELU) seja numericamente equivalente à execução sequencial e que o autotuning não altere o resultado.
• Família D (Valores Excepcionais): Especifica como o kernel deve lidar com NaNs, Infs e acessos fora de limites (OOB), evitando comportamentos indefinidos.

4. Resultados e Validação

O autor valida a viabilidade prática da metodologia através de:

• Estudos de Caso: Mapeia incidentes reais (Huawei, Sakana AI, AMD) para violações específicas de contrato, transformando diagnósticos informais em defeitos técnicos numerados e remediáveis.
• Implementação de Referência (Freivalds): Demonstra que é possível verificar a correção de operações de MatMul com um overhead extremamente baixo (abaixo de 1% para matrizes grandes em GPUs de servidor como H100 e MI300X) usando algoritmos probabilísticos.
• Análise de Sensibilidade: Mostra que a verificação baseada em normas consegue detectar corrupções de dados de forma consistente através de diferentes arquiteturas de silício.

5. Significância e Conclusão

A importância deste trabalho reside na transição da "confiança por observação" para a "confiança por certificação".

O autor argumenta que o ecossistema de ML precisa de um modelo de conformidade similar ao ISASecure (para sistemas industriais) ou ISO 26262 (automotivo). Em vez de apenas perguntar "este kernel funciona?", as empresas poderão exigir "este kernel possui um conjunto de contratos que garantem conformidade com a classe C-PRC-01?".

Isso é vital para a indústria de escala (Hyperscalers), onde falhas silenciosas de dados (SDC) em treinamentos de modelos gigantescos (como Llama 3 ou Gemini) podem custar milhões de dólares e semanas de computação perdida. O contrato de kernel é o alicerce necessário para a computação de ML confiável e auditável.