, стверджує, що розробляє прототип нової мови програмування.){kind=link}
Компютерҳои баландсифат барои ҳалли вазифаҳои бештар ва бештар лозим аст, ба монанди коркарди тасвирҳо ё барномаҳои гуногуни омӯзиши амиқ дар шабакаҳои нейрон, ки дар он шумо бояд миқдори зиёди маълумотро коркард кунед ва онро ба қадри кофӣ зуд иҷро кунед, вагарна он метавонад миқдори бениҳоят зиёдро талаб кунад. вақт. Ба таври васеъ чунин мешуморанд, ки ҳангоми иҷрои ин гуна амалиёт созиш байни суръат ва эътимод ногузир аст. Ба ақидаи ин тафаккур, агар суръат авлавият дошта бошад, пас эътимоднокӣ азият мекашад ва баръакс.
Аммо, як гурӯҳи муҳаққиқон, ки асосан дар Донишкадаи Технологии Массачусетс (MIT) қарор доранд, ин мафҳумро зери шубҳа мегузоранд ва мегӯянд, ки шумо воқеан ҳама чизро дошта метавонед. Ба гуфтаи Аманда Лю, донишҷӯи соли дуввуми Лабораторияи илмҳои компютерӣ ва зеҳни сунъии MIT (CSAIL), бо забони нави барномасозӣ, ки онҳо махсус барои ҳисоббарории баландсифат навиштаанд, “суръат ва дурустӣ набояд рақобат кунанд. Баръакс, дар барномаҳое, ки мо менависем, онҳо метавонанд якҷоя, паҳлӯ ба паҳлӯ раванд." Лю ва дастаи ӯ дар бораи потенсиали забони навтаъсиси A Tensor Language (ATL) моҳи гузашта дар конфронси Принсипҳои забонҳои барномасозӣ дар Филаделфия сӯҳбат карданд.
«Ҳама чиз дар забони мо, - мегӯяд Лю, - барои гирифтани рақами ягона ё тензор нигаронида шудааст. Тензорҳо, дар навбати худ, умумисозии векторҳо ва матритсаҳо мебошанд. Дар ҳоле ки векторҳо объектҳои якченака мебошанд (аксар вақт бо тирҳои инфиродӣ нишон дода мешаванд) ва матритсаҳо массивҳои дученакаи ададҳо мебошанд, тензорҳо массивҳои n-ченака мебошанд, ки метавонанд шакли массиви 3×3×3, масалан, ё ҳатто андозаи баландтар (ё паст).
Моҳияти алгоритм ё барномаи компютерӣ аз оғози ҳисобкунии муайян иборат аст. Аммо роҳҳои гуногуни навиштани ин барнома метавонанд вуҷуд дошта бошанд - "як гуногунии ҳайратангези татбиқи рамзҳои гуногун", тавре ки Лю ва ҳаммуаллифони ӯ дар коғази худ менависанд - баъзеи онҳо нисбат ба дигарон хеле тезтаранд. Сабаби асосии пуштибонии ATL, вай мефаҳмонад, ин аст: "Бо назардошти он, ки ҳисоббарории баландсифат захираҳои зиёдро талаб мекунад, шумо мехоҳед барномаҳоро дар шакли оптималӣ тағир диҳед ё аз нав нависед, то корҳоро суръат бахшед. Аксар вақт шумо бо барномае оғоз мекунед, ки навиштан осонтарин аст, аммо ин метавонад роҳи зудтарини иҷро кардани он набошад, аз ин рӯ ба шумо лозим меояд, ки ислоҳоти минбаъда ворид кунед."
Забони нави фармон ба забони мавҷудаи Coq асос ёфтааст, ки ёрирасони исботкуниро дар бар мегирад. Ёрдамчии исбот, дар навбати худ, қобилияти исбот кардани изҳороти худро аз ҷиҳати математикӣ дақиқ дорад. Coq дорои хосияти дигаре аст, ки онро барои гурӯҳи MIT ҷолиб гардонд: барномаҳое, ки бо ин забон навишта шудаанд ё мутобиқсозии он, ҳамеша қатъ мешаванд ва наметавонанд ба таври номуайян дар ҳалқаҳои беохир кор кунанд.
Ҳоло он аввалин ва то ҳол ягона забони тензор бо оптимизатсияҳои расман тасдиқшуда мебошад. Аммо гурӯҳи MIT ҳушдор медиҳад, ки ATL то ҳол танҳо як прототип аст, гарчанде ки ояндадор аст, ки дар як қатор барномаҳои хурд санҷида шудааст.
Ҳамчунин хонед: