Inteligența artificială la Olimpiada Internațională de Matematică: Cum AlphaProof și AlphaGeometry 2 au atins nivelul de medalie de argint

Raționamentul matematic este un aspect vital al capacităților cognitive umane, care impulsionează progresul în descoperirile științifice și dezvoltările tehnologice. Pe măsură ce ne străduim să dezvoltăm o inteligență artificială generală care să egaleze cogniția umană, este esențial să echipăm inteligența artificială cu capacități avansate de raționament matematic. În timp ce sistemele actuale de inteligență artificială pot rezolva probleme matematice de bază, ele se confruntă cu dificultăți în ceea ce privește raționamentul complex necesar pentru discipline matematice avansate, cum ar fi algebra și geometria. Cu toate acestea, acest lucru ar putea să se schimbe, deoarece Google DeepMind a făcut progrese semnificative în dezvoltarea capacităților de raționament matematic ale unui sistem de inteligență artificială. Acest progres a fost realizat la Olimpiada Internațională de Matematică (IMO) 2024. Înființată în 1959, IMO este cea mai veche și mai prestigioasă competiție matematică, care provoacă elevii de liceu din întreaga lume cu probleme de algebră, combinatorică, geometrie și teorie a numerelor. Fiecare an, echipe de tineri matematicieni concurează pentru a rezolva șase probleme foarte dificile. Anul acesta, Google DeepMind a prezentat două sisteme de inteligență artificială: AlphaProof, care se concentrează pe raționamentul matematic formal, și AlphaGeometry 2, care se specializează în rezolvarea problemelor geometrice. Aceste sisteme de inteligență artificială au reușit să rezolve patru dintre cele șase probleme, performând la nivelul unui medaliat cu argint.

AlphaProof: Combinarea inteligenței artificiale și a limbajului formal pentru demonstrarea teoremelor matematice

AlphaProof este un sistem de inteligență artificială proiectat pentru a demonstra afirmații matematice utilizând limbajul formal Lean. Acesta integrează Gemini, un model de limbaj pre-antrenat, cu AlphaZero, un algoritm de învățare prin întărire, renumit pentru stăpânirea jocurilor de șah, shogi și Go.

Modelul Gemini traduce declarații de problemă din limbaj natural în declarații formale, creând o bibliotecă de probleme cu niveluri de dificultate variate. Acest lucru are două scopuri: conversia limbajului natural imprecis în limbaj formal precis pentru verificarea demonstrațiilor matematice și utilizarea capacităților predictive ale lui Gemini pentru a genera o listă de soluții posibile cu precizia limbajului formal.

Când AlphaProof întâmpină o problemă, generează soluții potențiale și caută pași de demonstrație în Lean pentru a verifica sau infirma aceste soluții. Acesta este, în esență, o abordare neuro-simbiotică, în care rețeaua neurală, Gemini, traduce instrucțiuni din limbaj natural în limbajul formal simbolic Lean pentru a demonstra sau infirma afirmația. Similar cu mecanismul de auto-joc al lui AlphaZero, în care sistemul învață jucând jocuri împotriva lui însuși, AlphaProof se antrenează prin încercarea de a demonstra afirmații matematice. Fiecare încercare de demonstrație rafinează modelul de limbaj al lui AlphaProof, cu demonstrații reușite care întăresc capacitatea modelului de a aborda probleme mai dificile.

Pentru Olimpiada Internațională de Matematică (IMO), AlphaProof a fost antrenat prin demonstrarea sau infirmarea a milioane de probleme care acoperă niveluri de dificultate și subiecte matematice diferite. Acest antrenament a continuat pe parcursul competiției, unde AlphaProof și-a rafinat soluțiile până a găsit răspunsuri complete la probleme.

AlphaGeometry 2: Integrarea LLM și a inteligenței simbolice pentru rezolvarea problemelor geometrice

AlphaGeometry 2 este cea mai recentă iterație a seriei AlphaGeometry, proiectată pentru a aborda probleme geometrice cu precizie și eficiență îmbunătățite. Construind pe baza predecesorului său, AlphaGeometry 2 utilizează o abordare neuro-simbiotică care combină modelele de limbaj mare (LLM) cu inteligența simbolică. Această integrare combină logica bazată pe reguli cu capacitatea predictivă a rețelelor neurale pentru a identifica puncte auxiliare, esențiale pentru rezolvarea problemelor geometrice. LLM din AlphaGeometry prezice noi construcții geometrice, în timp ce inteligența simbolică aplică logica formală pentru a genera demonstrații.

