Egy matematikai válasz még nem jelenti a matematika megoldását

Az OpenAI eredménye új kérdéseket vetett fel

Az OpenAI szeptember 8-án jelentette be, hogy mesterséges intelligenciával megoldást készített a Navier, Stokes-féle létezési és simasági problémára. Ez a kérdés a hét Millennium-díjas probléma egyike. A bejelentés nyomán vita bontakozott ki arról, hogy milyen szerepet játszottak az emberek és a gépek, illetve kit illet az eredmény elismerése.

A fejleményt többen korábbi, ember és gép közötti mérföldkövekhez hasonlították. Tristan Buckmaster, a Navier, Stokes-ügyben érintett matematikusok egyike úgy fogalmazott: „Ez egy Deep Blue és Kaszparov-pillanat.” A felvetés természetesen továbbvezetett: ha az AI a matematika élvonalában is képes válaszokat adni, akkor a tudományág a sakkhoz és a góhoz hasonlóan „megoldhatóvá” válik-e.

A Princeton CITP Freedom to Tinker oldalán megjelent írás szerzői, Silvia De Toffoli és Eamon Duede szerint ez a megközelítés két, első látásra hihető feltételezésre épül. Az egyik, hogy az AI valóban megoldott egy matematikai problémát. A másik, hogy a matematika kizárólag problémák megoldásáról szól. A szerzők szerint egyik állítás sem helytálló.

A formális bizonyítás és a matematikai megértés különválhat

Az OpenAI a szerzők szerint két anyagot készített. Az egyik egy Lean-formalizáció, amely a helyességet tanúsítja, a másik pedig egy kézirat, amely látszólag a hozzá tartozó informális bizonyítást tartalmazza. A Lean-formalizáció fontos hozzájárulás, mert a logikai bizonyítás követelményeinek megfelelve bizonyosságot adhat az eredményről.

A matematikusok azonban ennél többet várnak egy bizonyítástól. Azt is szeretnék érteni, mi tesz igazzá egy állítást. Az érthető bizonyítás olyan matematikai ötleteket közvetít, amelyeket a kutatók felfoghatnak, megoszthatnak más szakértőkkel, összekapcsolhatnak a meglévő tudással, majd további munkában használhatnak fel.

A szerzők ezt a két elvárást logikai és érthető bizonyításnak nevezik. Hagyományosan ezek többnyire együtt jártak, mivel egy matematikusnak a bonyolult logikai levezetés elkészítése előtt meg kellett ragadnia a tétel mögötti, megosztható fő gondolatokat. Az AI azonban olyan formális bizonyításokat is előállíthat, amelyek elszakadnak az érthető matematikai érveléstől.

Az írás szerint ennek az ellenkezője is problémát okoz. Egy nagy horderejű ötlet önmagában nem bizonyítja, hogy az eredmény igaz. A valódi matematikai megoldásnak ezért egyszerre kell logikailag helyesnek és érthetőnek lennie. A Clay Mathematics Institute magyarázata szerint a bizonyítás nemcsak bizonyosságot, hanem megértést is ad.

A matematika nem ugyanaz a játék, mint a sakk vagy a gó

A szerzők szerint még az sem jelentené a matematika „megoldását”, ha a jövőbeli AI-rendszerek teljesen ellenőrzött és a matematikusok számára érthető bizonyításokat készítenének. A sakkban és a góban ugyanis meghatározott győzelmi feltételek vannak, a matematika esetében viszont nincs megfelelője a mattnak vagy a győzelemnek.

A matematikusok valóban versenyezhetnek egymással hírnévért, díjakért, állásokért és az elismerésért, de maga a matematika nem ellenséges játék, amelyben végső győztes születik. A tudományterülethez új fogalmak és elméletek kidolgozása, új kérdések felvetése és megválaszolása, különböző területek összekapcsolása, valamint a tudományos közösségek fenntartása is hozzátartozik. A szerzők szerint a matematikai munkát a szépsége és mélysége miatt is értékelik.

Ebben a keretben az AI-t természetesebb asszisztensként kezelni, mint versenytársként. A cikk Jeremy Avigad gondolatát idézi, amely szerint az AI technológia, amelyet az emberi célok szolgálatára terveztek. A Navier, Stokes-eredmény így fontos fejlemény lehet, de a szerzők szerint jelenleg nem világos, hogy az OpenAI egy termékeny, a matematika számára hasznosítható megoldást adott-e, vagy egyelőre csak választ a feltett kérdésre.