Equivalence Checking of ML GPU Kernels
Este artigo apresenta o Volta, o primeiro verificador de equivalência sonoro e completo para kernels de GPU, que verifica formalmente a correção de computações de aprendizado de máquina otimizadas manualmente, por compiladores ou por LLMs.
Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo
Na vasta e invisível maquinaria da inteligência artificial moderna, o trabalho mais crítico não acontece na nuvem, mas em chips de computador especializados chamados GPUs. Esses chips são projetados para realizar milhões de cálculos minúsculos simultaneamente, uma necessidade para treinar os grandes modelos de linguagem que agora escrevem código, traduzem idiomas e geram arte. Para fazer com que esses modelos funcionem rápido o suficiente para serem úteis, engenheiros devem escrever instruções altamente especializadas, conhecidas como kernels, que dizem à GPU exatamente como mover dados e realizar cálculos matemáticos. Nos últimos anos, empresas começaram a usar a própria inteligência artificial para escrever esses kernels, esperando encontrar formas mais rápidas de realizar o trabalho do que os engenheiros humanos conseguem. No entanto, essa velocidade vem acompanhada de um risco: quando uma IA ou um compilador reescreve um trecho de código para ser mais rápido, pode acidentalmente introduzir erros sutis. Esses erros podem fazer com que o computador produza a resposta errada ou, pior, que trave silenciosamente de maneiras quase impossíveis de encontrar através de testes padrão. O desafio central é que esses chips executam milhares de threads de trabalho ao mesmo tempo e, se não coordenarem perfeitamente, podem pisar nos calos uns dos outros, criando uma condição de corrida onde o resultado final depende da ordem imprevisível em que as coisas acontecem.
Uma equipe de pesquisadores desenvolveu uma nova ferramenta chamada Volta para resolver esse problema. Em vez de adivinhar se uma nova versão, mais rápida, de um kernel está correta, a Volta atua como um verificador formal que prova matematicamente que as duas versões produzem resultados idênticos. Os pesquisadores construíram um sistema que pega as instruções de baixo nível de um kernel de referência — a versão original e confiável — e o kernel otimizado — a nova versão mais rápida — e os passa por um motor simbólico. Em vez de alimentar o código com números específicos e ver o que sai, o motor trata as entradas como símbolos abstratos. Ele rastreia cada caminho possível que o código poderia seguir, monitorando como os dados se movem através dos milhares de threads paralelos e como eles se sincronizam uns com os outros. Se o código tentar acessar a memória de uma forma que possa causar um conflito, ou se as threads ficarem presas esperando umas pelas outras para sempre, a ferramenta sinaliza o erro imediatamente. Se o código rodar sem problemas, a ferramenta traduz a saída final de ambos os kernels em expressões matemáticas complexas e verifica se essas expressões são fundamentalmente as mesmas, independentemente dos números específicos fornecidos a elas.
Os pesquisadores testaram a Volta em uma ampla variedade de tarefas de aprendizado de máquina do mundo real, incluindo multiplicações de matrizes, convoluções e os mecanismos de atenção que alimentam os grandes modelos de linguagem. Eles descobriram que a ferramenta podia verificar com sucesso kernels que foram otimizados manualmente, por compiladores e até mesmo por grandes modelos de linguagem. Em um caso, eles examinaram um kernel gerado por uma IA que havia sido otimizado através de treze rodadas de melhoria automatizada. A Volta confirmou que esse código gerado por IA era matematicamente equivalente ao original escrito por humanos, provando que as otimizações agressivas não haviam quebrado a lógica. A ferramenta também provou seu valor ao detectar erros que outros métodos perderam. Por exemplo, detectou condições de corrida de dados em um tutorial popular e amplamente citado de programação de GPU que fora usado por milhares de desenvolvedores durante anos. Esses erros estavam ocultos porque só apareciam sob condições de tempo muito específicas que os testes padrão raramente captam. A ferramenta também identificou um bug em um kernel gerado por IA onde o código tentava ler dados de um local de memória que não existia; embora o hardware atual tenha ignorado esse erro, os pesquisadores mostraram que o código era fundamentalmente inseguro e poderia falhar em máquinas futuras.
A força dessa abordagem reside em sua capacidade de lidar com a complexidade única da programação de GPU, onde milhares de threads devem coordenar suas ações. Ferramentas anteriores podiam verificar programas de thread única ou operações matemáticas de alto nível, mas tinham dificuldade em decompor o massivo paralelismo de uma GPU em partes gerenciáveis. A Volta supera isso assumindo que os kernels que ela analisa seguem um padrão específico e estruturado comum no aprendizado de máquina, onde o número de threads e o tamanho dos dados são conhecidos antecipadamente. Dentro desse framework, a ferramenta pode provar com certeza se uma condição de corrida existe caso as threads não estejam devidamente sincronizadas, e pode provar que dois programas diferentes são equivalentes se produzirem o mesmo resultado simbólico. Os pesquisadores demonstraram que sua ferramenta podia verificar essas propriedades em questão de segundos ou minutos, mesmo para kernels contendo centenas de milhares de instruções. Eles também provaram que a lógica matemática por trás de sua ferramenta é sólida, o que significa que, se a ferramenta diz que dois programas são iguais, eles são verdadeiramente iguais para todas as entradas possíveis.
Este trabalho representa um passo significativo para tornar o desenvolvimento da inteligência artificial mais seguro e confiável. À medida que as empresas dependem cada vez mais de sistemas automatizados para gerar o código que alimenta seus modelos, a necessidade de uma forma rigorosa de verificar esse código torna-se crítica. Os pesquisadores mostraram que é possível ir além do simples teste, que pode apenas verificar um número limitado de cenários, para um método que fornece uma garantia formal de correção. Ao verificar a equivalência de kernels otimizados, a Volta dá aos desenvolvedores a confiança para usar otimizações mais rápidas e agressivas sem medo de introduzir bugs silenciosos. A ferramenta está atualmente disponível para uso, e os pesquisadores disponibilizaram seu código e as provas por trás dele ao público, permitindo que outros construam sobre essa base. Embora a ferramenta ainda não cubra todos os tipos possíveis de código de GPU, ela lida com sucesso com a grande maioria dos kernels que impulsionam o aprendizado de máquina moderno, oferecendo um novo padrão de confiança para a geração automatizada de computação de alto desempenho.
Afogado em artigos na sua área?
Receba digests diários dos artigos mais recentes que correspondam às suas palavras-chave de pesquisa — com resumos técnicos, no seu idioma.