Amikor az MI bekapcsolódik a bizonyításokba
Az elmúlt években számítógépes programokat fejlesztettek, amelyek képesek matematikai érvelések ellenőrzésére. Ezek a szoftverek azonban csak akkor működnek, ha az ember által írt bizonyításokat előbb egy szigorú, formális programnyelvre fordítják le, amit formálisításnak neveznek. Egy-egy bizonyítás átírása ilyen, teljesen egzakt kódra hónapokig, de akár évekig is eltarthat. Amikor megjelentek az első nagy nyelvi modellek, sok matematikus reménykedett abban, hogy a gépek automatikusan is elvégezhetik ezt az időigényes átültetést. A formális nyelvek azonban eltérnek az emberi beszédtől: itt minden szónak, jelnek és hivatkozásnak pontos jelentése van, a legkisebb tétovaság sem fér bele.
Mégis, az MI-s fejlesztés felgyorsult: a Math, Inc. nevű startup kifejlesztett egy Gauss nevű MI-t, amely már sikeresen formalizált két bonyolult, magas dimenziós gömbpakolásról szóló bizonyítást, amelyeket Maryna Viazovska dolgozott ki. Az egyik bizonyításért Viazovska 2022-ben Fields-érmet kapott – ez a matematika legnagyobb elismerése. Bár maga a matematikus közösség visszafogottan fogadta az áttörést, hiszen a fejlesztési folyamat nem éppen úgy zajlott, ahogy sokan remélték, ennek ellenére a példa jelzi, milyen jövő vár a matematika és a gépi tanulás találkozására.
A gömbpakolás rejtélye
2016-ban Viazovska jelentős áttörést ért el a gömbpakolási probléma terén, vagyis hogy miként lehet gömböket a leghatékonyabban elhelyezni a térben. Az alapvető háromdimenziós variáció – a narancsokból épülő piramis – már 1998-ban bizonyítást nyert, de magasabb dimenzióban egyre összetettebbé vált a kérdés. Viazovska elegáns megoldást kínált nyolc- és huszonnégy-dimenziós térben: a háromdimenziós optimális pakolás eredményeinek átültetésével és megfelelő matematikai igazolásával bizonyítani tudta, hogy ezekben a speciális terekben mekkora hely marad, ahova pontosan egy további gömb illeszthető.
Az áttörést jelentő nyolcdimenziós bizonyítást Viazovska több kollégájával közösen valósította meg. 2023-ban találkozott Sidharth Hariharannal, aki éppen a Lean formális nyelvével kísérletezett, és mindketten abban látták a kihívást, hogy lefordítsák Viazovska bizonyításait teljes egészében Lean kóddá. Csapatuk munkája minden matematikai fogalmat és tételt átültetett, amit online is elérhetővé tettek a fejlesztéshez csatlakozók számára.
Startupok harca: hamarabb lép az MI
Eközben a svájci Math, Inc.-et egy fiatal matematikus, Auguste Poiroux indította azzal a céllal, hogy a publikációk vagy könyvek tartalmát automatikusan lehessen Lean kódra fordítani és rögtön ellenőrizni. A Math, Inc. figyelmét felkeltette Hariharanék projektje, és belevágtak abba, hogy saját MI-jükkel, a Gauss-szal formalizálják a bizonyítások részeit. Egy idő után azonban a fejlesztők befejezték az együttműködést, hogy minden erőt az MI továbbfejlesztésére fordítsanak.
Rövidesen eljött az áttörés: sikerült Gauss segítségével a nyolcdimenziós bizonyítást teljesen Lean kóddá és közel 120 000 soros, ellenőrzött formára átültetni, emberi beavatkozás nélkül. Ugyanakkor a projekt kidolgozója úgy érezte, hogy többéves munkájukat az MI váratlanul kisajátította, de tudomásul vette, hogy a technológia forradalmasítja a matematikai kutatást.
Az MI uralma a matematika felett
A Math, Inc. később a huszonnégy-dimenziós bizonyítással is próbát tett: ezúttal csak a tudományos cikket adták Gaussnak, amely végül teljes egészében átírta és ellenőrizte a bonyolult bizonyítást. Bár az autoformalizáció még nem képes lefedni a matematika minden területét, gyorsul a fejlődés. Az új MI-rendszerek nem egyszerű fordítógépek: a forráscikkek kisebb hibáit is képesek korrigálni, előrevetítve, hogy a jövőben talán minden matematikai publikációt ilyen szoftverek fognak ellenőrizni.
Amikor a modellek teljesen megértik a matematika összefüggéseit, talán már nemcsak ellenőrizni, hanem új felfedezéseket is tenni tudnak – olyan ugrásokra lesznek képesek, amelyek meghaladják az emberi képzeletet is. Az MI-vel való szimbiózis pedig új dimenzióba emelheti a tudomány fejlődését.
