A Tensor Language (ATL) – Computação de Alto Desempenho
Matéria publicada em 7 de fevereiro de 2022 no: https://news.mit.edu
Com um protótipo de linguagem tensorial, “velocidade e correção não precisam competir, elas podem andar juntas, de mãos dadas”.
Uma nova linguagem de tensores desenvolvida no Instituto de Tecnologia de Massachusetts – MIT, com otimizações formalmente verificadas, pode trazer benefícios para computação de alto desempenho.
A computação de alto desempenho é necessária para um número cada vez maior de tarefas – como processamento de imagens ou vários aplicativos de aprendizado profundo em redes neurais – em que é preciso percorrer imensas pilhas de dados e fazê-lo com rapidez razoável.
Acredita-se amplamente que, na realização de operações desse tipo, há trocas inevitáveis entre velocidade e confiabilidade.
Se a velocidade for a principal prioridade, de acordo com essa visão, a confiabilidade provavelmente será prejudicada e vice-versa.
No entanto, uma equipe de pesquisadores, baseada principalmente no MIT, está questionando essa noção, alegando que se pode, de fato, ter as duas coisas, confiabilidade e velocidade.
Com a nova linguagem de programação, que foi escrita especificamente para computação de alto desempenho, diz Amanda Liu, estudante do segundo ano de doutorado no Laboratório de Ciência da Computação e Inteligência Artificial do MIT (CSAIL), “velocidade e correção não precisam competir, em vez disso, podem andar juntos, de mãos dadas, nos programas que escrevemos.”
Liu – juntamente com o pós-doutorando da Universidade da Califórnia em Berkeley Gilbert Louis Bernstein, o professor associado do MIT Adam Chlipala e o professor assistente do MIT Jonathan Ragan-Kelley – descreveram o potencial da criação recentemente desenvolvida, “A Tensor Language” (ATL), no mês passado em a conferência de Princípios de Linguagens de Programação na Filadélfia.
“Tudo em nossa linguagem”, diz Liu, “destina-se a produzir um único número ou um tensor”.
Os tensores, são generalizações de vetores e matrizes.
Os vetores são objetos unidimensionais e as matrizes são bidimensionais, os tensores são matrizes n -dimensionais, que podem assumir a forma de uma matriz 3 x 3 x 3, por exemplo, ou algo ainda maior.
O objetivo de um algoritmo ou programa de computador é iniciar uma computação específica, mas, podem haver muitas maneiras diferentes de escrever esse programa – “uma variedade desconcertante de diferentes realizações de código”, como Liu e seus coautores escreveram em seu artigo de conferência que será publicado em breve – algumas consideravelmente mais rápidas do que outras.
A principal razão por trás da ATL é esta, ela explica:
“Dado que a computação de alto desempenho consome muitos recursos, você deseja modificar ou reescrever programas em uma forma ideal para acelerar as coisas. Muitas vezes começamos com um programa que é mais fácil de escrever, mas que pode não ser a maneira mais rápida de executá-lo, de modo que ainda são necessários ajustes adicionais.”
Como exemplo, suponha que uma imagem seja representada por uma matriz de números de 100 x 100, cada um correspondendo a um pixel, e você deseja obter um valor médio para esses números.
Isso pode ser feito em um cálculo de dois estágios, primeiro determinando a média de cada linha e em seguida, obtendo a média de cada coluna.
A ATL tem um kit de ferramentas associado – o que os cientistas da computação chamam de “framework” – que pode mostrar como esse processo de duas etapas pode ser convertido em um processo de uma etapa mais rápido.
“Podemos garantir que essa otimização esteja correta usando algo chamado assistente de prova (proof assistant)“, diz Liu.
Para isso, a nova linguagem da equipe se baseia em uma linguagem existente, Coq, que contém um assistente de prova.
O assistente de prova, por sua vez, tem a capacidade inerente de provar suas asserções de forma matematicamente rigorosa.
O Coq tinha outra característica intrínseca que o tornava atraente para o grupo baseado no MIT:
Programas escritos nele, ou adaptações dele, sempre terminam e não podem ser executados para sempre em loops infinitos, como pode acontecer com programas escritos em Java, por exemplo.
“Executamos um programa para obter uma única resposta – um número ou um tensor”, sustenta Liu.
“Um programa que nunca termina seria inútil para nós, mas o término é algo que obtemos de graça usando o Coq.”
O projeto ATL combina dois dos principais interesses de pesquisa de Ragan-Kelley e Chlipala.
Ragan-Kelley há muito se preocupa com a otimização de algoritmos no contexto da computação de alto desempenho.
Chlipala, por sua vez, concentrou-se mais na verificação formal, como na matemática, de otimizações algorítmicas.
Isso representa sua primeira colaboração.
Bernstein e Liu foram trazidos para a empresa no ano passado, e a ATL é o resultado.
Ela agora é a primeira e até agora a única linguagem tensorial com otimizações formalmente verificadas.
Liu adverte, no entanto, que o ATL ainda é apenas um protótipo – embora promissor – que foi testado em vários pequenos programas.
“Um dos nossos principais objetivos, olhando para o futuro, é melhorar a escalabilidade do ATL, para que possa ser usado para os programas maiores que vemos no mundo real”, diz Liu.
No passado, as otimizações desses programas geralmente eram feitas à mão, em uma base muito mais ad hoc, o que geralmente envolve tentativa e erro e, às vezes, bastante erro.
Com o ATL, acrescenta Liu, “as pessoas poderão seguir uma abordagem muito mais baseada em princípios para reescrever esses programas e fazê-lo com maior facilidade e maior garantia de correção”.
Original escrito por Steve Nadis | MIT CSAIL em 7 de fevereiro de 2022 no Instituto de Tecnologia de Massachusetts.
