Kun Google DeepMind voitti ihmiset kaikessa, alkaen Pelaa Siirry strategialautapeleihin,
se väittää nyt päihittävänsä maailman parhaat opiskelijat matematiikan tehtävien ratkaisemisessa.

Lontoossa sijaitseva Koneoppiminen Yhtiö ilmoitti 25. heinäkuuta, että sen tekoälyjärjestelmät ratkaisivat neljä kuudesta tehtävästä, jotka annettiin opiskelijoille vuoden 2024 kansainvälisessä matemaattisessa olympialaisessa (IMO) Bathissa, Isossa-Britanniassa. Tekoäly tarjosi tiukat, vaiheittaiset todisteet, jotka kaksi huippumatemaatikot arvioivat ja saavutti pisteet 28/42 - vain yksi piste kultamitalialueelta.

"Se on ilmeisesti erittäin merkittävä edistysaskel", sanoo Joseph Myers, matemaatikko Cambridgesta, Iso-Britanniasta, joka yhdessä Fields-mitalisti Tim Gowersin kanssa tarkasteli ratkaisuja ja auttoi valitsemaan alkuperäiset ongelmat tämän vuoden IMO:lle.

DeepMind ja muut yritykset kilpailevat viime kädessä tarjotakseen koneille todisteita, joilla on merkitystä Ratkaise matematiikan tutkimuskysymyksiä. Maailman johtavassa nuorten matemaatikoiden kilpailussa IMO:ssa esitellyistä ongelmista on tullut etenemisen vertailukohta tähän tavoitteeseen, ja niitä pidetään "suurena haasteena" koneoppimiselle, yhtiö sanoi.

"Tämä on ensimmäinen kerta, kun tekoälyjärjestelmä on saavuttanut mitalitason suorituskyvyn", DeepMindin tieteen tekoälyn varatoimitusjohtaja Pushmeet Kohli sanoi tiedotustilaisuudessa. "Tämä on tärkeä virstanpylväs kehittyneiden todisteiden tutkijoiden rakentamisessa", Kohli sanoi.

Laajennus

Vain muutama kuukausi sitten, tammikuussa, DeepMind-järjestelmä AlphaGeometry-mitalitason saavutuksia saavutettu yhden tyyppisten IMO-ongelmien ratkaisemisessa, nimittäin euklidisessa geometriassa. Ensimmäinen tekoäly, joka suoriutuu kultamitalitasolla kokonaistestissä – mukaan lukien algebran, kombinatoriikan ja lukuteorian kysymykset, joita pidetään yleensä geometriaa haastavampina – on oikeutettu saamaan 5 miljoonan dollarin palkinnon, AI ​​Mathematics Olympiad Prize (AIMO). (Palkintoon liittyy tiukat kriteerit, kuten lähdekoodin paljastaminen ja työskentely rajoitetulla laskentateholla, mikä tarkoittaa, että DeepMindin nykyiset ponnistelut eivät kelpaa.)

Uusimmassa yrityksessään tutkijat käyttivät AlphaGeometry2:ta geometriaongelman ratkaisemiseen alle 20 sekunnissa; tekoäly on parannettu ja nopeampi versio heidän ennätysjärjestelmästään, sanoo DeepMind-tietokoneasiantuntija Thang Luong.

Muille kysymyksille tiimi kehitti täysin uuden järjestelmän nimeltä AlphaProof. AlphaProof ratkaisi kaksi algebratehtävää kilpailussa ja yhden lukuteoriassa, mikä kesti kolme päivää. (Varsinaisen IMO:n osallistujilla on kaksi 4,5 tunnin mittaista istuntoa.) Se ei pystynyt ratkaisemaan näitä kahta ongelmaa kombinatoriikassa, toisessa matematiikan alueella.


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

Tutkijat ovat saaneet ristiriitaisia ​​tuloksia, kun he ovat vastanneet matemaattisiin kysymyksiin käyttämällä kielimalleja – sellaisia ​​järjestelmiä, jotka käyttävät chatbotteja, kuten ChatGPT:tä. Joskus mallit antavat oikean vastauksen, mutta eivät osaa selittää perustelujaan rationaalisesti, ja joskus he huutavat hölynpölyä.

