Высокопроизводительные вычисления необходимы для постоянно растущего числа задач, таких как обработка изображений или различные приложения для глубокого обучения в нейронных сетях, где нужно обрабатывать огромные объемы данных и делать это достаточно быстро, иначе это может занять большое количество времени. Широко распространено мнение, что при выполнении операций такого рода неизбежен компромисс между скоростью и надежностью. Согласно этой точке зрения, если скорость является главным приоритетом, то, скорее всего, пострадает надежность, и наоборот.
Однако группа исследователей, базирующаяся в основном в Массачусетском технологическом институте, ставит это мнение под сомнение, утверждая, что на самом деле можно достичь и того и другого. С новым языком программирования, который они написали специально для высокопроизводительных вычислений, говорит Аманда Лю, аспирантка второго курса Лаборатории компьютерных наук и искусственного интеллекта Массачусетского технологического института (CSAIL), «скорость и правильность не должны конкурировать друг с другом. . Вместо этого они могут идти рука об руку в программах, которые мы пишем».
Лю — вместе с постдоком Калифорнийского университета в Беркли Гилбертом Луи Бернштейном, доцентом Массачусетского технологического института Адамом Члипалой и доцентом Массачусетского технологического института Джонатаном Рэган-Келли — описали потенциал своего недавно разработанного творения, « Тензорного языка » (ATL), в прошлом месяце в на конференции «Принципы языков программирования» в Филадельфии.
«Все в нашем языке, — говорит Лю, — направлено на создание либо одного числа, либо тензора». Тензоры, в свою очередь, являются обобщениями векторов и матриц. В то время как векторы — это одномерные объекты (часто представленные отдельными стрелками), а матрицы — это знакомые нам двумерные массивы чисел, тензоры — это n -мерные массивы , которые могут принимать форму массива 3x3x3.
Весь смысл компьютерного алгоритма или программы заключается в том, чтобы инициировать конкретное вычисление. Но может быть много разных способов написания этой программы — «ошеломляющее разнообразие различных реализаций кода», как написали Лю и ее соавторы в своем докладе на конференции, который скоро будет опубликован — некоторые значительно быстрее, чем другие. Она объясняет, что основная причина использования ATL заключается в следующем: «Учитывая, что высокопроизводительные вычисления настолько ресурсоемки, вы хотите иметь возможность модифицировать или переписывать программы в оптимальную форму, чтобы ускорить работу. Часто начинают с программы, которую легче всего написать, но это может быть не самый быстрый способ ее запуска, поэтому все еще необходимы дальнейшие корректировки».
В качестве примера предположим, что изображение представлено массивом чисел 100×100, каждое из которых соответствует пикселю, и вы хотите получить среднее значение для этих чисел. Это можно сделать в двухэтапном вычислении, сначала определив среднее значение каждой строки, а затем получив среднее значение каждого столбца. У ATL есть соответствующий инструментарий — то, что компьютерщики называют «структурой», — который может показать, как этот двухэтапный процесс можно преобразовать в более быстрый одноэтапный процесс.
«Мы можем гарантировать, что эта оптимизация верна, используя нечто, называемое помощником по проверке», — говорит Лю. С этой целью новый язык команды основывается на существующем языке Coq, который содержит помощника по проверке. Помощник по доказательству, в свою очередь, обладает способностью доказывать свои утверждения математически строгим образом.
У Coq была еще одна неотъемлемая особенность, которая делала его привлекательным для группы из Массачусетского технологического института: программы, написанные на нем, или его адаптации всегда завершаются и не могут вечно работать в бесконечных циклах (как это может случиться, например, с программами, написанными на Java). «Мы запускаем программу, чтобы получить единственный ответ — число или тензор», — утверждает Лю. «Программа, которая никогда не завершается, была бы для нас бесполезна, но завершение — это то, что мы получаем бесплатно, используя Coq».
Проект ATL объединяет два основных исследовательских интереса Рагана-Келли и Члипалы. Раган-Келли уже давно занимается оптимизацией алгоритмов в контексте высокопроизводительных вычислений. Тем временем Члипала больше сосредоточился на формальной (как и на математической) проверке алгоритмической оптимизации. Это их первая совместная работа. Бернстайн и Лю пришли на предприятие в прошлом году, и результатом стала ATL.
Теперь это первый и пока единственный тензорный язык с формально проверенными оптимизациями. Однако Лю предостерегает, что ATL все еще является лишь прототипом, хотя и многообещающим, который был протестирован на ряде небольших программ. «Заглядывая в будущее, одной из наших главных целей является улучшение масштабируемости ATL, чтобы ее можно было использовать для более крупных программ, которые мы видим в реальном мире», — говорит она.
В прошлом оптимизация этих программ, как правило, выполнялась вручную, на гораздо более специальной основе, которая часто включала пробы и ошибки, а иногда и большое количество ошибок. С помощью ATL, добавляет Лю, «люди смогут следовать гораздо более принципиальному подходу к переписыванию этих программ — и делать это с большей легкостью и с большей уверенностью в правильности».
Будьте в курсе в удобном формате, присоединяйтесь: TG-канал и ВК
Опубликуйте материал о вашем проекте, стартапе или технологии
hello@technovery.com