Google DeepMind julkaisi tänään AlphaProof Nexuksen, agenttijärjestelmän, joka ratkoi yhdeksän vuosikymmeniä avoinna ollutta Erdős-matematiikkaongelmaa. Tutkimuspaperin mukaan kaksi näistä kysymyksistä oli ratkaisematta 56 vuoden ajan, ja jokaisen ratkaisun laskentakustannus pysyi muutamassa sadassa dollarissa.
Järjestelmä yhdistää Gemini 3.1 Pro -kielimallin Lean-nimiseen formaaliin todistuskieleen. Malli ehdottaa todistusaskeleita, Lean-kääntäjä tarkistaa ne ja palauttaa virheviestit takaisin uuden yrityksen pohjaksi. Symbolinen palautekierto paikkaa kielimallien tunnetut heikkoudet pitkissä logiikkaketjuissa.
Lean-tarkistin pitää päättelyn raiteilla
Perinteinen kielimallin matematiikkaratkaisu kantaa koko logiikkaketjun yhden vastauksen mittaan luonnollisella kielellä. AlphaProof Nexus tekee toisin. Gemini 3.1 Pro generoi yksittäisiä todistusaskeleita Leanin formaalilla syntaksilla, ja kääntäjä joko hyväksyy tai hylkää jokaisen niistä.
Virheviestit eivät katoa hukkaan. Ne siirtyvät seuraavalle yritykselle promptin osana, joten malli näkee tarkasti, missä päättely tökkäsi. The Decoderin uutisoinnin mukaan tutkijat kuvaavat tätä symbolisena turvaverkkona, joka antaa kielimallille reaaliaikaista palautetta logiikan oikeellisuudesta.
Lopullisessa vaiheessa ihminen vain varmistaa, että koneellisesti tarkistettu todistus vastaa alkuperäistä kysymystä. Itse todistuksen pätevyys nojaa Leanin kääntäjään, ei kielimallin omaan luotettavuuteen. Tämä erottaa lähestymistavan puhtaasti generatiivisista ratkaisijoista.
Yhdeksän avointa ongelmaa ja 56 vuoden takainen kysymys
Tutkimuspaperin mukaan AlphaProof Nexus yritti ratkaista 353:a avointa Erdős-ongelmaa. Niistä yhdeksän taipui, mukaan lukien kaksi kysymystä, jotka olivat olleet ratkaisematta 56 vuoden ajan.
Lisäksi järjestelmä todisti 44 ratkaisematonta otaksumaa Online Encyclopedia of Integer Sequencesin tietokannasta. Se ratkaisi 15 vuotta avoinna olleen kysymyksen Hilbertin funktioista algebrallisessa geometriassa ja paransi yhtä konveksin optimoinnin tunnettua rajaa.
Onnistumisprosentti on silti maltillinen. Yhdeksän ratkaisua 353 ongelmasta on alle kolme prosenttia, ja taipuneet kysymykset keskittyvät helpompaan päähän jakaumaa. AlphaProof Nexus on aputyökalu, ei automaattinen matematiikan ratkaisija. Vaikeimmat avoimet kysymykset säilyvät edelleen ihmistutkijoiden työpöydällä.
Neljä agenttitasoa kasvavalla työkalupakilla
AlphaProof Nexus ei ole yksittäinen monoliittinen agentti, vaan neljä eri kokonaisuutta kasvavalla työkalupakilla. Yksinkertaisin variantti, Agentti A, ajaa rinnakkain itsenäisiä Gemini 3.1 Pro -aliagentteja, jotka tuottavat Lean-askeleita silmukassa ja saavat kääntäjän palautteen takaisin.
Agentti B lisää kuvioon kyselyt AlphaProofiin, Googlen vahvistusoppimispohjaiseen olympia-matematiikkajärjestelmään. Se voi täyttää puuttuvia palasia todistuksen keskeltä. Agentti C tuo evolutiivisen kerroksen, jossa aliagentit jakavat yhteisen poolin todistusluonnoksia. Gemini 3.0 Flash arvioi luonnoksia uskottavuuden ja uutuuden mukaan Elo-järjestelmällä.
Täysi versio, Agentti D, yhdistää kaikki edelliset kerrokset. Mitä useampi kerros käytössä, sitä monimutkaisempia ongelmia järjestelmä taklaa. Inspiraatio evolutiiviseen vaiheeseen tulee suoraan DeepMindin aiemmin julkistamasta AlphaEvolvesta, joka käyttää samaa periaatetta algoritmien etsintään.
Pari sataa dollaria per ongelma muuttaa tutkimusta
Aiemmat näyttävät ratkaisut, kuten OpenAI:n päättelymalli, joka kumosi Erdősin yksikköetäisyysotaksuman, perustuvat raakaan kielimallien voimaan. AlphaProof Nexus valitsee toisen reitin: skaalautuvan ja formaalisti tarkistetun pipelinen, jonka jokainen vaihe on koneellisesti todennettavissa.
Halvempi inferenssi tarkoittaa, että agentin voi ajaa rutiininomaisesti suurelle avoimien kysymysten joukolle. Matemaatikot voivat seuloa läpi tuhansia otaksumia ja toivoa, että muutamat aukeavat ilman, että jokaiselle tarvitsee omistaa kuukausien manuaalinen työ.
Lähestymistapa on toinen kuin OpenAI:n vastaavissa kokeissa, mutta ei välttämättä ristiriidassa. Useat tutkijat ovat huomauttaneet, että OpenAI voisi kytkeä Leanin omaan järjestelmäänsä. DeepMindin painopiste on kuitenkin toistettavuudessa ja jokapäiväisessä tutkimustyökalussa, joka voi palvella matemaattisen tutkimuksen virtaviivaistamista.
Yhteenveto
AlphaProof Nexus ei ratkaise matematiikkaa puolesta. Se nostaa kielimallin avustamasta päättelystä paljon vahvemman kerroksen, jossa kääntäjä tarkistaa jokaisen askeleen. Yhdeksän avointa Erdős-ongelmaa, 56 vuotta avoinna ollut kysymys ja Hilbertin funktioita koskeva ratkaisu ovat konkreettisia todisteita siitä, että formaali verifikaatio ja kielimallit täydentävät toisiaan.
DeepMindin paperin mukaan systemaattinen ja edullinen agentti voi siirtää matemaatikkojen aikaa raakapäättelystä mielenkiintoisempien kysymysten muotoiluun. Onnistumisprosentti on yhä matala, mutta hinta-laatu-suhde tuo työkalun realistisesti tutkijoiden ulottuville.