Matematica, ultimul bastion al gândirii abstracte umane, pare tot mai aproape de o revoluție tăcută, una declanșată nu de o teoremă spectaculoasă, ci de puterea tot mai mare a inteligenței artificiale. Modelele de limbaj de mari dimensiuni (LLM), precum cele din spatele ChatGPT, pătrund acum într-un teritoriu până recent considerat inaccesibil pentru computere, demonstrațiile matematice riguroase, anunță NewScientist.
Urmărește cele mai noi producții video TechRider.ro
- articolul continuă mai jos -
La începutul lunii iunie, circa 100 dintre cei mai importanți matematicieni ai lumii s-au reunit la Universitatea Cambridge într-o conferință dedicată formalizării matematicii – adică procesului prin care o demonstrație este transpusă într-un limbaj logic, lizibil de computer, capabil să verifice corectitudinea fiecărui pas. Dacă în urmă cu doar câțiva ani acest domeniu era o nișă ignorată de cercetarea „mare”, astăzi AI-ul îl transformă într-o miză majoră.
„Totul a explodat deodată. Ceea ce era cândva un colț obscur al matematicii devine dintr-o dată centrul atenției”, spune Jeremy Avigad, profesor la Carnegie Mellon University și coorganizator al conferinței. În prim-plan: modele capabile nu doar să asiste matematicienii, ci chiar să genereze demonstrații valide, uneori mai rapid și mai riguros decât oamenii.
AlphaProof, un AI care înțelege teoremele
Una dintre cele mai spectaculoase prezentări a fost susținută de echipa DeepMind, divizia de inteligență artificială a Google. Cercetătorii au vorbit despre AlphaProof, un model AI care anul trecut a obținut echivalentul unei medalii de argint la Olimpiada Internațională de Matematică (IMO), competiție rezervată liceenilor cu aptitudini excepționale. Deși unii matematicieni consideră acele probleme „simple”, performanța rămâne remarcabilă pentru un sistem autonom.
Dar AlphaProof nu se limitează la concursuri. La Cambridge, echipa a demonstrat cum sistemul poate contribui la formalizarea unei porțiuni din teorema numerelor prime, un pilon al teoriei numerelor. Deja tradusă într-un limbaj formal numit Lean, demonstrația a fost verificată complet automat de AlphaProof. Practic, AI-ul a confirmat corectitudinea unei demonstrații complexe, exact cum ar face-o o echipă de experți umani.
Trinity, de la scrisul de mână la cod formalizat
Un alt moment-cheie al conferinței a venit de la startup-ul american Morph Labs, care a prezentat Trinity – un instrument capabil să traducă automat demonstrațiile scrise de mână în cod Lean, verificabil matematic. Cercetătorii au folosit sistemul pentru a transpune o demonstrație legată de faimoasa și controversata conjectură ABC, încă nerezolvată în mod convingător.
„Este pentru prima dată când vedem un sistem care ia o lucrare întreagă, chiar dacă scurtă, și o traduce complet într-un limbaj formal”, spune Kevin Buzzard, matematician la Imperial College London. Procesul a fost asistat de oameni, dar rezultatul i-a uimit pe mulți: un cod valid, matematic corect, obținut în mare parte de o mașină.
O promisiune uriașă, dar nu fără critici
Christian Szegedy, de la Morph Labs, este convins că astfel de sisteme vor progresa rapid. „Odată ce eliminăm nevoia de intervenție umană constantă, va fi ca o reacție în lanț. Vom putea formaliza toată matematica”, afirmă el.
Optimismul e împărtășit și de Timothy Gowers, matematician britanic laureat cu medalia Fields. „În următorii 1 până la 5 ani, modul în care facem matematică se va schimba radical, poate la fel de mult ca în epoca în care au apărut e-mailul, LaTeX sau arXiv”, spune el.
Totuși, nu toată lumea este convinsă. Rodrigo Ochigame, de la Universitatea Leiden, avertizează că Morph Labs nu a publicat nicio lucrare științifică despre metodele folosite, nici nu a oferit detalii despre câtă putere de calcul a fost necesară. „Este greu să evaluăm rezultatul când vedem doar un exemplu izolat și niciun test extins pe alte teoreme”, spune el.
Minhyong Kim, de la International Centre for Mathematical Sciences din Marea Britanie, atrage la rândul său atenția că majoritatea matematicienilor încă lucrează cu creionul și hârtia. „Matematica este extrem de diversă. Unii vor adopta AI-ul cu entuziasm, alții vor rămâne la metodele tradiționale”.
O revoluție tăcută
Indiferent de ritmul adoptării, ceva s-a schimbat deja. Inteligența artificială nu mai e doar un instrument de completat propoziții sau de generat imagini, ci devine tot mai capabilă să pătrundă într-un teritoriu care părea inabordabil, cel al raționamentului matematic abstract.
Cât de departe va ajunge? Rămâne de văzut. Dar într-o lume în care demonstrările riguroase cer luni, uneori ani de muncă intensă, promisiunea unei colaborări între om și mașină este mai tentantă ca niciodată.
