MIT er að þróa nýtt forritunarmál fyrir afkastamikil tölvur

Það þarf afkastamikil tölvumál til að leysa sífellt fleiri verkefni – eins og myndvinnslu eða ýmis djúpnámsforrit á tauganetum – þar sem þú þarft að vinna mikið magn af gögnum og gera það nógu hratt, annars getur það tekið ótrúlega mikið af gögnum. tíma. Almennt er talið að þegar slíkar aðgerðir eru framkvæmdar sé málamiðlun milli hraða og áreiðanleika óumflýjanleg. Samkvæmt þessari hugsun, ef hraði er í forgangi, þá er líklegt að áreiðanleiki verði fyrir skaða og öfugt.

Hins vegar er hópur vísindamanna með aðsetur fyrst og fremst við Massachusetts Institute of Technology (MIT) að ögra þessari hugmynd og halda því fram að þú getir í raun átt allt. Að sögn Amanda Liu, framhaldsnema á öðru ári við tölvunarfræði- og gervigreindarrannsóknarstofu MIT (CSAIL), með nýtt forritunarmál sem þeir skrifuðu sérstaklega fyrir afkastamikil tölvumál, „þurfa hraði og réttmæti ekki að keppa. Þvert á móti geta þau farið saman, hlið við hlið, í þeim þáttum sem við skrifum.“ Liu og teymi hennar ræddu um möguleika þeirra nýstofnaða A Tensor Language (ATL) í síðasta mánuði á Principles of Programming Languages ​​ráðstefnunni í Fíladelfíu.

"Allt á okkar tungumáli," segir Liu, "miðar að því að fá annað hvort eina tölu eða tensor." Tensorar eru aftur á móti alhæfing á vektorum og fylkjum. Þó að vektorar séu einvíðir hlutir (oft táknaðir með einstökum örvum) og fylki séu kunnugleg tvívídd talnafylki, eru tensorar n-víddar fylkingar sem geta verið í formi 3×3×3 fylkis, til dæmis, eða jafnvel hærri (eða lága) vídd.

Kjarninn í tölvualgrími eða forriti er að hefja ákveðinn útreikning. En það geta verið margar mismunandi leiðir til að skrifa þetta forrit -- "óvænt úrval af mismunandi kóðaútfærslum," eins og Liu og meðhöfundar hennar skrifa í blaðinu sínu -- sem sumar eru verulega hraðari en aðrar. Helstu rökin á bak við ATL, útskýrir hún, er þessi: „Í ljósi þess að afkastamikil tölvumál eru svo auðlindafrek, þá vilt þú geta breytt eða endurskrifað forrit á besta formi til að flýta fyrir. Oft byrjar þú á forritinu sem er auðveldast að skrifa, en það er kannski ekki fljótlegasta leiðin til að keyra það, svo þú þarft samt að gera frekari breytingar.“

Nýja stjórnmálið er byggt á núverandi Coq tungumáli, sem inniheldur sönnunarhjálp. Sönnunaraðstoðarmaðurinn hefur aftur á móti getu til að sanna fullyrðingar sínar stærðfræðilega nákvæmlega. Coq hefur annan eiginleika sem gerði það aðlaðandi fyrir MIT hópinn: forrit sem eru skrifuð á því tungumáli, eða aðlögun á því, hætta alltaf og geta ekki keyrt endalaust í óendanlegum lykkjum.

Nú er það fyrsta og hingað til eina tensortungumálið með formlega staðfesta hagræðingu. MIT teymið varar hins vegar við því að ATL sé enn aðeins frumgerð - að vísu efnileg - sem hefur verið prófuð á fjölda lítilla forrita.

Lestu líka:

• Nefndi skilyrði fyrir rétta Windows uppfærslu
• OpenAI kenndi gervigreind að breyta skipunum í forritakóða