Kilenc nyitott Erdős-problémát oldott meg a DeepMind AI-rendszere
Két feladat 56 éve várt megoldásra; a Science-ben megjelent tanulmány több tucat további matematikai eredményről is beszámol.
▶ 30 MÁSODPERCBEN
- MI TÖRTÉNT
- A Google DeepMind AlphaProof Nexus rendszere önállóan megoldott kilenc nyitott Erdős-problémát, és bizonyított 44 további matematikai sejtést.
- MIÉRT FONTOS
- A Science-ben közölt, szakértők által ellenőrzött munka azt mutatja, hogy az AI ellenőrizhető bizonyításokkal is hozzájárulhat a matematikai kutatáshoz.
Két, 56 éve megoldatlan Erdős-problémára is bizonyítást talált a Google DeepMind AlphaProof Nexus nevű AI-rendszere. A The Decoder beszámolója szerint a Science folyóiratban megjelent új tanulmány összesen kilenc önállóan megoldott feladatról számol be a vizsgált 353 nyitott Erdős-probléma közül. Ezeket a megoldásokat a kutatócsapat korábban már közzétette az interneten.
Nem csak Erdős feladataival boldogult
A rendszer az OEIS egészszámsorozat-adatbázisából 44 sejtést is bizonyított, vagyis olyan matematikai állításokat igazolt, amelyekhez addig nem volt bizonyítás. Emellett megoldott egy nyitott algebrai geometriai kérdést, és javított egy ismert korláton a min-max optimalizálásban. Utóbbi olyan számítási módszer, amelyet például egyes AI-modellek tanításánál is használnak.
A modell javít, a Lean ellenőriz
Az AlphaProof Nexus központi eleme a Gemini 3.1 Pro nagy nyelvi modell (LLM). Ez egészíti ki és dolgozza át a Lean formális nyelvén írt bizonyításvázlatokat: a matematikai lépéseket itt géppel ellenőrizhető szabályok szerint kell megfogalmazni. A Lean minden szerkesztési lépés után ellenőrzi az aktuális változatot, hibaüzenetei pedig visszajelzést adnak a modell következő próbálkozásához.
A nehezebb részfeladatokhoz a rendszer az AlphaProof nevű, bizonyításokra szakosodott eszközt is segítségül hívhatja. A kilenc Erdős-problémát azonban már egy olyan változat is megoldotta, amely nem használta az AlphaProofot. Ennél az eredménycsoportnál tehát a külön bizonyítóeszköz nélkül is működött a nyelvi modell és a Lean együttműködése.
TECH-SZÓTÁR
- Nagy nyelvi modell
- Szövegek feldolgozására és előállítására tanított AI-modell.
- Formális bizonyítás
- Pontosan meghatározott nyelven és szabályokkal leírt, géppel ellenőrizhető matematikai bizonyítás.
- Min-max optimalizálás
- Olyan optimalizálási módszer, amely egy lehetséges legnagyobb érték csökkentésére törekszik.
A bizonyítások közléséről is vita folyik
A DeepMind szakértőkkel ellenőriztette a munkáját, és folyóiratban közölte az eredményeket. Nem sokkal korábban az OpenAI több száz AI-val készített bizonyítást tett közzé a GitHubon, nem pedig szakfolyóiratokban. Az ebből kibontakozó vitában a Terence Tao matematikus köré szerveződő Association for Human Mathematics bojkottot sürgetett. A tét így nemcsak az, hogy mire képes az AI, hanem az is, hogyan kerüljenek az eredményei a matematikai szakmai nyilvánosság elé.
» Követett téma: AI · régió: USA · kulcsszó: DeepMind, gépi bizonyítás