В MIT разработали первый в мире тензорный язык программирования — он может сам оптимизировать программы

Ученые из Массачусетского технологического института (MIT) совместно с Калифорнийским университетом разработали прототип первого в мире тензорного языка программирования с формальной верификацией оптимизаций. Он получил название ATL, (сокращенно от A Tensor Language) и призван сделать вычисления не только высокоскоростными, но и более надежными. 

Зачем нужен новый язык программирования 

По словам специалистов, высокопроизводительные вычисление необходимы для все большего числа задач, таких как обработка изображений или различные приложения глубокого обучения в нейронных сетях. То есть везде, где нужно обрабатывать огромные массивы данных, причем быстро. Есть мнение, что при выполнении вышеописанных операций неизбежен компромисс между скоростью и надежностью: если в приоритете скорость, то, скорее всего, пострадает надежность, и наоборот. 

Однако теперь это утверждение ставит под сомнение группа ученых из MIT. По словам аспирантки лаборатории компьютерных наук и искусственного интеллекта Аманды Лю, благодаря новому языку программирования, который был создан специально для высокопроизводительных вычислений, не нужно выбирать между скоростью и надежностью.

Язык получил название A Tensor Language или сокращенно ATL. Как пояснила Аманда Лю, он ориентирован на получение либо одного числа, либо тензора. Тензоры в свою очередь — это обобщение векторов и матриц. Если векторы — это одномерные объекты (часто представляемые отдельными стрелками), а матрицы — это n-мерные массивы, которые могут иметь форму, например, массива 3х3х3 или еще более высокой (или низкой) размерности. 

Возможности и особенности языка 

По словам исследователей, главное преимущество ATL заключается в том, что язык может модифицировать или переписывать программы в оптимальную форму, чтобы ускорить работу. 

Предположим, что изображение представлено массивом чисел 100×100, каждое из которых соответствует пикселю. Задача: получить среднее значение для этих чисел. Это можно сделать с помощью двухэтапного вычисления, то есть сначала определить среднее значение каждой строки, а потом получить среднее значение каждого столбца. В ATL есть соответствующий инструментарий, который способен преобразовать двухэтапный процесс в одноэтапный.

Ученые рассказали, что ATL основан на языке программирования Coq со встроенным помощником, который призван проверять эффективность алгоритма строгим математическим методам. 

Кроме того, у Coq есть еще одна особенность, благодаря которой он попал в поле зрения группы из Массачусетского технологического института: программы, написанные на нем или его модификации, всегда завершаются и не могут застрять в бесконечном цикле, в отличии, например, от программ на Java.

Программирование на Coq

Сейчас ATL — это первый и пока единственный тензорный язык с формально подтвержденными оптимизациями. Однако ученые предупреждает, что это пока всего лишь прототип, хотя и многообещающий, который был протестирован на ряде небольших программ. В дальнейших планах команды MIT — улучшить масштабируемость ATL, чтобы его можно было использовать для больших программ.

Другие новые языки программирования: Logica (от Google), Zig и Ć.