Potom, čo Google DeepMind porazil ľudí vo všetkom, od Zahrajte si strategické stolové hry Prejsť na,
teraz tvrdí, že je na pokraji poraziť najlepších svetových študentov pri riešení matematických problémov.

So sídlom v Londýne Strojové učenie Spoločnosť 25. júla oznámila, že jej systémy umelej inteligencie (AI) vyriešili štyri zo šiestich problémov, ktoré dostali študenti na Medzinárodnej matematickej olympiáde (IMO) v roku 2024 v Bath v Spojenom kráľovstve. Umelá inteligencia poskytla presné dôkazy krok za krokom, ktoré hodnotili dvaja špičkoví matematici a dosiahli skóre 28/42 – iba jeden bod z územia zlatých medailí.

"Je to samozrejme veľmi významný pokrok," hovorí Joseph Myers, matematik z Cambridge, Spojené kráľovstvo, ktorý spolu s Fieldsovým medailistom Timom Gowersom preskúmali riešenia a pomohli vybrať pôvodné problémy pre tohtoročnú IMO.

DeepMind a ďalšie spoločnosti sa pretekajú v tom, kto nakoniec poskytne strojom dôkazy, na ktorých záleží Riešiť výskumné otázky z matematiky. Problémy prezentované na IMO, poprednej svetovej súťaži pre mladých matematikov, sa stali meradlom pokroku smerom k tomuto cieľu a považujú sa za „veľkú výzvu“ pre strojové učenie, uviedla spoločnosť.

„Je to prvýkrát, čo systém umelej inteligencie dosiahol medailový výkon,“ uviedol na tlačovom brífingu Pushmeet Kohli, viceprezident pre umelú inteligenciu v DeepMind. "Toto je dôležitý míľnik pri budovaní pokročilých vyšetrovateľov dôkazov," povedal Kohli.

Rozšírenie

Len pred pár mesiacmi, v januári, systém DeepMind Úspechy na medailovej úrovni AlphaGeometry dosiahnuté pri riešení jedného typu problémov IMO, a to tých v euklidovskej geometrii. Prvá umelá inteligencia, ktorá dosiahne zlatú medailu v celkovom teste – vrátane otázok z algebry, kombinatoriky a teórie čísel, ktoré sa vo všeobecnosti považujú za náročnejšie ako geometria – bude oprávnená získať cenu 5 miliónov dolárov, cenu AI ​​Mathematics Olympiad Prize (AIMO). (Ocenenie má prísne kritériá, ako je zverejnenie zdrojového kódu a práca s obmedzeným výpočtovým výkonom, čo znamená, že súčasné úsilie DeepMind by nespĺňalo podmienky.)

Vo svojom najnovšom pokuse výskumníci použili AlphaGeometry2 na vyriešenie problému s geometriou za menej ako 20 sekúnd; AI ​​je vylepšená a rýchlejšia verzia ich záznamového systému, hovorí počítačový špecialista DeepMind Thang Luong.

Pre ostatné typy otázok tím vyvinul úplne nový systém s názvom AlphaProof. AlphaProof vyriešil v súťaži dva problémy z algebry a jeden v teórii čísel, čo trvalo tri dni. (Účastníci skutočnej IMO majú dve stretnutia po 4,5 hodiny.) Nepodarilo sa vyriešiť dva problémy v kombinatorike, ďalšej oblasti matematiky.


Nahaufnahme einer Goldmedaille, gewonnen bei der 63. Internationalen Mathematik-Olympiade von einem rumänischen Teilnehmer.

Výskumníci mali zmiešané výsledky pri odpovedaní na matematické otázky pomocou jazykových modelov - typu systémov, ktoré poháňajú chatboty ako ChatGPT. Niekedy modely dávajú správnu odpoveď, ale nedokážu racionálne vysvetliť svoje úvahy a niekedy chrlia nezmysly.

