, стверджує, що розробляє прототип нової мови програмування.){kind=link}
A computação de alto desempenho é necessária para resolver cada vez mais tarefas – como processamento de imagens ou vários aplicativos de aprendizado profundo em redes neurais – em que você precisa processar grandes quantidades de dados e fazê-lo com rapidez suficiente, caso contrário, pode levar uma quantidade incrível de tempo. Tempo. Acredita-se que ao realizar tais operações, um compromisso entre velocidade e confiabilidade é inevitável. De acordo com esse pensamento, se a velocidade é uma prioridade, é provável que a confiabilidade sofra e vice-versa.
No entanto, um grupo de pesquisadores baseado principalmente no Instituto de Tecnologia de Massachusetts (MIT) está desafiando essa noção, argumentando que você pode realmente ter tudo. De acordo com Amanda Liu, estudante do segundo ano de pós-graduação do Laboratório de Ciência da Computação e Inteligência Artificial (CSAIL) do MIT, com uma nova linguagem de programação que eles escreveram especificamente para computação de alto desempenho, “velocidade e correção não precisam competir. Pelo contrário, eles podem andar juntos, lado a lado, nos programas que escrevemos." Liu e sua equipe falaram sobre o potencial de sua recém-criada A Tensor Language (ATL) no mês passado na conferência Principles of Programming Languages na Filadélfia.
"Tudo em nossa linguagem", diz Liu, "destina-se a obter um único número ou um tensor". Os tensores, por sua vez, são uma generalização de vetores e matrizes. Enquanto os vetores são objetos unidimensionais (geralmente representados por setas individuais) e as matrizes são matrizes de números bidimensionais familiares, os tensores são matrizes n-dimensionais que podem assumir a forma de uma matriz 3×3×3, por exemplo, ou mesmo dimensão mais alta (ou baixa).
A essência de um algoritmo ou programa de computador é iniciar um determinado cálculo. Mas pode haver muitas maneiras diferentes de escrever este programa - "uma variedade surpreendente de diferentes implementações de código", como Liu e seus coautores escrevem em seu artigo - algumas das quais são significativamente mais rápidas que outras. A principal razão por trás da ATL, ela explica, é a seguinte: “Dado que a computação de alto desempenho consome muitos recursos, você deseja modificar ou reescrever programas de uma forma ideal para acelerar as coisas. Muitas vezes você começa com o programa que é mais fácil de escrever, mas que pode não ser a maneira mais rápida de executá-lo, então você ainda precisa fazer mais ajustes."
A nova linguagem de comando é baseada na linguagem Coq existente, que inclui um auxiliar de prova. O assistente de prova, por sua vez, tem a capacidade de provar matematicamente suas afirmações com precisão. O Coq tem outra propriedade que o tornou atraente para o grupo do MIT: programas escritos nessa linguagem, ou uma adaptação dela, sempre terminam e não podem ser executados indefinidamente em loops infinitos.
Agora é a primeira e até agora a única linguagem tensorial com otimizações formalmente verificadas. A equipe do MIT adverte, no entanto, que o ATL ainda é apenas um protótipo - embora promissor - que foi testado em vários pequenos programas.
Leia também: