Az elmúlt hónapokban több, évtizedek óta nyitott matematikai probléma kapott állítólagos megoldást nagy nyelvi modellek (LLM-ek) munkájának köszönhetően. 2024 májusában egy belső OpenAI-modell ellenspéldát talált Erdős egységtávolság-tételére (állítás nyitva 1946 óta). Egy hónappal később OpenAI egy Cycle Double Cover (CDC) problémára vonatkozó bizonyítást publikált, majd júliusig további tíz nyitott problémára adtak megoldásokat, szeptemberben pedig Navier–Stokes-probléma bizonyítását közölték. Anthropic formálisan leírta Fermat nagy tételének formalizációját és előrehaladást tett a Riemann‑hipotézis határaival kapcsolatban. Ezek az esetek azt mutatják, hogy a modellek hirtelen jók lettek bizonyos típusú matematikai feladatokban.
Mi tesz egy problémát megoldhatónak egy LLM számára?
Egy egyszerű mentális modell szerint minden probléma megoldása egy sor felismerésből (insight) és a felismert irány kidolgozásához szükséges munkából áll: felismerés → munka → felismerés → munka → megoldás. Az, hogy egy feladat mennyire nehéz, az a legrövidebb olyan felismeréssor hosszával és a közöttük lévő fejlesztőmunka mennyiségével szemléltethető. Tim Gowers hasonló elképzelést használ: a nehézség a legrövidebb olyan „utasításlánc”, amely lehetővé tenné, hogy szakértők rekonstruálják a bizonyítást — egyfajta Kolmogorov-komplexitás, de szakértői háttérrel.
A komplexitás exponenciálisan nő a szükséges felismerések számával. A megoldások többsége a felismerések közti munkában rejlik: egy eureka-élmény után hónapok telhetnek el, míg a következő fogaskerék megjelenik. Ennek alapján a probléma korát, a próbálkozások számát vagy a felajánlott díjat gyakran használják nehézségmutatóként, de ezek csak közelítések.
Mitől értékes egy felismerés?
Egy felismerés általában megváltoztatja a feladat megfogalmazását és a problémáról alkotott reprezentációt. Két tényező határozza meg, mennyit ér egy insight:
- mennyire volt valószínűtlen előtte, és mennyire nyilvánvaló utána; és
- melyik helyen áll a felismeréssorban, mert egy későbbi insight csak akkor használható, ha az előzőek elég munkával előkészítették.
Ez megakadályozza a naiv brute‑force ötletet, hogy mindent kipróbálunk: a felismeréssor egy elágazó fát jár be, ahol az első lépések gyökeresen befolyásolják a következő lehetséges irányokat.
Az emberi kutatás mint szélességi keresés
Az emberek jellemzően szélességi (breadth-first) mintát követnek: sok lehetőséget generálnak, ezeket sekélyen felfedezik, a legtöbbet elvetik, és néhány ígéretessel elköteleződnek. Egy ígéretes irányt akkor hagynak el, ha a korai eredmények nem adnak elég visszajelzést, mert a kidolgozás hónapokat vehet igénybe. A kutatási szoftverek célja ezt az időt csökkenteni; az AI viszont sok esetben annyira le tudja rövidíteni az időigényt, hogy maga a keresési minta megfordul.
Modellek: időt cserélnek számítástechnikára
A modelleknél a felismerés utáni munka (t) a számítási erőforrásokban és a tokenekben jelenik meg, egy pályán költve vagy párhuzamos ügynökök között elosztva. A pretraining a szakirodalomhoz hasonló előismereteket ad, amiket egy embernek külön fel kellene kutatnia.
A nagy különbség a keresés módjában van: az LLM-ek mélységi (depth-first) keresést folytatnak. Adott prompttal egy modell sokszor egy teljes, talán helyesnek tűnő megoldást ad. CoT (chain‑of‑thought) lefutása is gyakran mohó, mélységi jellegű. Párhuzamos ügynökök esetén több, egymástól független irány kidolgozását kapjuk — mindegyik vagy elakad, vagy egy látszólag jó érvet ad.
Egyedül ez sok gyönyörű, de hamis bizonyításhoz vezethet. Azonban ha van egy automatikus ellenőrző (verifier), amely képes leszűrni a lezárt trajektóriákat és kiválasztani a helyeseket, akkor ésszerűvé válik óriási számítási erő befektetése akár bizonytalan ötletekbe: percek alatt megállapítható, hogy egy adott elképzelés működik‑e. A korlát az, hogy a verifier csak kész, lezárt érveket tud megítélni — nem ad iránymutatást arra, hogy egy félig kidolgozott ötlet jó úton van‑e.
A minőségi küszöb: ember vs. modell
Az embernél a felismerés minőségi küszöbe magas, mert egy rossz irány hónapok elvesztegetését jelentheti. A modell számára ez a küszöb gyakorlatilag eltűnik: a hint lehet gyenge, félkész vagy váratlan, mert könnyen követhető és gyorsan megvizsgálható, hogy eljut‑e valahová. Az LLM-ek lehetővé teszik, hogy időt számítástechnikára cseréljünk, és rövidebb idő alatt több problémát próbáljunk meg.
A sikertelen próbálkozások mint negatív hintek
A rendszer visszajelzéseit és a sikertelen megoldásokat visszaforgatják a modellbe mint negatív hinteket. Egy tipikus harness három elemből áll:
- Drafter: megírja a promptokat a solvernek, figyelembe veszi a modell priors‑ait és a korábbi hibákat.
- Solver: egy vagy több al‑ügynököt futtatva több jelölt megoldást dolgoz ki párhuzamosan.
- Verifier/Checker: eldönti, hogy az állítás helyes‑e és validálja az érvet.
A CDC‑bizonyításoknál például a drafter explicit módon kikötötte, hogy vegyük feltételezésnek a teljes, pozitív bizonyítás létezését, és kizárta a katalógusszerű, félmegoldásokat, valamint felsorolta a gyakori eltévedési módokat, amelyeket az ellenőrzésnek mindig vizsgálnia kell. Ezek valójában a korábbi sikertelen utak explicit listázásai — negatív hintek, amelyek a következő iterációt irányítják.
A unit-distance ellenspélda rekonstruálása a harness szemüvegén át
Tim Gowers három javaslata (keress ellenspéldát; általánosítsd a legjobb ismert konstrukciót; próbálj számmező‑sorozatokat növekvő fokszámmal és príidelétekkel) jól illeszthetők a fenti rendszerbe:
- A counterexample‑irány ritka a szakmai priors szerint, tehát a drafter valószínűleg úgy jutott el hozzá, hogy a solverk többször is elakadt a klasszikus bizonyítási irányban.
- A legjobb ismert konstrukció általánosítása tipikus közösségi lépés, de itt az volt a lényeg, hogy ez az általánosítás egy disproof‑irányt tett lehetővé.
- A számmezők növekvő fokszáma már standard technika, ha az előző lépések megadják a terepet, amin működhet.
Jacob Tsimerman (OpenAI) dolgozott az ellenspéldán; ismerte a számelméleti eszközöket, elgondolkodott a növekvő fokszámú mezőkön, majd leállt — nem képessége hiányzott, hanem az emberi pszichológia: hónapokig tartó „mocsárban” való elköteleződés bizonyíték nélkül nagy személyes és szakmai költséggel jár. A modellek ezzel szemben képesek „hosszabban játszani” kockázatos, kevés bizonyítékot adó vizeken anélkül, hogy morálisan vagy karrierügyileg érdekelt felek lennének.
Más bizonyítások, és mi változott a modelleken
OpenAI Navier–Stokes‑bizonyítása, a szerzői olvasat szerint, a Córdoba és Martínez‑Zoroa által megtett utat viszi tovább és fejezi be; a kézirat 166 oldalnyi javítással és komplex matematikával dolgozik. Anthropic Fermat‑ és Riemann‑munkái hasonló vázat mutatnak: sok száz sikertelen ötlet, több ügynök, szkriptek és checkerek, valamint néhány kulcsfogalom hozza a teljes terhet.
Három konkrét képesség változása különösen fontos:
- Az, hogy a modellek jobbak lettek a primitívek összefűzésében hosszú távú feladatokra (csökkenti a t munkát);
- A self‑verification képesség: a modellek egyes lépéseket képesek belsőleg is ellenőrizni, és hibákat kiszűrni még a verifier előtt (olcsóbbá teszi a prunálást a trajektória belsejében);
- Orchestration: a modellek tudnak al‑ügynököket irányítani, memóriát használni a steeringhez és a rossz utak kizárásához (így épülnek a negatív hintek).
Elágazási tényező (branching factor) és amikor a modellek jobbak
Gowers képlete hiányossága, hogy nem veszi figyelembe a lehetséges következő hintek számát b: ha minden lépésnél b lehetséges irány van, akkor k felismerés esetén b^k út van. Az emberek ízlése és ítélőképessége gyakran csökkenti az effektív b‑t; a modellek viszont sok lehetséges ágat képesek gyorsan végigjátszani. Ez azt jósolja, hogy a modellek jól teljesítenek ott, ahol b^k × compute‑költség alacsony — például ahol a köztes lépések elágazása kicsi, vagy ahol egy korai felismerés (például ellenspélda keresése) a megoldási teret erősen leszűkíti.
Ennek köszönhető, hogy a unit‑distance ellenspélya különösen hatásosnak bizonyult: a counterexample‑irány lerántotta az elágazási faktort. Hasonló okból esett gyorsan például a kiberbiztonság is, ahol a köztes elágazások száma viszonylag alacsony, és a megoldásformák előre ismertek.
Hol tarthatják meg az emberek az előnyt?
Az emberi előny valószínűleg ott marad, ahol a keresési fa mély és erősen elágazó: nagy b és/vagy nagy k mellett az emberi intuitív prunálás és ítélőképesség nélkül a számítás nem megvalósítható. Az ember jó abban, hogy beszűkítse az ágakat; a modell jó abban, hogy gyorsan leprunálja egy ágat végigkövetve. A két megközelítés komplementer lehet, de csak akkor, ha hozzáférünk a modellek sikertelen próbálkozásainak információjához — mert sok tudás a kudarcokban rejlik.
Terence Tao nézetére hivatkozva a bizonyítás önmagában nem cél: a matematikai megértés fejlesztése a cél. Ha csak a végső bizonyítást látjuk, de nem a miértet és a mi módonokat, akkor elveszítjük a közösségi tanulás sok részét.
Záró megjegyzés: mi történne, ha 1901‑ig tanítanánk egy modellt?
Végül a szerző röviden kitér egy gondolatkísérletre: ha egy modellt 1901‑ig terjedő adatokkal képeznénk, vajon előállna‑e a General Theory of Relativity? Az elképzelés szerint egy erős, meglepő felismerés — gravitás geometriai kezelésének gondolata — jelentősen leszűkítené a megoldási teret, és a nehéz algebrai munkát egy modell képes lenne elvégezni. A szerző szerint ez a próba gyors lehet, ha a kutatók ügyesen jóhardolják a tesztet: a modellnek csak néhány nagy felismerésre lenne szüksége, a maradék munka pedig a modell erőssége.
Összefoglalva: a mostani LLM‑sikerek oka a mélységi keresés, a számítás‑idő csere, a belső és külső ellenőrzések, valamint az orchestration, amelyek együtt lehetővé teszik, hogy a modellek sok gyenge felismerést kövessenek elölről végig, és gyorsan kiszűrjék a használhatatlanokat. Az emberek és a modellek erősségei komplementerek lehetnek: az emberi intuíció beszűkíti az ágakat, a modellek pedig olcsón és gyorsan végigpróbálnak sok utat, feltárva olyan megoldásokat is, amelyekhez egyedül a humán kutatás nem jutott volna el.
