Axiom Math verifikon formalisht projektin Stacks: rreth 16 milionë rreshta kodi të kontrolluar nga agjentët e inteligjencës artificiale
Sipas raportimit të TechCrunch, kompania Axiom Math njoftoi të mërkurën se ka verifikuar formalisht Stacks Project, një nga korpuset më të mëdha të matematikës të shkruara ndonjëherë nga njerëzit. Njoftimi vjen në një kohë kur vetëm muajin e kaluar OpenAI publikoi 719 dorëshkrime që pretendonin zgjidhje për disa nga problemet më të vështira të fushës, dhe madje edhe kontrollet kompjuterike mund të rrëshqasin — ndaj Axiom po vë bast se matematika mund ta shmangë këtë fat duke qëndruar mbi themele të verifikuara.
Projekti Stacks u nis në vitin 2005 nga matematikani i Universitetit Columbia, Johan de Jong, si një referencë me burim të hapur, dhe matematikanët kanë kontribuar në të që atëherë, nga algjebra e nivelit universitar deri te idetë më të avancuara të algjebrës, gjeometrisë dhe teorisë së numrave. Kolegu i tij në Columbia, Peter Woit, ka thënë se nuk ka asgjë tjetër vërtet të krahasueshme me të, duke e krahasuar me librat e famshëm Bourbaki që rindërtuan matematikën nga themelet në shekullin e 20-të.
Flota e agjentëve të inteligjencës artificiale të kompanisë e përktheu bibliotekën prej rreth 7,654 faqesh në rreth 16 milionë rreshta kodi të kontrolluar kompjuterikisht në gjuhën Lean, ku një program asistent provash kontrollon çdo rresht; nëse prova kalon, matematikanët mund të jenë të sigurt se është logjikisht e shëndoshë. Sfida ishte ndërlidhja: çdo teoremë mbështetet te ato para saj, ndaj agjentët duhej të ruanin çdo lidhje në rreth 16 milionë rreshta. “Gjërat e mëdha dhe gjërat delikate në jetë thjesht nuk shkojnë bashkë”, tha për TechCrunch drejtoresha ekzekutive e Axiom, Carina Hong.
Hong, 25 vjeçe, e la programin e doktoraturës në matematikë në Stanford dhe e themeloi kompaninë në mars 2025; në mars Axiom mblodhi 200 milionë dollarë në një raund Series A të udhëhequr nga Menlo Ventures, ndërsa vlera e startup-it arrin 1.6 miliardë dollarë. Për projektin Stacks, ekipi u dha agjentëve një strukturë të lirshme dhe i la të punonin paralelisht, duke gjetur vetë detyra, ndërsa kompania trajnoi edhe modelet e veta posaçërisht për matematikën.
Sipas anëtarit të stafit teknik Ashvin Swaminathan, rezultati mbush një nga boshllëqet më të mëdha të matematikës së formalizuar, atë të gjeometrisë algjebrike: studiuesit që donin të kontrollonin punë të re me Lean kishin pak ku të mbështeteshin — tani e kanë. Axiom argumenton se çdo rezultat i verifikuar bëhet një bllok ndërtimi për provat e ardhshme, në frymën e asaj që matematikani i UCLA-së dhe fituesi i medaljes Fields, Terence Tao, e ka përmbledhur thjesht: sa më shumë prova të formalizuara të kesh, aq më shumë prova të formalizuara mund të bësh. Kompania synon që mbi këto themele të verifikuara të mbështetet edhe softueri i së ardhmes, që do të shkruhet gjithnjë e më shumë nga agjentët e AI.
