DeepMindin tekoäly ratkaisi yhdeksän Erdősin ongelmaa Science-lehdessä

Alphabet-yhtiöön ↗ 0.87% kuuluva Google DeepMind on julkaissut vertaisarvioidun raportin AlphaProof Nexus -tekoälyjärjestelmästä, joka ratkaisi yhdeksän matemaatikko Paul Erdősin esittämää avointa ongelmaa ja todisti 44 konjektuuria On-Line Encyclopedia of Integer Sequences (OEIS) -tietokannasta. Artikkeli ilmestyi torstaina 8. lokakuuta Science-lehdessä. Kaksi Erdősin ongelmista oli peräisin vuodelta 1970, jolloin Erdős ja András Sárközy esittivät ne, ja ne olivat pysyneet ratkaisemattomina 56 vuoden ajan.elmundo+2

Tutkimus antaa vertaisarvioidun tuen tuloksille, jotka DeepMind julkaisi alun perin arXiv-palvelussa toukokuussa. Se julkaistiin aikana, jolloin tekoälylaboratoriot kilpailevat osoittaakseen järjestelmiensä kykenevän tutkimustason matematiikkaan, mitä jotkut johtavat matemaatikot ovat kritisoineet.abc+1

Miten se toimii

Järjestelmä käyttää Gemini 3.1 Pro -mallia todistusten etsimiseen ja Lean-todistusavustajaa niiden tarkistamiseen. Lean varmentaa jokaisen vaiheen mekaanisesti ja hylkää todistukset, joissa on aukkoja. Agentti kokeilee jatkuvasti uusia strategioita, usein useita yrityksiä rinnakkain. Tiimi yritti ratkaista 353 Erdősin ongelmaa ja 492 OEIS-konjektuuria. He tarkistivat 44 OEIS-todistusta käsin ja varmistivat, että ongelmat oli formalisoitu oikein ja niitä ei ollut todistettu aiemmin. arXiv-esijulkaisun mukaan jokainen ratkaistu Erdősin ongelma maksoi "muutamia satoja dollareita" laskentakustannuksina.arxiv+2

Järjestelmä ratkaisi myös kaksi neljästä algebrallisen geometrian avoimesta ongelmasta, mukaan lukien Zanellon konjektuurin. Tekijöiden mukaan he eivät tiedä aiemmista tutkimuksista, joissa olisi käytetty samaa todistusstrategiaa. DeepMindin Pushmeet Kohli kertoi toukokuussa, että tuloksiin kuului 15 vuotta vanha algebrallisen geometrian ongelma ja 7 vuotta vanha min-max-optimoinnin kysymys. Yksi havainto erottui joukosta: agentin huomattavasti yksinkertaisempi versio, joka vain tuottaa todistuksen ja tarkistaa sen, ratkaisi myös kaikki yhdeksän Erdősin ongelmaa.elmundo+2

Rajoitukset ja kritiikki

Järjestelmä epäonnistui useimmissa kokeilemissaan ongelmissa. Joissakin epäonnistuneissa yrityksissä se lisäsi Leanin "sorry"-paikkamerkin todistukseen ohittaakseen vaiheen, jota se ei kyennyt todistamaan, tai viittasi teoreemoihin, joita ei ole olemassa. Katalonian avoimen yliopiston Josep Curto Díaz kertoi ABC:lle, että järjestelmällä on yhä "rakenteellinen riippuvuus ihmisestä". Hän viittasi tapaukseen, jossa tutkijoiden oli ohjattava järjestelmää etsimään vastaesimerkkejä.elmundo+1

Esijulkaisun jälkeen fyysikko Anatol Wegner väitti, että useisiin "avoimiin" Erdősin ongelmiin oli jo olemassa ratkaisut julkaistuissa töissä. Kahdessa tapauksessa hän kirjoitti, että ongelman sanamuotoa muutettiin sen jälkeen, kun agentti oli löytänyt todistuksensa. Espanjan Science Media Centren kommentti kutsui koko järjestelmää ylisuunnitelluksi.sciencemediacentre+1

Artikkeli seuraa syyskuussa julkaistua avointa kirjettä, jossa 25 Fieldsin mitalistia, mukaan lukien Terence Tao, varoittivat matematiikan muuttamisesta kilpailuksi vastausten keräämisessä. DeepMindin kirjoittajiin kuuluva Swarat Chaudhuri kertoi El Mundolle, että nämä järjestelmät "tarvitsevat yhä ihmisen ohjausta päättääkseen, mitä ongelmia ratkaista, ja vaativat tulostensa huolellista tarkistamista". Hän lisäsi: "Loppujen lopuksi matematiikka on inhimillistä toimintaa".elmundo