, стверджує, що розробляє прототип нової мови програмування.){kind=link}
Det behövs högpresterande datoranvändning för att lösa allt fler uppgifter – som bildbehandling eller olika djupinlärningsapplikationer på neurala nätverk – där du behöver bearbeta enorma mängder data, och göra det tillräckligt snabbt, annars kan det ta otroligt mycket tid. Det anses allmänt att när man utför sådana operationer är en kompromiss mellan hastighet och tillförlitlighet oundviklig. Enligt detta tänkande, om hastighet är en prioritet, kommer tillförlitligheten sannolikt att bli lidande och vice versa.
Men en grupp forskare baserade främst vid Massachusetts Institute of Technology (MIT) utmanar denna uppfattning och hävdar att du faktiskt kan få allt. Enligt Amanda Liu, en andraårs doktorand vid MIT:s datavetenskap och artificiell intelligens Laboratory (CSAIL), med ett nytt programmeringsspråk som de skrev specifikt för högpresterande datorer, behöver inte hastighet och korrekthet konkurrera. Tvärtom kan de gå ihop, sida vid sida, i de program vi skriver." Liu och hennes team pratade om potentialen i deras nyskapade A Tensor Language (ATL) förra månaden vid Principles of Programming Languages-konferensen i Philadelphia.
"Allt på vårt språk", säger Liu, "syftar till att få antingen ett enda nummer eller en tensor." Tensorer är i sin tur en generalisering av vektorer och matriser. Medan vektorer är endimensionella objekt (ofta representerade av individuella pilar) och matriser är bekanta tvådimensionella arrayer av tal, är tensorer n-dimensionella arrayer som kan ta formen av en 3×3×3 array, till exempel, eller till och med högre (eller låg) dimension.
Kärnan i en datoralgoritm eller ett datorprogram är att initiera en viss beräkning. Men det kan finnas många olika sätt att skriva det här programmet - "en överraskande mängd olika kodimplementeringar", som Liu och hennes medförfattare skriver i sin tidning - av vilka några är betydligt snabbare än andra. Huvudmotivet bakom ATL, förklarar hon, är detta: "Med tanke på att högpresterande datoranvändning är så resurskrävande vill du kunna modifiera eller skriva om program i en optimal form för att påskynda saker och ting. Ofta börjar du med det program som är lättast att skriva, men det kanske inte är det snabbaste sättet att köra det, så du behöver fortfarande göra ytterligare justeringar."
Det nya kommandospråket är baserat på det befintliga Coq-språket, som inkluderar en korrekturhjälp. Korrekturassistenten har i sin tur förmågan att bevisa sina påståenden matematiskt exakt. Coq har en annan egenskap som gjorde det attraktivt för MIT-gruppen: program skrivna på det språket, eller en anpassning av det, avslutas alltid och kan inte köras i oändlighet i oändliga loopar.
Nu är det det första och hittills enda tensorspråket med formellt verifierade optimeringar. MIT-teamet varnar dock för att ATL fortfarande bara är en prototyp - om än en lovande sådan - som har testats på ett antal små program.
Läs också: