DeepMind kilenc bizonyítása újdonságpróbán

Egy matematikai bizonyítás lehet elegáns, mégis maradhat benne olyan hiba, amelyet évekig senki sem vesz észre. A Google DeepMind AlphaProof Nexus nevű MI-ügynöke kilenc, Paul Erdős által felvetett feladathoz készített bizonyítást, és egy szoftver minden lépést ellenőrzött. A kutatás első változata májusban preprintként jelent meg, majd szakmai lektorálás után október 8-án közölte a Science (Science). A szoftver a logikai helyességet ellenőrizhette, azt viszont már matematikusoknak kellett eldönteniük, hogy a bizonyítás újat is mond-e.

A bíráló, akit nem lehet meggyőzni

A chatbotok meggyőzően tudnak matematikai szöveget írni. Egy magabiztos bekezdés elfedhet egy hiányzó lépést, amelyet csak a figyelmes olvasó vesz észre. Az AlphaProof Nexus ezt a csapdát kerüli el: Lean nyelven dolgozik. Ebben a programozási nyelvben a definíciókat, állításokat és bizonyításokat olyan pontosan lehet megadni, hogy a számítógép ellenőrizni tudja őket.

A Leant úgy képzelhetjük el, mint egy bírálót, aki végigolvassa a kész bizonyítás minden sorát, és rögzített szabályok alapján ellenőrzi. A stílus nem számít. Ha egy lépés nem következik az előzőekből, a bizonyítás elbukik, bármilyen elegánsnak tűnik is a többi része.

A kutatócsoport szerint az ügynök Lean nyelven megírt bizonyításokra keresett. A kutatók egy korábbi DeepMind-rendszerhez, az AlphaProofhoz is hozzáférést adtak neki; ezt kifejezetten matematikai bizonyításokra fejlesztették. A csapat tesztjeiben egy egyszerűbb összeállítás ugyanazt az eredményt hozta: egy Leanhez kapcsolt nyelvi modell AlphaProof nélkül is elkészítette mind a kilenc Erdős-bizonyítást (The Decoder). Ezekhez a feladatokhoz tehát nem volt szükség a specializált rendszerre.

A tanulmány olyan bizonyításokról számol be, amelyeket a Lean elfogadott: kilenc Erdős-állításhoz, valamint az egész számsorozatokat és mintázatokat gyűjtő Online Encyclopedia of Integer Sequences 44 sejtéséhez. A sejtések olyan állítások, amelyeket igaznak tartanak, de még nem bizonyítottak (Science). Az Erdős-eredmények között szerepel egy egész számokra vonatkozó, kétrészes kérdés, amelyet Erdős Pál és Sárközy András 1970-ben vetett fel. A kérdés több mint fél évszázadon át nyitott maradt (ABC).

Amit a bíráló nem lát

A Lean garanciája pontosan körülhatárolható: azt igazolja, hogy a bizonyítás a kódban leírt állítást bizonyítja. Arra viszont nem ad választ, hogy a kód valóban azt fejezi-e ki, amit Erdős eredetileg értett, megoldotta-e már valaki korábban a kérdést, és hoz-e új felismerést a válasz.

Az 1970-es feladat jól mutatja, miért számít ez utóbbi két kérdés. A második részéből következik az első, ezért egyetlen bizonyítás mindkettőt megoldja. Az agent bizonyításai nyomán kiderült, hogy az eredeti, 1970-es cikk egyik konstrukciójának kisebb módosítása szintén választ ad mindkét részre (arXiv). Az agent bizonyításai helyesek voltak, a feladat megoldása azonban közelebb állt, mint amit a „nyitott” címke sugallt.

Az ilyen esetek felismeréséhez a területet jól ismerő matematikusok kellenek. Gergely Bérczi, a dániai Aarhusi Egyetem matematikusa és a tanulmány egyik szerzője segített kiválasztani a megfelelő feladatokat és ellenőrizni a megoldásokat (Aarhusi Egyetem). Részt vett a bizonyítások olyan változatainak megírásában is, amelyeket az emberi olvasók követni tudnak. Lean az egyes lépéseket ellenőrizte, Bérczi és munkatársai pedig azt mérlegelték, mit tesznek hozzá ezek a lépések a matematikához.

A mostani tanulmány más kérdést vet fel, mint az előző hónap egyik fontos eredménye. Akkor az Anthropic Claude-ja egy már ismert bizonyítást írt át Leannek: ez volt Fermat utolsó tételének bizonyítása (To Brief). Egy híres, már ismert bizonyítás átírásánál nem merül fel az újdonság kérdése. A nyitottnak tekintett állítások között keresve viszont az újdonság megítélése válik a munka fő kérdésévé.

A kutatócsoport közzétette a bizonyításfájlokat, így mások is lefuttathatják őket ugyanazon az ellenőrző rendszeren (GitHub). A tanulmány egy jól körülhatárolható előrelépést mutat be: egy MI-ügynök géppel ellenőrizhető bizonyításokat készített néhány olyan állításhoz, amelyet a matematikusok korábban nyitottnak tekintettek. A garancia azokra az állításokra vonatkozik, ahogyan azokat Leanben megfogalmazták. Annak megítélése, hogy az egyes bizonyítások mit adtak hozzá a matematikához, továbbra is az őket elolvasó matematikusokra maradt.