OpenAI: Astra-malli ratkaisi 10 pitkään avoinna ollutta matemaattista ongelmaa 2 000 dollarilla

OpenAI paljasti lauantaina, että sen sisäinen Astra-malli tuotti uusia tuloksia 10 matematiikan ja teoreettisen tietojenkäsittelytieteen ongelmaan, jotka olivat pysyneet ratkaisemattomina vähintään vuosikymmenen. Yhtiö julkaisi koneellisesti tarkistettavat todistukset jokaisen väitteen tueksi. Yhtiö raportoi 10 ratkaisun token-kustannukseksi noin 2 000 dollaria nykyisillä API-hinnoilla.forbes+1

Varmennetut todistukset useilla aloilla

Tulokset kattavat korkeampiulotteisen pallojen pakkauksen, koodausteorian, kryptografian, ääriarvokombinatoriikan ja kvanttipeliteorian. Keskeinen tulos on eksplisiittinen konstruktio ei-sofisesta ryhmästä, mikä on ollut avoin kysymys vuodesta 1999 lähtien ja kumoaa konjektuurin, jonka mukaan kaikki numeroituvat ryhmät ovat sofisia. Astra kumosi myös Connesin jäykkyyskonjektuurin vuodelta 1980 ja ratkaisi kolme Paul Erdősin luettelon ongelmaa, mukaan lukien ongelma 183 monivärisistä Ramseyn luvuista.newscientist+1

OpenAI julkaisi 249-sivuisen käsikirjoituksen sekä Lean 4 -todistussertifikaatit GitHubissa Apache 2.0 -lisenssillä. Yhtiö raportoi "sorry"-merkintöjen määräksi nollan, mikä tarkoittaa, ettei yhtäkään formalisoidun todistuksen vaihetta jätetty todistamatta. Lean-ydin palauttaa binaarisen tuomion: todistus joko kääntyy tai ei, mikä poistaa tarpeen luottaa mallin tuotokseen sokeasti.siliconangle+1

Thomas Bloom, joka ylläpitää Erdősin ongelmaluetteloa, kutsui tuloksia "suuriksi uutisiksi" ja arvioi ne merkittävämmiksi kuin aiemman OpenAI-mallin toukokuussa tuottaman Erdősin yksikköetäisyyden vastaesimerkin. Abhishek Saha Lontoon Queen Mary -yliopistosta totesi, että mikä tahansa 10 ratkaisusta "olisi merkittävä ja vaikuttava saavutus".newscientist+1

Skeptikot kehottavat varovaisuuteen

Ilmoitus herätti terävää kritiikkiä. Tunnettu tekoälyskeptikko Gary Marcus kuvaili julkaisua "hämmästyttäväksi, mutta pahasti liioitelluksi". Hän väitti, ettei menestys muodollisesti varmennettavassa matematiikassa yleisty aloille, joilla varmentaminen on vaikeampaa. Hän huomautti, että 2 000 dollarin luku kattaa vain onnistuneet yritykset ja jättää huomioimatta asiakirjojen valmistelussa auttaneiden matemaatikkojen ja tietojenkäsittelytieteilijöiden palkat.garymarcus.substack

Francesco Fournier-Facio Cambridgen yliopistosta kyseenalaisti työn läpinäkyvyyden ja väitti, että sofisuuden ratkaisu nojaa vahvasti Andreas Thomin ja Gábor Kunin aiempiin artikkeleihin vuosilta 2016 ja 2019. OpenAI:n alkuperäistä väitettä, jonka mukaan 10 ongelman "pääasiallisessa tuloksessa ei ole tapahtunut edistystä vähintään vuosikymmeneen", muutettiin sen jälkeen, kun Fournier-Facio valitti sen olevan virheellinen.newscientist

Laajemmat vaikutukset

Astra on edelleen julkaisematon. OpenAI kuvailee sitä malliperheeksi, joka on rakennettu koordinoimaan useita agentteja laajoissa tehtävissä. Toimitusjohtaja Sam Altman on esitellyt mallia päättäjille Washingtonissa, mutta yhtiö ei ole ilmoittanut julkaisupäivää tai sitä, julkaistaanko se GPT-6-mallina vai muuna versiona.siliconangle

Ajankohta osuu yksiin sen kanssa, että matemaattinen yhteisö vastustaa tekoälyyrityksiä. Kesäkuussa Kansainvälinen matemaattinen unioni hyväksyi Leidenin julistuksen, jossa varoitetaan, että tekoälyyritykset "käyttävät julkaistua tutkimusta ilman suostumusta, ohittavat vertaisarvioinnin ja uhkaavat todistusten ja attribuution eheyttä".siliconangle