Juuri viime viikolla ohjelmistoyritysten Numina ja HuggingFace tutkijaryhmä voitti kielimallin avulla AMIO-edistyspalkinnon, joka perustuu IMO-ongelmien yksinkertaistettuihin versioihin. Yritykset ovat tehneet koko järjestelmästään avoimen lähdekoodin ja asettaneet ne muiden tutkijoiden ladattavaksi. Mutta voittajat sanoivatLuonto, että kielimallit eivät luultavasti riittäisi ratkaisemaan vaikeampia ongelmia.

Vain luokka

AlphaProof yhdistää kielimallin vahvistusoppimisteknologiaan, joka käyttää "AlphaZero" -moottoria, jota yritys on menestyksekkäästi käyttänyt hyökkäyspeleissä, kuten Go ja joissakin. erityisiä matemaattisia ongelmia käytetty. Vahvistusoppimisessa hermoverkko oppii yrityksen ja erehdyksen kautta. Tämä toimii hyvin, kun hänen vastauksiaan voidaan arvioida objektiivisella standardilla. Tätä tarkoitusta varten AlphaProof koulutettiin lukemaan ja kirjoittamaan todisteita muodollisella kielellä nimeltä Lean, jota käytetään matemaatikoiden suosimassa samannimisessä Proof Assistant -ohjelmistopaketissa. Tätä varten AlphaProof testasi, olivatko sen tulosteet oikein suorittamalla ne Lean-paketissa, mikä auttoi täyttämään joitain koodin vaiheita.

Kielimallin kouluttaminen vaatii valtavia tietomääriä, mutta Leanissa oli vain vähän matemaattista näyttöä. Tämän ongelman ratkaisemiseksi tiimi kehitti lisäverkon, joka yritti kääntää olemassa olevan tietueen miljoonasta luonnollisella kielellä kirjoitetusta ongelmasta ilman ihmisen kirjoittamia ratkaisuja Lean-kieleksi, sanoo Thomas Hubert, DeepMind-koneoppimisen tutkija, joka johti AlphaProofin kehitystä. "Meidän lähestymistapamme oli, voimmeko oppia todistamaan, vaikka emme alun perin harjoitelleet ihmisten kirjoittamia todisteita?" (Yhtiö otti samanlaisen lähestymistavan Goon, jossa sen tekoäly oppi pelaamaan peliä pelaamalla itseään vastaan ​​sen sijaan, että ihmiset tekevät sen.)

Maagiset avaimet

Monet Lean-käännökset eivät olleet järkeviä, mutta riittävän hyviä, jotta AlphaProof pääsisi siihen pisteeseen, jossa se saattoi aloittaa vahvistamisoppimissyklinsä. Tulokset olivat paljon odotettua parempia, Gowers sanoi lehdistötilaisuudessa. "Monilla IMO:n ongelmilla on tämä taika-avainominaisuus. Ongelma näyttää aluksi vaikealta, kunnes löydät taika-avaimen, joka avaa sen", sanoi Gowers, joka työskentelee Collège de Francessa Pariisissa.

Joissakin tapauksissa AlphaProof näytti pystyvän tarjoamaan tuon ylimääräisen luovuuden askeleen tarjoamalla yhden oikean askeleen äärettömän suuresta mahdollisesta ratkaisusta. Mutta lisäanalyysiä tarvitaan sen määrittämiseksi, olivatko vastaukset vähemmän yllättäviä kuin näytti, Gowers lisäsi. Samanlainen keskustelu syntyi yllättävän keskustelun jälkeen "Juna 37", hänen DeepMinds AlphaGo -bottinsa kuuluisa vuoden 2016 voitto maailman parhaasta Go-pelaajasta tehty – käännekohta tekoälylle.

Nähtäväksi jää, voidaanko tekniikoita täydentää toimimaan matematiikan tutkimustasolla, Myers sanoi lehdistötilaisuudessa. "Voiko se laajentaa muihin matematiikkatyyppeihin, joissa ei ehkä ole miljoonia ongelmia?"

"Olemme siinä pisteessä, että he voivat todistaa avoimien tutkimusongelmien lisäksi myös ongelmia, jotka ovat erittäin haastavia maailman parhaille nuorille matemaatikoille", sanoi DeepMind-tietokoneasiantuntija David Silver, joka oli AlphaGoa kehittänyt johtava tutkija 2010-luvun puolivälissä.