Len minulý týždeň tím výskumníkov zo softvérových spoločností Numina a HuggingFace použil jazykový model na získanie strednej „ceny za pokrok“ AMIO založenej na zjednodušených verziách problémov IMO. Spoločnosti sprístupnili celé svoje systémy ako open source a sprístupnili ich ďalším výskumníkom na stiahnutie. Ale povedali víťaziPríroda, že samotné jazykové modely by na riešenie zložitejších problémov zrejme nestačili.

Iba trieda

AlphaProof kombinuje jazykový model s technológiou posilňovania výučby, ktorá využíva engine „AlphaZero“, ktorý spoločnosť úspešne použila pre útočné hry, ako sú Go a niektoré špecifické matematické problémy použité. Pri posilňovaní učenia sa neurónová sieť učí prostredníctvom pokusov a omylov. Funguje to dobre, keď sa jeho odpovede dajú vyhodnotiť pomocou objektívneho štandardu. Za týmto účelom bol AlphaProof vyškolený na čítanie a písanie dôkazov vo formálnom jazyku nazvanom Lean, ktorý sa používa v softvérovom balíku „Proof Assistant“ s rovnakým názvom, ktorý je obľúbený medzi matematikmi. Za týmto účelom AlphaProof otestoval, či sú jeho výstupy správne, spustením v balíku Lean, čo pomohlo vyplniť niektoré kroky v kóde.

Trénovanie jazykového modelu si vyžaduje obrovské množstvo údajov, no v Leane bolo k dispozícii len málo matematických dôkazov. Na prekonanie tohto problému tím vyvinul ďalšiu sieť, ktorá sa pokúsila preložiť existujúci záznam milióna problémov napísaných v prirodzenom jazyku, ale bez riešení napísaných človekom, do Lean, hovorí Thomas Hubert, výskumník strojového učenia DeepMind, ktorý spoluviedol vývoj AlphaProof. "Náš prístup bol, môžeme sa naučiť dokazovať, aj keď sme pôvodne necvičili na dôkazoch napísaných ľuďmi?" (Spoločnosť zaujala podobný prístup ako Go, kde sa jej AI naučila hrať hru tak, že hrala sama proti sebe, a nie podľa toho, ako to robia ľudia.)

Magické kľúče

Mnohé z Lean prekladov nedávali zmysel, ale dosť bolo dosť dobrých na to, aby sa AlphaProof dostal do bodu, kedy by mohol začať svoje cykly učenia. Výsledky boli oveľa lepšie, ako sa očakávalo, povedal Gowers na tlačovom brífingu. "Mnoho problémov v IMO má túto vlastnosť magického kľúča. Problém sa spočiatku javí ako ťažký, kým nenájdete magický kľúč, ktorý ho otvorí," povedal Gowers, ktorý pracuje na Collège de France v Paríži.

V niektorých prípadoch sa zdalo, že AlphaProof dokáže poskytnúť ďalší krok kreativity poskytnutím jedného správneho kroku z nekonečne veľkého možného riešenia. Je však potrebná ďalšia analýza, aby sa zistilo, či boli odpovede menej prekvapujúce, ako sa zdalo, dodal Gowers. Podobný diskurz sa objavil po tom prekvapujúcom "Vlak 37", DeepMinds AlphaGo bot u jeho slávne víťazstvo v roku 2016 nad najlepším svetovým hráčom Go vyrobený – prelomový bod pre AI.

Či je možné techniky zdokonaliť tak, aby fungovali na úrovni výskumu v matematike, sa ešte len uvidí, povedal Myers na tlačovom brífingu. "Môže sa rozšíriť na iné typy matematiky, ktoré nemusia mať milióny problémov?"

"Sme v bode, kde môžu dokázať nielen otvorené výskumné problémy, ale aj problémy, ktoré sú veľmi náročné pre tých najlepších mladých matematikov na svete," povedal počítačový špecialista DeepMind David Silver, ktorý bol v polovici 2010 hlavným výskumníkom pri vývoji AlphaGo.