uutiset

한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina

Koneen sydänraportti

Machine Heart -toimitusosasto

Gemini-suuren mallin ja AlphaZero-vahvistusoppimisalgoritmin avulla voit hallita geometriaa, algebraa ja lukuteoriaa.

Tekoälylle matemaattinen olympiadi ei ole enää ongelma.

Torstaina Google DeepMindin tekoäly sai päätökseen saavutuksen: tekoälyn avulla ratkaista tämän vuoden kansainvälisen matemaattisen olympialaisen IMO:n todellinen kysymys, ja se oli vain yhden askeleen päässä kultamitalista.

Juuri viime viikolla päättyneessä IMO-kilpailussa oli kuusi kysymystä, jotka koskivat algebraa, kombinatoriikkaa, geometriaa ja lukuteoriaa. Googlen ehdottama hybridi tekoälyjärjestelmä sai neljä kysymystä oikein ja sai 28 pistettä saavuttaen hopeamitalin.

Aiemmin tässä kuussa UCLA:n virkamiesprofessori Terence Tao oli juuri edistänyt tekoälyn matemaattista olympialaista (AIMO Progress Award) miljoonan dollarin palkinnolla. Tekoälyn ongelmanratkaisun taso oli yllättäen parantunut tälle tasolle ennen heinäkuuta.

IMO, tee kysymykset samanaikaisesti ja ratkaise vaikeimmat kysymykset oikein.

IMO on vanhin, suurin ja arvostetuin nuorten matemaatikoiden kilpailu, joka on järjestetty vuosittain vuodesta 1959 lähtien. Viime aikoina IMO-kilpailu on myös laajalti tunnustettu suureksi haasteeksi koneoppimisen alalla, ja siitä on tullut ihanteellinen vertailukohta tekoälyjärjestelmien edistyneiden matemaattisten päättelykykyjen mittaamiseen.

Tämän vuoden IMO-kilpailussa DeepMind-tiimin kehittämät AlphaProof ja AlphaGeometry 2 saavuttivat yhdessä virstanpylvään läpimurron.

Niistä AlphaProof on muodollisen matemaattisen päättelyn vahvistava oppimisjärjestelmä ja AlphaGeometry 2 on parannettu versio DeepMindin geometrian ratkaisujärjestelmästä AlphaGeometry.

Tämä läpimurto osoittaa keinotekoisen yleisälyn (AGI) potentiaalin kehittyneillä matemaattisilla päättelykyvyillä avata uusia tieteen ja teknologian alueita.

Joten miten DeepMindin tekoälyjärjestelmä osallistui IMO-kilpailuun?

Yksinkertaisesti sanottuna nämä matemaattiset ongelmat käännetään ensin manuaalisesti muodolliseen matemaattiseen kieleen, jotta tekoälyjärjestelmä voi ymmärtää ne. Virallisessa kilpailussa ihmiskilpailijat jättävät vastauksensa kahdessa istunnossa (kaksi päivää), aikaraja on 4,5 tuntia per istunto. AlphaProof+AlphaGeometry 2:sta koostuva tekoälyjärjestelmä ratkaisi yhden ongelman muutamassa minuutissa, mutta muiden ongelmien ratkaisemiseen kului kolme päivää. Mutta jos noudatat tiukasti sääntöjä, DeepMindin järjestelmä on aikakatkaissut. Jotkut ihmiset spekuloivat, että tähän voi liittyä paljon raakaa voimaa tapahtuvaa halkeilua.

AlphaProof ratkaisi kaksi algebratehtävää ja yhden lukuteoriatehtävän määrittämällä vastaukset ja todistamalla niiden oikeellisuuden, Google sanoi. Näihin kuuluu kilpailun vaikein ongelma, jonka tämän vuoden IMO:ssa ratkaisi vain viisi kilpailijaa. Ja AlphaGeometry 2 osoittaa geometriaongelman.

Tekoälyn antama ratkaisu: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html

IMO:n kultamitalisti ja Fields-mitalisti Timothy Gowers ja kaksinkertainen IMO:n kultamitalisti, IMO 2024 -ongelmanvalintakomitean puheenjohtaja, tohtori Joseph Myers arvostivat yhdistetyn järjestelmän antamat ratkaisut IMO:n pisteytyssääntöjen mukaisesti.

Jokainen kuudesta kysymyksestä on 7 pisteen arvoinen, jolloin enimmäispistemäärä on 42 pistettä. DeepMindin järjestelmä sai lopullisen pistemäärän 28, mikä tarkoittaa, että kaikki neljä sen ratkaisemaa tehtävää saivat täydelliset pisteet - mikä vastaa korkeinta pistemäärää hopeamitalin kategoriassa. Tänä vuonna kultamitalikynnys oli 29 pistettä, ja virallisen kilpailun 609 pelaajasta 58 voitti kultaa.

Tämä kaavio näyttää Google DeepMindin tekoälyjärjestelmän suorituskyvyn suhteessa ihmiskilpailijoihin IMO 2024 -tapahtumassa. Järjestelmä sai 28 pistettä yhteensä 42 pisteestä ja saavutti samalla tason kilpailun hopeamitalin kanssa. Lisäksi tänä vuonna 29 pistettä voi voittaa kultamitalin.

AlphaProof: muodollinen päättelymenetelmä

Googlen käyttämistä hybridi-AI-järjestelmistä AlphaProof on itse koulutettu järjestelmä, joka käyttää muodollista kieltä Lean todistaakseen matemaattisia väitteitä. Se yhdistää valmiiksi koulutetun kielimallin AlphaZero-vahvistusoppimisalgoritmiin.

Niiden joukossa muodolliset kielet tarjoavat tärkeitä etuja matemaattisten päättelytodistusten oikeellisuuden muodolliseen tarkistamiseen. Tähän asti tästä on ollut rajallista käyttöä koneoppimisessa, koska ihmisen kirjoittaman tiedon määrä oli hyvin rajallinen.

Sitä vastoin luonnolliset kieleen perustuvat menetelmät, vaikka niillä on pääsy suurempiin tietomääriin, tuottavat välipohjaisia ​​päättelyvaiheita ja ratkaisuja, jotka vaikuttavat järkeviltä, ​​mutta ovat virheellisiä.

Google DeepMind rakentaa sillan näiden kahden toisiaan täydentävän kentän välille hienosäätämällä Gemini-mallia kääntämään luonnollisen kielen ongelmalausekkeet automaattisesti muodollisiksi lauseiksi, mikä luo suuren kirjaston eri vaikeusasteisia muodollisia ongelmia.

Kun otetaan huomioon matemaattinen ongelma, AlphaProof luo ehdotettuja ratkaisuja ja sitten todistaa ne etsimällä mahdollisia todisteita Leanista. Jokaista löydettyä ja tarkistettua todistusratkaisua käytetään vahvistamaan AlphaProofin kielimallia ja parantamaan sen kykyä ratkaista myöhempiä haastavampia ongelmia.

Kouluttaakseen AlphaProofia Google DeepMind osoitti tai hylkäsi miljoonia matemaattisia ongelmia, jotka kattoivat monenlaisia ​​vaikeuksia ja aiheita IMO-kilpailua edeltäneiden viikkojen aikana. Kilpailun aikana käytetään myös harjoitussilmukkaa vahvistamaan itse luotujen kilpailuongelmavarianttien näyttöä, kunnes täydellinen ratkaisu löytyy.

AlphaProof-vahvistusoppimisen koulutussilmukkaprosessin infografiikka: Noin miljoona epävirallista matemaattista ongelmaa käännetään muodolliseen matemaattiseen kieleen muodollisen verkoston toimesta. Ratkaisija etsii sitten verkosta todisteita tai todisteita ongelmasta ja harjoittelee itseään vähitellen ratkaisemaan haastavampia ongelmia AlphaZero-algoritmin avulla.

Kilpailukykyisempi AlphaGeometry 2

AlphaGeometry 2 on merkittävästi paranneltu versio AlphaGeometrystä, matemaattisesta tekoälystä, joka ilmestyi Nature-lehdessä tänä vuonna. Se on neuro-symbolinen hybridijärjestelmä, jossa kielimalli perustuu Kaksosiin ja koulutetaan tyhjästä suuruusluokkaa enemmän synteettiseen dataan kuin edeltäjänsä. Tämä auttaa mallia ratkaisemaan haastavampia geometrisia ongelmia, mukaan lukien kohteen liikkeitä ja kulmien, mittasuhteiden tai etäisyyksien yhtälöitä koskevat ongelmat.