Când se confruntă cu o problemă geometrică, LLM din AlphaGeometry evaluează numeroase posibilități, prezicând construcții cruciale pentru rezolvarea problemelor. Aceste predicții servesc ca indicii valoroase, ghidând motorul simbolic către deducții precise și apropiindu-se de o soluție. Acestă abordare inovatoare permite AlphaGeometry să abordeze provocări geometrice complexe care depășesc scenariile convenționale.

O îmbunătățire cheie în AlphaGeometry 2 este integrarea LLM Gemini. Acest model este antrenat de la zero pe mult mai multe date sintetice decât predecesorul său. Acest antrenament extins îi permite să abordeze probleme geometrice mai dificile, inclusiv cele care implică mișcări de obiecte și ecuații de unghiuri, rapoarte sau distanțe. În plus, AlphaGeometry 2 dispune de un motor simbolic care funcționează cu două ordine de mărime mai rapid, permițându-i să exploreze alternative de soluții cu o viteză fără precedent. Aceste progrese fac din AlphaGeometry 2 un instrument puternic pentru rezolvarea problemelor geometrice complexe, stabilind un nou standard în domeniu.

AlphaProof și AlphaGeometry 2 la IMO

Anul acesta, la Olimpiada Internațională de Matematică (IMO), participanții au fost testați cu șase probleme diverse: două de algebră, una de teorie a numerelor, una de geometrie și două de combinatorică. Cercetătorii de la Google au tradus aceste probleme în limbaj matematic formal pentru AlphaProof și AlphaGeometry 2. AlphaProof a abordat două probleme de algebră și una de teorie a numerelor, inclusiv cea mai dificilă problemă a competiției, rezolvată de doar cinci concurenți umani anul acesta. Între timp, AlphaGeometry 2 a rezolvat cu succes problema de geometrie, deși nu a reușit să rezolve cele două provocări de combinatorică.

Fiecare problemă de la IMO valorează șapte puncte, adăugându-se la un total de 42 de puncte. AlphaProof și AlphaGeometry 2 au obținut 28 de puncte, realizând scoruri perfecte la problemele pe care le-au rezolvat. Acest lucru i-a plasat la nivelul superior al categoriei de medalii de argint. Pragul pentru medalia de aur anul acesta a fost de 29 de puncte, atins de 58 dintre cei 609 de concurenți.

Următorul salt: Limbaj natural pentru provocări matematice

AlphaProof și AlphaGeometry 2 au demonstrat progrese impresionante în capacitățile de rezolvare a problemelor matematice ale inteligenței artificiale. Cu toate acestea, aceste sisteme încă se bazează pe experți umani pentru a traduce probleme matematice în limbaj formal pentru procesare. În plus, nu este clar cum aceste abilități matematice specializate ar putea fi integrate în alte sisteme de inteligență artificială, cum ar fi explorarea ipotezelor, testarea soluțiilor inovatoare pentru problemele de lungă durată și gestionarea eficientă a aspectelor consumatoare de timp ale demonstrațiilor.

Pentru a depăși aceste limitări, cercetătorii de la Google dezvoltă un sistem de raționament în limbaj natural bazat pe Gemini și pe cercetările lor recente. Acest nou sistem are ca scop să avanseze capacitățile de rezolvare a problemelor fără a necesita traducerea limbajului formal și este proiectat pentru a se integra cu ușurință cu alte sisteme de inteligență artificială.

Concluzia

Performanța lui AlphaProof și AlphaGeometry 2 la Olimpiada Internațională de Matematică reprezintă un salt semnificativ înainte în capacitățile inteligenței artificiale de a aborda raționamentul matematic complex. Ambele sisteme au demonstrat un nivel de performanță de medalie de argint, rezolvând patru dintre cele șase probleme dificile, demonstrând progrese semnificative în demonstrarea teoremelor formale și în rezolvarea problemelor geometrice. În ciuda realizărilor lor, aceste sisteme de inteligență artificială încă depind de intrarea umană pentru traducerea problemelor în limbaj formal și se confruntă cu provocări de integrare cu alte sisteme de inteligență artificială. Cercetările viitoare au ca scop să îmbunătățească în continuare aceste sisteme, posibil integrând raționamentul în limbaj natural pentru a-și extinde capacitățile pe o gamă mai largă de provocări matematice.