Он может иметь преимущества в высокопроизводительных вычислениях
Широко распространено мнение, что в высокопроизводительных вычислениях неизбежны компромиссы между скоростью и надёжностью. Однако команда исследователей утверждает, что можно получить всё. Подробностями делимся к старту флагманского курса по Data Science.
Высокопроизводительные вычисления необходимы во всё большем количестве задач, таких как обработка изображений или различные приложения глубокого обучения нейронных сетей, где нужно с трудом пробиваться сквозь огромные массивы данных и делать это с приемлемой скоростью.
По словам аспиранта второго года обучения Аманды Лью в написанном специально для высокопроизводительных вычислений новом языке программирования «скорость и корректность не должны конкурировать. Вместо этого в программе, которую мы пишем, они должны идти вместе, рука об руку».
Лью вместе с постдокторантом Гилбертом Льюисом Бронштейном, адъюнкт профессором Массачусетского технологического института Адамом Чипала и доцентом Массачусетского технологического института Джонатаном Раган-Келли на конференции Principles of Programming Languages в Филадельфии рассказали о потенциале своего недавнего творения — тензорного языка программирования (ATL).
«Всё в нашем языке, — рассказывает Лью, — нацелено возвращать какое-то число или тензор».
Тензоры, в свою очередь, — это обобщение векторов и матриц. Векторы — это одномерные объекты, обычно представленные одиночными стрелками, а матрицы известны как двумерные массивы чисел, тензоры — это n-мерные массивы, которые могут принимать, например, форму массива 3×3×3 или чего-то с большей или меньшей мерностью.
Весь смысл компьютерного алгоритма (или программы) — положить начало определённым вычислениям. Но программу можно написать многими способами.
«Разнообразие различных реализаций [алгоритмов] обескураживает, — пишут Лью и её соавтор в докладе для конференции, который вскоре будет опубликован. — Некоторые значительно быстрее других». Основная причина создания ATL, объясняют они, заключается в следующем:
«Учитывая, что высокопроизводительные вычисления столь ресурсоёмкие, нужно иметь возможность изменять или переписывать программы в оптимальную для ускорения работы форму. Часто начинается с программы, которую легче всего написать, но программа может оказаться не самой быстрой, так что необходимы дальнейшие корректировки».
Предположим, изображение представлено массивом чисел с размерами 100 на 100, каждое из которых связано с пикселем, и нужно получить среднее значение этих чисел. Сделать это можно вычислениями в два этапа, сначала определив среднее в строке матрицы, а затем — среднее значение каждого столбца.
У ATL есть инструменты, которые специалисты компьютерных наук называют «фреймворком», эти инструменты демонстрируют, как двухэтапный процесс может конвертироваться в одноэтапный.
«Корректность оптимизаций можно гарантировать, используя интерактивное доказательство теорем», — говорит об этом Лью. С этой целью новый язык строится поверх существующего языка Coq, содержащего инструмент интерактивного доказательства теорем, который доказывает утверждения математически строгим образом.
У Coq имеется ещё одна особенность, которая сделала его привлекательным для группы учёных: написанные на этом языке (или на его адаптации) программы не работают в бесконечных циклах, как это может произойти, например, с программами на Java. Они всегда завершаются.
«Мы запускаем программу, чтобы получить один ответ — число или тензор, — утверждает Лью. — Программа, которая никогда не завершается, была бы для нас бесполезна, но завершение программ — это то, что мы получаем, просто используя Coq».
ATL сочетает два основных научных интереса Реган-Келли и Чипала. Келли долго был обеспокоен оптимизацией алгоритмов в контексте высокопроизводительных вычислений.
Чипала тем временем сосредотачивался на формальной (на основе математики) верификации оптимизаций алгоритмов. Это их первое сотрудничество. В прошлом году Бернштейна и Лью привлекли к работе на предприятии, результатом которой стал ATL.
Сейчас это первый и единственный тензорный язык с формально верифицируемыми оптимизациями. Однако Лью предупреждает, что ATL пока остаётся прототипом — хотя и многообещающим, — протестированным на ряде небольших программ.
«Одна из наших главных целей на будущее — улучшить масштабируемость ATL, чтобы можно было использовать его для программ большего размера, которые мы видим в реальном мире», — говорит она.
В прошлом оптимизации таких программ обычно выполнялись вручную, только по необходимости, внепланово и без специальной подготовки, что приводило к частым испытаниям кода и иногда к удачным ошибкам.
«С ATL, — добавляет Лью, — люди смогут следовать более принципиальному подходу к переписыванию программ и делать это проще, получая больше гарантий корректности».
Погрузиться в изучение алгоритмов с самого начала или прокачать свои навыки вы сможете на наших курсах:
Выбрать другую востребованную профессию.
Краткий каталог профессий и курсов
Data Science и Machine Learning
Python, веб-разработка
Мобильная разработка
Java и C#
От основ — в глубину
А также
