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

В Массачусетском технологическом институте уверены, что «скорость и правильность не должны конкурировать друг с другом. Вместо этого они могут идти «рука об руку».

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

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

В качестве примера предположим, что изображение представлено массивом чисел 100×100, каждое из которых соответствует пикселю, и вы хотите получить среднее значение для этих чисел. Результат можно получить в двухэтапном вычислении, сначала определив среднее значение каждой строки, а затем получив среднее значение каждого столбца. У ATL есть соответствующий инструментарий — то, что программисты называют «структурой», — который может показать, как этот двухэтапный процесс можно преобразовать в более быстрый одноэтапный процесс.

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

У Coq есть еще одна неотъемлемая особенность, которая сделала его привлекательным для группы из Массачусетского технологического института: программы, написанные на нем, или его адаптации всегда завершаются и не могут вечно работать в бесконечных циклах (как это может случиться, например, с программами, написанными на Java). «Мы запускаем программу, чтобы получить единственный ответ — число или тензор. Программа, которая никогда не завершается, была бы для нас бесполезна, но завершение — это то, что мы получаем бесплатно, используя Coq», говорят в MIT.

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

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