Pärast seda, kui Google DeepMind võitis inimesi kõiges, alates Mängi Mine strateegia lauamängudesse,
see väidab nüüd olevat matemaatikaülesannete lahendamisel maailma parimate õpilaste ületamise äärel.
Londonis asuv Masinõpe Ettevõte teatas 25. juulil, et tema tehisintellekti (AI) süsteemid lahendasid neli kuuest ülesandest, mis anti õpilastele 2024. aasta rahvusvahelisel matemaatikaolümpiaadil (IMO) Ühendkuningriigis Bathis. Tehisintellekt esitas ranged, samm-sammult tõendid, mida hindasid kaks tippmatemaatikut ja saavutas tulemuseks 28/42 – vaid üks punkt kuldmedali territooriumist.
"See on ilmselgelt väga oluline edasiminek," ütleb Ühendkuningriigi Cambridge'i matemaatik Joseph Myers, kes koos Fieldsi medalisti Tim Gowersiga vaatas lahendused üle ja aitas valida selle aasta IMO algsed probleemid.
DeepMind ja teised ettevõtted võistlevad selle nimel, et pakkuda masinatele lõpuks olulisi tõendeid Lahendage uurimisküsimusi matemaatikas. Maailma juhtival noorte matemaatikute konkursil IMO esitletud probleemid on muutunud selle eesmärgi saavutamise etaloniks ja neid peetakse masinõppe jaoks "suureks väljakutseks", teatas ettevõte.
"See on esimene kord, kui AI-süsteem on saavutanud medalitasemel jõudluse," ütles DeepMindi AI teaduse asepresident Pushmeet Kohli pressibriifingul. "See on oluline verstapost kõrgetasemeliste tõendite uurijate loomisel," ütles Kohli.
Laiendus
Vaid paar kuud tagasi, jaanuaris, DeepMind süsteem AlphaGeometry medalitaseme saavutused saavutatud üht tüüpi IMO probleemide lahendamisel, nimelt Eukleidilise geomeetria probleemide lahendamisel. Esimene tehisintellekt, kes sooritab üldises testis kuldmedali tasemel – sealhulgas algebra, kombinatoorika ja arvuteooria küsimused, mida üldiselt peetakse keerulisemaks kui geomeetria – on õigus saada 5 miljonit dollarit, AI matemaatikaolümpiaadi auhinda (AIMO). (Auhinnal on ranged kriteeriumid, nagu lähtekoodi avalikustamine ja piiratud arvutusvõimsusega töötamine, mis tähendab, et DeepMindi praegused jõupingutused ei kvalifitseeru.)
Oma viimases katses kasutasid teadlased AlphaGeometry2 geomeetriaprobleemi lahendamiseks vähem kui 20 sekundiga; AI on nende rekordsüsteemi täiustatud ja kiirem versioon, ütleb DeepMindi arvutispetsialist Thang Luong.
Muud tüüpi küsimuste jaoks töötas meeskond välja täiesti uue süsteemi nimega AlphaProof. AlphaProof lahendas kaks algebraülesannet võistlusel ja ühe arvuteoorias, mis võttis aega kolm päeva. (Tegelikus IMO-s osalejatel on kaks 4,5-tunnist seanssi.) See ei suutnud lahendada kahte ülesannet kombinatoorikas, mis on teine matemaatika valdkond.

Teadlastel on keelemudelite abil matemaatilistele küsimustele vastamisel olnud erinevaid tulemusi – selliseid süsteeme, mis kasutavad vestlusroboteid nagu ChatGPT. Mõnikord annavad mudelid õige vastuse, kuid ei suuda oma arutluskäiku ratsionaalselt selgitada, ja mõnikord nad ajavad jama.
Just eelmisel nädalal kasutas tarkvaraettevõtete Numina ja HuggingFace teadlaste meeskond keelemudelit, et võita IMO probleemide lihtsustatud versioonidel põhinev AMIO vaheauhind. Ettevõtted on muutnud kogu oma süsteemid avatud lähtekoodiga ja teinud need teistele teadlastele allalaadimiseks kättesaadavaks. Aga võitjad ütlesidLoodus, et keelemudelitest üksi ilmselt raskemate probleemide lahendamiseks ei piisa.
Ainult klass
AlphaProof ühendab keelemudeli tugevdava õppetehnoloogiaga, mis kasutab "AlphaZero" mootorit, mida ettevõte on edukalt kasutanud ründemängude jaoks, nagu Go ja mõned spetsiifilisi matemaatilisi probleeme kasutatud. Tugevdusõppes õpib närvivõrk katse-eksituse meetodil. See toimib hästi, kui tema vastuseid saab hinnata objektiivse standardi abil. Selleks koolitati AlphaProof lugema ja kirjutama tõestusi ametlikus keeles nimega Lean, mida kasutatakse matemaatikute seas populaarses samanimelises tarkvarapaketis Proof Assistant. Selleks testis AlphaProof, kas selle väljundid on õiged, käivitades need Lean-paketis, mis aitas täita mõnda koodi sammu.
Keelemudeli koolitamine nõuab tohutuid andmemahtusid, kuid Leanis oli vähe matemaatilisi tõendeid. Selle probleemi lahendamiseks töötas meeskond välja täiendava võrgustiku, mis üritas tõlkida leani keeleks olemasolevat miljonit probleemi, mis oli kirjutatud loomulikus keeles, kuid ilma inimese poolt kirjutatud lahendusteta, ütleb Thomas Hubert, DeepMindi masinõppe uurija, kes juhtis AlphaProofi väljatöötamist. "Meie lähenemisviis oli, kas me saame õppida tõestama isegi siis, kui me ei treeninud algselt inimeste kirjutatud tõestusi?" (Ettevõte kasutas Go-ga sarnast lähenemist, kus tema tehisintellekt õppis mängu mängima pigem iseenda vastu kui inimeste käitumise järgi.)
Maagilised võtmed
Paljud Leani tõlked ei olnud mõistlikud, kuid need olid piisavalt head, et AlphaProof jõuda selleni, et see saaks alustada oma tugevdamisõppetsükleid. Tulemused olid oodatust palju paremad, ütles Gowers pressibriifingul. "Paljudel IMO probleemidel on see võluvõtme omadus. Probleem tundub alguses raske, kuni leiate võluvõtme, mis selle avab," ütles Gowers, kes töötab Pariisis Collège de France'is.
Mõnel juhul tundus, et AlphaProof suudab pakkuda selle loovuse lisaastme, pakkudes ühe õige sammu lõpmatult suurest võimalikust lahendusest. Kuid on vaja täiendavat analüüsi, et teha kindlaks, kas vastused olid vähem üllatavad, kui tundusid, lisas Gowers. Sarnane diskursus tekkis pärast üllatavat "Rong 37", DeepMindsi AlphaGo robot tema juures kuulus 2016. aasta võit maailma parima Go-mängija üle tehtud – pöördepunkt AI jaoks.
Seda, kas tehnikaid saab täiustada, et töötada matemaatika uurimistasemel, tuleb veel näha, ütles Myers pressibriifingul. "Kas seda saab laiendada ka teist tüüpi matemaatikale, millel ei pruugi olla miljoneid ülesandeid koolitatud?"
"Oleme selles punktis, kus nad suudavad tõestada mitte ainult avatud uurimisprobleeme, vaid ka probleeme, mis on maailma parimatele noortele matemaatikutele väga rasked," ütles DeepMindi arvutispetsialist David Silver, kes oli 2010. aastate keskel AlphaGo väljatöötamise juhtivteadur.
