A Google DeepMind bemutatta az AlphaProof Nexus nevű rendszert, amely kilenc nyitott Erdős-problémát és 44 egyéb matematikai sejtést oldott meg sikeresen. A kutatás részleteit a Science folyóiratban publikálták, megerősítve a korábbi előzetes eredményeket. A rendszer a Gemini 3.1 Pro modellt használja a bizonyítások keresésére, amelyeket egy Lean nevű szoftverrel ellenőriz.
A működés alapja, hogy az MI-ágens folyamatosan új stratégiákat próbál ki, miközben a Lean azonnal elutasítja a hibás lépéseket. Bár a rendszer a feladatok többségén elbukott, és néha nem létező tételekre hivatkozott, a sikeres megoldások igazolják az MI matematikai képességeit. Egy-egy probléma megoldása néhány száz dollárnyi számítási kapacitásba került.
A matematikus közösség egy része óvatosságra int a technológiával kapcsolatban. Több szakértő szerint az MI-rendszereknek továbbra is emberi útmutatásra van szükségük a feladatok kijelöléséhez és az eredmények ellenőrzéséhez.
Az eredeti szöveg (Perplexity Discover)
A Google DeepMind, az Alphabet része, szakmailag lektorált beszámolót tett közzé az AlphaProof Nexusról. Ez az MI-rendszer kilenc, Erdős Pál matematikus által felvetett nyitott problémát oldott meg, és bebizonyított 44 sejtést az egész számok sorozatainak online enciklopédiájából (OEIS). A tanulmány október 8-án, csütörtökön jelent meg a Science-ben. Két Erdős-problémát Erdős és Sárközy András vetett fel 1970-ben, és 56 évig megoldatlanok maradtak.
A tanulmány szakmailag lektorált megerősítést ad azoknak az eredményeknek, amelyeket a DeepMind először májusban tett közzé az arXivon. Akkor jelent meg, amikor az MI-laborok azzal versengenek, hogy rendszereik kutatási szintű matematikára is képesek, és ezt a versenyt néhány vezető matematikus bírálta.
A rendszer a Gemini 3.1 Pro segítségével keres bizonyításokat, ellenőrzésükre pedig a Lean bizonyításasszisztenst használja. A Lean gépiesen ellenőrzi az egyes lépéseket, és elutasít minden olyan bizonyítást, amelyben hézag van. Az ágens közben újabb és újabb stratégiákat próbál ki, gyakran sok kísérlettel párhuzamosan. A csapat 353 Erdős-problémával és 492 OEIS-sejtéssel próbálkozott. A 44 OEIS-bizonyítást kézzel ellenőrizték, és megállapították, hogy a problémákat helyesen formalizálták, és korábban még nem bizonyították őket. Az arXiv-előnyomat szerint minden megoldott Erdős-probléma „néhány száz dollárba” került számítási kapacitásban.
A rendszer az algebrai geometria négy nyitott problémája közül kettőt is megoldott, köztük Zanello egyik sejtését. A szerzők szerint nem tudnak olyan korábbi tanulmányról, amely ugyanezt a bizonyítási stratégiát alkalmazta volna. A DeepMind munkatársa, Pushmeet Kohli májusban elmondta, hogy az eredmények között volt egy 15 éves algebrai geometriai probléma és egy 7 éves kérdés a min-max optimalizálás területéről. Egy megállapítás kiemelkedett: az ágens egy sokkal egyszerűbb változata, amely csak előállít egy bizonyítást, majd ellenőrzi, szintén megoldotta mind a kilenc Erdős-problémát.
A rendszer a legtöbb megpróbált feladaton elbukott. Néhány sikertelen kísérletnél a Lean „sorry” helykitöltőjét csempészte a bizonyításba, hogy átugorjon egy lépést, amelyet nem tudott igazolni, máskor pedig nem létező tételekre hivatkozott. Josep Curto Díaz, a Katalóniai Nyílt Egyetem munkatársa az ABC-nek azt mondta, hogy a rendszer még mindig „strukturális emberi függőséget” mutat. Felhozott egy esetet, amelyben a kutatóknak kellett rávezetniük, hogy ellenpéldákat keressen.
A preprint megjelenése után Anatol Wegner fizikus amellett érvelt, hogy a „nyitott” Erdős-problémák közül többre már létezett megoldás a publikált szakirodalomban. Két esetben, mint írta, a feladat megfogalmazását megváltoztatták azután, hogy az ágens megtalálta a bizonyításokat. A spanyol Science Media Centre egyik kommentárja szerint a teljes rendszer túlbonyolított.
A tanulmány egy szeptemberi nyílt levelet követ, amelyben 25 Fields-érmes matematikus, köztük Terence Tao, óvott attól, hogy a matematika az eredmények halmozásáról szóló versennyé váljon. Swarat Chaudhuri, a DeepMind egyik szerzője az El Mundónak úgy fogalmazott, hogy ezeknek a rendszereknek „még mindig emberi útmutatásra van szükségük annak eldöntéséhez, mely problémákat oldják meg, eredményeiket pedig gondosan át kell vizsgálni”. Hozzátette: „A matematika végső soron emberi tevékenység.”
