Google áttörést jelent be a matematika terén az új bizonyításmegoldó AI modellekkel!

Google DeepMind mesterséges intelligenciája ezüstérmet szerzett a Nemzetközi Matematikai Olimpián

Csütörtökön a Google DeepMind bejelentette, hogy az AlphaProof és AlphaGeometry 2 nevű MI rendszerei megoldottak négyet az idei Nemzetközi Matematikai Olimpia (IMO) hat problémájából, ezáltal ezüstérmet szerezve. A tech óriás szerint ez az első alkalom, hogy egy MI ilyen szintű teljesítményt ért el a rangos matematikai versenyen, bár az állítások nem mindig egyértelműek.

A Google szerint az AlphaProof megerősítéses tanulást alkalmaz, hogy matematikai állításokat bizonyítson a Lean nevű formális nyelven. A rendszer saját magát képezi azáltal, hogy milliónyi bizonyítást generál és ellenőriz, fokozatosan egyre nehezebb problémákat megoldva. Eközben az AlphaGeometry 2 a Google korábbi geometriai megoldó MI modelljének továbbfejlesztett változata, amely most egy Gemini-alapú nyelvi modellel működik, és jelentősen több adatot tanítottak meg rá.

A Google szerint Sir Timothy Gowers és Dr. Joseph Myers prominens matematikusok értékelték az MI modell megoldásait az IMO hivatalos szabályai szerint. A vállalat jelentése szerint a kombinált rendszer 28 pontot szerzett a lehetséges 42-ből, éppen elmaradva a 29 pontos aranyérmes küszöbtől. Ebben benne volt a verseny legnehezebb problémájának tökéletes megoldása is, amelyet a Google állítása szerint idén csak öt emberi versenyző oldott meg.

Olyan matematikai verseny, mint egyetlen másik

Az 1959 óta évente megrendezett IMO elit középiskolás matematikusokat állít szembe kivételesen nehéz algebrai, kombinatorikai, geometriai és számelméleti problémákkal. Az IMO problémáinak megoldása elismert mércévé vált az MI rendszerek matematikai érvelési képességeinek értékelésére.

A Google állítása szerint az AlphaProof két algebrai problémát és egy számelméleti problémát oldott meg, míg az AlphaGeometry 2 a geometriai kérdést. Az MI modell állítólag nem tudta megoldani a két kombinatorikai problémát. A vállalat szerint rendszereik egy problémát percek alatt oldottak meg, míg mások megoldása akár három napot is igénybe vett.

A Google elmondása szerint először lefordították az IMO problémákat formális matematikai nyelvre, hogy MI modelljük feldolgozhassa. Ez a lépés eltér a hivatalos versenytől, ahol az emberi versenyzők közvetlenül a problémaállításokkal dolgoznak két 4,5 órás ülés során.

A Google jelentése szerint az AlphaGeometry 2 az idei verseny előtt az elmúlt 25 év történelmi IMO geometriai problémáinak 83 százalékát tudta megoldani, szemben elődje 53 százalékos sikerességi rátájával. A vállalat állítása szerint az új rendszer az idei geometriai problémát 19 másodperc alatt oldotta meg a formális változat kézhezvétele után.

Korlátok

A Google állításai ellenére Sir Timothy Gowers árnyaltabb perspektívát kínált a Google DeepMind modellekről egy X-en közzétett bejegyzésben. Miközben elismerte az eredményt mint „jóval túlmutatót azon, amit a korábbi automatikus tételbizonyítók elértek,” Gowers több fontos feltételt is kiemelt.

„A fő feltétel az, hogy a program sokkal hosszabb időre volt szüksége, mint az emberi versenyzőknek—néhány probléma megoldásához több mint 60 órára—és természetesen sokkal gyorsabb feldolgozási sebességre, mint a szegény emberi agy,” írta Gowers. „Ha az emberi versenyzőknek ennyi időt engedtek volna problémánként, kétségtelenül magasabb pontszámot értek volna el.”

Gowers azt is megjegyezte, hogy emberek fordították le a problémákat a Lean formális nyelvre, mielőtt az MI modell elkezdte volna munkáját. Hangsúlyozta, hogy bár az MI végezte a lényegi matematikai érvelést, ezt az „autoformalizálási” lépést emberek végezték el.

A matematikai kutatásra gyakorolt szélesebb körű hatásokkal kapcsolatban Gowers bizonytalanságot fejezett ki. „Közel vagyunk ahhoz, hogy a matematikusok feleslegesekké váljanak? Nehéz megmondani. Azt tippelném, hogy még egy-két áttörésre van szükségünk ehhez,” írta. Szerinte a rendszer hosszú feldolgozási ideje azt jelzi, hogy még nem „oldotta meg a matematikát”, de elismerte, hogy „van valami érdekes, amit a működése során látunk.”

Gowers spekulált arról is, hogy az ilyen MI rendszerek értékes kutatási eszközökké válhatnak. „Tehát lehet, hogy közel vagyunk egy olyan programhoz, amely lehetővé teszi a matematikusok számára, hogy választ kapjanak számos kérdésre, feltéve, hogy ezek a kérdések nem túl bonyolultak—olyan dolgok, amelyeket pár órán belül meg lehet oldani. Ez hatalmas segítség lenne kutatási eszközként, még ha önmagában nem is képes nyitott problémákat megoldani.”

Érdekesség: A Google DeepMind által használt AlphaZero MI rendszer, amely sakk és go játékokban is kiválóan teljesít, mindössze néhány óra alatt sajátította el a sakk szabályait és vált világszinten verhetetlenné.

Források: Google DeepMind, Sir Timothy Gowers bejegyzései X-en