AlphaGeometry 2 sisältää symbolisen moottorin, joka on kaksi suuruusluokkaa nopeampi kuin edeltäjänsä. Kun uusia ongelmia kohdataan, uudet tiedon jakamismekanismit mahdollistavat erilaisten hakupuiden kehittyneet yhdistelmät monimutkaisempien ongelmien ratkaisemiseksi.

Ennen tämän vuoden kilpailua AlphaGeometry 2 pystyi ratkaisemaan 83 % kaikista historiallisista IMO:n geometrian ongelmista viimeisen 25 vuoden aikana, kun edeltäjänsä vain 53 %. IMO 2024:ssä AlphaGeometry 2 ratkaisi tehtävän 4 19 sekunnin kuluessa sen formalisoinnin vastaanottamisesta.

Esimerkki kysymyksestä 4 vaatii osoittamaan, että ∠KIL:n ja ∠XPY:n summa on 180°. AlphaGeometry 2 ehdottaa pisteen E rakentamista suoralle BI siten, että ∠AEB = 90°. Piste E auttaa määrittämään janan AB keskipisteen L ja luo näin useita samankaltaisia ​​kolmioita, kuten ABE ~ YBI ja ALE ~ IPC päätelmän todistamiseksi.

Google DeepMind raportoi myös, että osana IMO:n työtä tutkijat kokeilevat myös uutta luonnollisen kielen päättelyjärjestelmää, joka perustuu Geminiin ja huippuluokan luonnollisen kielen päättelyjärjestelmää, toivoen saavuttavansa edistyneitä ongelmanratkaisukykyjä. Järjestelmä ei vaadi kysymysten kääntämistä viralliselle kielelle ja se voidaan yhdistää muihin tekoälyjärjestelmiin. Tämän vuoden IMO:n kilpailukysymysten testissä se "osoitti suurta potentiaalia".

Google jatkaa tekoälymenetelmien tutkimista matemaattisen päättelyn edistämiseksi ja aikoo julkaista AlphaProofista pian lisää teknisiä yksityiskohtia.

Olemme innoissamme tulevaisuudesta, jossa matemaatikot käyttävät tekoälytyökaluja tutkiakseen hypoteeseja, kokeillakseen rohkeita uusia lähestymistapoja pitkäaikaisten ongelmien ratkaisemiseen ja suorittamassa nopeasti aikaa vieviä todisteiden elementtejä – ja Geminin kaltaiset tekoälyjärjestelmät tulevat vaikuttamaan matematiikkaan. ja enemmän laajasta päättelystä tulee entistä voimakkaampi.

tutkimusryhmä

Google sanoi, että uutta tutkimusta tuki kansainvälinen matemaattinen olympialainen, ja lisäksi:

AlphaProof-kehitystä johtivat Thomas Hubert, Rishi Mehta ja Laurent Sartran: Hussain Masoom, Aja Huang, Miklós Z. Horváth, Tom Zahavy, Vivek Veeriah, Eric Wieser, Jessica Yung, Lei Yu, Yannick Schroecker, Julian Schrittwieser, Ottavia Bertolli, Borja Ibarz, Edward Lockhart, Edward Hughes, Mark Rowland ja Grace Margand.

Heidän joukossaan Aja Huang, Julian Schrittwieser, Yannick Schroecker ja muut jäsenet olivat myös AlphaGo-paperin ydinjäseniä 8 vuotta sitten (2016). Kahdeksan vuotta sitten AlphaGo, jonka he rakensivat vahvistusoppimisen perusteella, tuli tunnetuksi. Kahdeksan vuotta myöhemmin vahvistusoppiminen loistaa jälleen AlphaProofissa. Joku valitti ystäväpiirissä: RL on niin palannut!

AlphaGeometry 2:n ja luonnollisen kielen päättelytyötä johtaa Thang Luong. AlphaGeometry 2:n kehitystä johtivat Trieu Trinh ja Yuri Chervonyi, ja tärkeitä panoksia ovat olleet Mirek Olšák, Xiaomeng Yang, Hoang Nguyen, Junehyuk Jung, Dawsen Hwang ja Marcelo Menegali.

Lisäksi David Silver, Quoc Le, Hassabis ja Pushmeet Kohli vastaavat koko projektin koordinoinnista ja johtamisesta.

Viitesisältö:

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/