AlphaProof: Inteligența Artificială care Revolutionează Dovada Matematică

AlphaProof, creat de echipa Google DeepMind, reprezintă un avans semnificativ în domeniul inteligenței artificiale (IA), reușind să concureze aproape de nivelul medaliei de aur la prestigioasa Olimpiadă Internațională de Matematică din 2024. Acest sistem IA a clasat performanțele sale la nivelul medaliștilor de argint, lipsindu-i doar un punct pentru a obține aurul.

Deși computerele sunt recunoscute pentru abilitatea lor de a efectua calcule rapide, ele au întâmpinat dificultăți în competițiile de matematică de nivel înalt, din cauza necesității de logică și raționament avansat. În esență, calculatoarele pot efectua operațiuni aritmetice complexe într-un timp record, dar adesea nu înțeleg esența matematică din spatele acestor operații. De exemplu, în timp ce adunarea poate părea simplă, oamenii pot realiza demonstrații semi-formale bazate pe definițiile adunării sau pot apela la aritmetica Peano pentru a defini proprietățile numerelor naturale și operațiunile acestora printr-un set de axiome.

Pentru a efectua o demonstrație matematică, este necesară înțelegerea structurii fundamentale a matematicii. Modul în care matematicienii construiesc demonstrații, numărul de pași necesari pentru a ajunge la o concluzie și ingeniozitatea designului acestor pași sunt mărturii ale geniului și eleganței lor matematice. Thomas Hubert, cercetător la DeepMind și autor principal al studiului AlphaProof, menționează: “Știați că Bertrand Russell a publicat o carte de 500 de pagini pentru a demonstra că unu plus unu egal doi?”

Echipa DeepMind a dorit să dezvolte o IA care să înțeleagă matematica la acest nivel. Acest lucru a început prin soluționarea unei probleme obișnuite în IA: lipsa datelor de antrenament. Modelele mari de limbaj, care alimentează sistemele IA precum Chat GPT, învață din miliarde de pagini de text. Deși bazele lor de date conțin texte despre matematică, succesul lor în demonstrarea teoremelor matematice este limitat de modul lor de funcționare: acestea se bazează pe rețele neurale enorme pentru a prezice următorul cuvânt sau token în secvențe generate ca răspuns la prompturile utilizatorilor. Raționamentul lor este statistic prin design, ceea ce înseamnă că oferă răspunsuri care “par” corecte.

DeepMind a necesitat ca IA să nu doar “pară” corectă, ci să fie “realmente” corectă, garantând certitudinea absolută. Acest lucru a necesitat un mediu de antrenament complet nou și formalizat, pentru care echipa a folosit un pachet software numit Lean. Lean este un program de computer care ajută matematicienii să scrie definiții și demonstrații precise, folosind un limbaj de programare formal numit, de asemenea, Lean. Odată ce o afirmație matematică este tradusă sau formalizată și încărcată în program, acesta poate verifica dacă demonstrația este corectă.

Știință&Tehnică

Revista “Ştiinţă şi Tehnică“, cea mai cunoscută şi longevivă publicaţie de popularizare a ştiintelor din România