Suche
Mein Konto
După ce Google DeepMind a învins oamenii în orice, de la Joacă jocurile de societate Go to strategie,
acum pretinde că este pe punctul de a-i învinge pe cei mai buni studenți ai lumii la rezolvarea problemelor de matematică.
Cel din Londra Învățare automată Compania a anunțat pe 25 iulie că sistemele sale de inteligență artificială (AI) au rezolvat patru dintre cele șase probleme adresate studenților la Olimpiada Internațională de Matematică (IMO) din 2024 din Bath, Regatul Unit. AI a oferit dovezi riguroase, pas cu pas, evaluate de doi matematicieni de top și a obținut un scor de 28/42 - doar un punct din teritoriul cu medalia de aur.
„Este evident un progres foarte semnificativ”, spune Joseph Myers, un matematician din Cambridge, Marea Britanie, care, împreună cu medaliatul Fields Tim Gowers, a revizuit soluțiile și a ajutat la selectarea problemelor originale pentru IMO din acest an.
DeepMind și alte companii sunt în cursa pentru a oferi mașinilor dovezi care contează Rezolvați întrebări de cercetare în matematică. Problemele prezentate la IMO, principala competiție mondială pentru tinerii matematicieni, au devenit un etalon pentru progresul către acest obiectiv și sunt considerate o „mare provocare” pentru învățarea automată, a spus compania.
„Este prima dată când un sistem AI atinge performanțe la nivel de medalie”, a declarat Pushmeet Kohli, vicepreședinte al AI în știință la DeepMind, într-o conferință de presă. „Acesta este o piatră de hotar importantă în construirea anchetatorilor de probe avansate”, a spus Kohli.
Extensie
Cu doar câteva luni în urmă, în ianuarie, sistemul DeepMind Realizări la nivel de medalie AlphaGeometry realizat în rezolvarea unui tip de probleme IMO, și anume cele din geometria euclidiană. Prima IA care va evolua la nivel de medalie de aur la testul general – inclusiv întrebări de algebră, combinatorică și teoria numerelor, considerate în general mai provocatoare decât geometrie – va fi eligibilă pentru a primi un premiu de 5 milioane de dolari, Premiul Olimpiada de Matematică AI (AIMO). (Premiul are criterii stricte, cum ar fi dezvăluirea codului sursă și lucrul cu putere de calcul limitată, ceea ce înseamnă că eforturile actuale ale DeepMind nu s-ar califica.)
În cea mai recentă încercare, cercetătorii au folosit AlphaGeometry2 pentru a rezolva problema geometriei în mai puțin de 20 de secunde; AI este o versiune îmbunătățită și mai rapidă a sistemului lor de înregistrare, spune specialistul în computere DeepMind Thang Luong.
Pentru celelalte tipuri de întrebări, echipa a dezvoltat un sistem complet nou numit AlphaProof. AlphaProof a rezolvat două probleme de algebră în competiție și una în teoria numerelor, care a durat trei zile. (Participanții la IMO propriu-zis au două sesiuni a câte 4,5 ore fiecare.) A fost incapabil să rezolve cele două probleme în combinatorică, o altă zonă a matematicii.
Cercetătorii au avut rezultate mixte atunci când au răspuns la întrebări matematice folosind modele lingvistice - genul de sisteme care alimentează chatbot-uri precum ChatGPT. Uneori, modelele dau răspunsul corect, dar nu își pot explica raționamentul, iar uneori scot prostii.
Chiar săptămâna trecută, o echipă de cercetători de la companiile de software Numina și HuggingFace a folosit un model lingvistic pentru a câștiga un „premiu de progres” intermediar AMIO bazat pe versiuni simplificate ale problemelor IMO. Companiile și-au făcut întregul sistem open source și le-au pus la dispoziție pentru descărcare de către alți cercetători. Dar câștigătorii au spusNatură, că numai modelele de limbaj probabil nu ar fi suficiente pentru a rezolva probleme mai dificile.
Doar clasa
AlphaProof combină un model de limbaj cu tehnologia de învățare prin întărire care utilizează motorul „AlphaZero” pe care compania l-a folosit cu succes pentru jocuri de atac precum Go și unele probleme matematice specifice folosit. În învățarea prin întărire, o rețea neuronală învață prin încercare și eroare. Acest lucru funcționează bine atunci când răspunsurile sale pot fi evaluate folosind un standard obiectiv. În acest scop, AlphaProof a fost instruit să citească și să scrie dovezi într-un limbaj formal numit Lean, care este folosit în pachetul software „Proof Assistant” cu același nume, popular în rândul matematicienilor. Pentru a face acest lucru, AlphaProof a testat dacă ieșirile sale erau corecte, rulându-le în pachetul Lean, care a ajutat la completarea unora dintre pașii din cod.
Formarea unui model lingvistic necesită cantități masive de date, dar puține dovezi matematice erau disponibile în Lean. Pentru a depăși această problemă, echipa a dezvoltat o rețea suplimentară care a încercat să traducă o înregistrare existentă a unui milion de probleme scrise în limbaj natural, dar fără soluții scrise de oameni în Lean, spune Thomas Hubert, un cercetător DeepMind, care a condus dezvoltarea AlphaProof. „Abordarea noastră a fost, putem învăța să dovedim chiar dacă nu ne-am antrenat inițial pe dovezi scrise de oameni?” (Compania a adoptat o abordare similară cu Go, unde AI-ul său a învățat să joace jocul jucând împotriva ei înșiși, mai degrabă decât din modul în care o fac oamenii.)
Chei magice
Multe dintre traducerile Lean nu aveau sens, dar erau suficient de bune pentru a aduce AlphaProof în punctul în care și-ar putea începe ciclurile de învățare de consolidare. Rezultatele au fost mult mai bune decât se aștepta, a spus Gowers la conferința de presă. „Multe probleme de la IMO au această proprietate cheie magică. Problema pare greu la început până când găsești o cheie magică care o deschide”, a spus Gowers, care lucrează la Collège de France din Paris.
În unele cazuri, AlphaProof părea să poată oferi acel pas suplimentar de creativitate, oferind un pas corect dintr-o soluție posibilă infinit de mare. Dar este nevoie de analize suplimentare pentru a determina dacă răspunsurile au fost mai puțin surprinzătoare decât păreau, a adăugat Gowers. Un discurs asemănător a apărut după cel surprinzător „Trenul 37”, botul DeepMinds AlphaGo al lui celebra victorie din 2016 asupra celui mai bun jucător Go uman din lume făcut – un punct de cotitură pentru AI.
Rămâne de văzut dacă tehnicile pot fi perfecționate pentru a funcționa la nivel de cercetare în matematică, a spus Myers la conferința de presă. „Se poate extinde la alte tipuri de matematică pe care s-ar putea să nu aibă milioane de probleme pregătite?”
„Suntem în punctul în care pot dovedi nu numai probleme deschise de cercetare, ci și probleme care sunt foarte provocatoare pentru cei mai buni tineri matematicieni din lume”, a spus specialistul în computere DeepMind David Silver, care a fost cercetătorul principal care a dezvoltat AlphaGo la mijlocul anilor 2010.