Високопродуктивні обчислення необхідні для вирішення все більшої кількості завдань – таких як обробка зображень або різні програми глибокого навчання на нейронних мережах – де необхідно обробляти величезні масиви даних, причому робити це досить швидко, інакше це може зайняти неймовірну кількість часу. Широко поширена думка, що при виконанні подібних операцій неминучий компроміс між швидкістю та надійністю. Відповідно до цієї думки, якщо швидкість є пріоритетом, то надійність, швидше за все, постраждає і навпаки.
Однак група дослідників, що базується в основному в Массачусетському технологічному інституті (МІТ), ставить це поняття під сумнів, стверджуючи, що насправді можна мати все. За словами Аманди Лю, аспірантки другого року навчання в Лабораторії комп’ютерних наук та штучного інтелекту МІТ (CSAIL), з новою мовою програмування, яку вони написали спеціально для високопродуктивних обчислень, «швидкість і коректність не повинні конкурувати. Навпаки, вони можуть йти разом, пліч-о-пліч, у програмах, які ми пишемо». Лю разом із командою розповіла про потенціал нещодавно створеної ними мови «A Tensor Language» (ATL) минулого місяця на конференції «Принципи мов програмування» у Філадельфії.
«Все у нашій мові, – каже Лю, – спрямоване на отримання або одного числа, або тензора». Тензори, своєю чергою, є узагальненням векторів та матриць. Якщо вектори – це одновимірні об’єкти (часто представлені окремими стрілками), а матриці – знайомі двовимірні масиви чисел, то тензори – це n-вимірні масиви, які можуть мати форму масиву 3×3×3, наприклад, або ще вищої (або низької) розмірності.
Суть комп’ютерного алгоритму чи програми у тому, щоб ініціювати певне обчислення. Але може існувати безліч різних способів написання цієї програми – «дивовижна різноманітність різних реалізацій коду», як пишуть Лю та її співавтори у своїй статті – деякі з них значно швидше за інших. Основне обґрунтування ATL полягає в наступному, пояснює вона: «Враховуючи, що високопродуктивні обчислення настільки ресурсомісткі, ви хочете мати можливість модифікувати або переписувати програми в оптимальну форму, щоб прискорити роботу. Часто починають із програми, яку найлегше написати, але це може виявитися не найшвидшим способом її виконання, тож все одно потрібні подальші коригування».
Нова мова команди заснована на існуючій мові Coq, яка містить помічник доказу. Помічник доказу, своєю чергою, має здатність доводити свої твердження математично точно. Coq має ще одну властивість, яка зробила її привабливою для групи з Массачусетського технологічного інституту: програми, написані цією мовою або її адаптацією, завжди завершуються і не можуть працювати нескінченно в нескінченних циклах.
Зараз це перша і поки що єдина тензорна мова з формально перевіреними оптимізаціями. Команда МІТ, однак, попереджає, що ATL все ще є лише прототипом – хоч і багатообіцяючим – який був протестований на низці невеликих програм.
Читайте також: