Pärast OpenAI läbimurret tabas Erdose ülesandeid uus löök: Google'i AI-agent lahendas veel 9 avatud probleemi
Pärast OpenAI läbimurret tabas Erdose ülesandeid uus löök: Google’i AI-agent lahendas veel 9 avatud probleemi
Google DeepMind, Google ja akadeemilised partnerid avaldasid arXivis töö AlphaProof Nexuse kohta - süsteemi, mis otsib matemaatilisi tõestusi suurte keelemudelite põhiste agentidega ja kontrollib tulemuse Leanis. Agendi tugevaim variant lahendas autonoomselt 9 353 formaliseeritud avatud ülesandest ErdosProblemsi kataloogis ning tõestas ka 44 492 avatud hüpoteesist OEIS-is, täisarvujadade entsüklopeedias.
Uudist on lihtne segi ajada OpenAI hiljutise läbimurdega ühikkauguste probleemi juures, kuid need on eri lood. OpenAI puhul oli jutt ühest kõlavast tulemusest diskreetses geomeetrias. Google’i puhul on fookus kontrollitaval tõestusotsingul juba formaliseeritud uurimisülesannete kogumi jaoks.
Kuidas AlphaProof Nexus töötab
Uurija annab süsteemile Lean-faili koos teoreemi formaalse sõnastuse ja tühja kohaga tõestuse jaoks. Edasi parandavad Gemini 3.1 Pro põhised alam-agendid mustandit, saavad Leani kompilaatori veateateid ja kasutavad neid tagasisidena. Täiskonfiguratsioon ühendab eraldi alamsihtide jaoks ka AlphaProofi ning evolutsioonilise mehhanismi, kus kriitikud hindavad erinevaid katseid ja neid kasutatakse järgmistes jooksudes uuesti.
Erdose ülesannete puhul ei käivitanud autorid süsteemi käsitsi valitud ilusate näidete peal, vaid kõigil Leani formaliseeringutel, mis olid eksperimendi ajal Formal Conjecturesi repositooriumis saadaval: 353 sõnastust enam kui 1200 ülesandega kataloogist. Pärast iga edu kontrollisid eksperdid vastavust algsele probleemile. Tõestused avaldati google-deepmind/alphaproof-nexus-results repositooriumis ja tulemused kanti Terence Tao wikisse.
Miks see oluline on
Formaalne kontroll ei muuda LLM-i eksimatuks matemaatikuks. Artiklis kirjeldatakse otse läbikukkumisi: agent võis peita raskuse abilemmaks, milles oli lünk, või viidata olematule “tuntud” väitele. Kuid sellised vead ei läbi lõplikku barjääri. Edu läheb kirja ainult siis, kui Lean võtab tõestuse vastu ilma sorry-ta, see tähendab ilma sulgemata kohtadeta.
Ka piirangud on olulised. Valim kaldub ülesannete poole, mille kogukond on juba jõudnud Leanis kirja panna. OEIS-i puhul kontrollisid autorid lisaks jadade esimesi liikmeid testlemmadega, et vähendada vale formaliseerimise riski. Isegi Erdose nimekirjas sulges agent 9 ülesannet 353-st, mitte ei “lahendanud matemaatikat”.
Ometi on mõõtkava juba teine kui üksikdemonstratsioonil. Autorid kirjutavad mõnesaja dollari suurusest inferentsikulust ülesande kohta ning baasagent, mis vaheldumisi genereerib LLM-iga ja kontrollib Leanis, suutis hiljem korrata kõiki 9 õnnestumist, ehkki keerulistel ülesannetel kallimalt. AlphaProof Nexust juba kasutatakse või testitakse mitmes matemaatika ja füüsika valdkonnas.
Mis teaduses muutub
Peamine järeldus ei ole, et matemaatikud muutuvad üleliigseks. Inimesed peavad endiselt valima ülesandeid, formaliseerima sõnastusi, kontrollima Lean-koodi vastavust algsele küsimusele ja mõistma leitud tõestuse väärtust. Kuid AI roll nihkub märgatavalt: see ei ole enam ainult tekstiline abiline ega ainult olümpiaadiülesannete lahendaja, vaid tööriist kontrollitavate uue teadmise fragmentide otsimiseks.
OpenAI tulemuse järel näeb see välja nagu ühe suuna kiirenemine: suured laborid hakkavad näitama mitte lihtsalt arutlevaid mudeleid, vaid töötavaid kooslusi “agent pluss formaalne kontroll”. Kui selline lähenemine muutub odavamaks ja mugavamaks, võib järgmine läbimurre tulla mitte ühest efektse ülesande lahendusest, vaid väikeste tõestuste regulaarsest voost.
- arxiv.orgAdvancing Mathematics Research with AI-Driven Formal Proof Search
- github.comGitHub - google-deepmind/alphaproof-nexus-results: Lean math proofs generated by AlphaProof Nexus and accompanying natural language prose proofs.
- neuro.eeМодель OpenAI впервые автономно решила открытую задачу математики | Neuro.ee
- commons.wikimedia.orgFile:Google-Deep Mind headquarters in London, 6 Pancras Square.jpg - Wikimedia Commons
- commons.wikimedia.orgFile:Paul Erdos with Terence Tao.jpg - Wikimedia Commons













