Mi fán terem a SAT?
A SAT (kielégíthetőségi) probléma az MI egyik alapvető eleme, bár gyökeresen más irányból közelíti meg a mesterséges intelligencia fogalmát, mint a ChatGPT vagy a képgenerátorok. A SAT szimbolikus MI, vagyis régi vágású, szabályalapú intelligencia, amely eldöntendő állításokra épül: ezek mindössze két értéket vehetnek fel, igazat vagy hamisat, amelyeket szigorú logikai láncok kötnek össze. Ha egy kérdést ilyen alapállításokra lehet bontani, akkor a SAT-programok gyakran képesek hibátlan és zárt levezetést adni: ezt nevezzük automatikus bizonyításnak. Az ilyen bizonyítások néha több ezer vagy akár millió lépésből állnak, de logikailag kifogástalanok.
Lényeges hangsúlyozni, hogy Heule sikere abban rejlik, hogyan tudja a matematikai problémákat „jól” átállítani, hogy a SAT-eszközök ráharapjanak. Gyerekkorától vonzódik a rejtvénylogikához, első százdarabos kirakóját már egyévesen megoldotta – és a Delft Műszaki Egyetemen, majd számítástechnikai doktori tanulmányaiban tovább tökéletesítette ezt a gondolkodásmódot. Tudományos pályájának egyik sarkköve a kérdés: miként lehet a gondolkodást automatizálni? Tapasztalatai szerint a gépi bizonyítás sosem pontosan úgy működik, mint az emberi logika, hanem teljesen más szemléletmód kell hozzá.
Puzzle vagy számítás?
A SAT-feladat egy adott probléma bináris, azaz csak 0-t vagy 1-et tartalmazó állításokra való fordításából áll. Képzelj el egy óriási sudoku táblát, ahol minden négyzetbe csak 0 vagy 1 kerülhet, és adottak a szabályok is: minden sorban és oszlopban milyen eloszlásnak kell teljesülnie. Nem könnyű, de hihetetlenül erős problémákat lehet ezzel a módszerrel kezelni – legyen szó hardverellenőrzésről, szoftverellenőrzésről, munkaidő-beosztásról vagy akár absztrakt matematikai fejtörőkről.
Holott elsőre úgy hangzik, mintha sima bináris számításról lenne szó, a SAT megközelítése teljesen eltér a hagyományos programozástól. Míg a hagyományos szoftverek műveleteket hajtanak végre kiinduló adatokon, a SAT-algoritmusok lehetséges kombinációkat kutatnak fel: kizárják azt, ami nem működik, logikai ugrásokkal szűkítik a lehetőségeket, míg meg nem találják a kielégítő megoldást, vagy rá nem jönnek, hogy nincs ilyen.
Mit adhat az MI a SAT mellé?
Heule egyik fő tudománya, hogy ösztönösen ráérez a megfelelő problémareprezentációra – hogyan lehet úgy kódolni egy matematikai kérdést, hogy a SAT-program a legnagyobb erejét mutassa meg. Az igazi áttörés akkor várható, ha ezek az átváltások maguktól is, automatikusan történhetnek: vagyis ne kelljen minden alkalommal egy „kódoló zsenit” közbeiktatni. Ha a nagy nyelvi modelleket (LLM-eket) számos jó példával tanítják be ilyen átváltásokra, akkor messze a legtöbb felhasználónál jobb SAT-kódolásokat tudnak létrehozni. A legnagyobb kihívás ilyenkor annak ellenőrzése, hogy tényleg helyes-e a fordítás.
A matematikai folyamat megújulása
Lényeges hangsúlyozni, hogy a generatív MI rengeteg hihető segédtételt (lemmát) tud alkotni, ám ezek helyességét csak automatikus eszközök tudják ténylegesen ellenőrizni. Ha valami mégsem stimmel, a SAT-program konkrét ellenpéldát tud visszaadni – lehetőleg a legegyszerűbbet, ami azonnal megvilágítja a bukást. Ezek az ellenpéldák segítik az MI-t, hogy már legközelebb pontosabban találja el, mit javasoljon.
Ehhez társulhatnak a bizonyításellenőrző rendszerek, például a Lean, amely minden részletet, minden kapcsolódást leellenőriz. Így az MI szervezi a főbb lépéseket, az automatizált bizonyítás mindent átnéz, a Lean pedig azt ellenőrzi, hogy tényleg egy összefüggő egészet alkotnak a mozaikdarabok. Amíg a rendszer végig hitelesen működik, addig bátran lehet rá építeni, és tovább haladni.
Bizalom kontra érthetőség
Az automatizált bizonyítások gyakran olyan hosszúak és komplexek, hogy ember számára átláthatatlanok. Kritikusai ki is emelik: valódi értelmet veszít, ha nem fogja fel senki, mi történik. De Heule szerint az érthetőség túlértékelt, a bizalom pedig alulértékelt a matematikában. Nincs olyan élő matematikus, aki mindent átlát – de ha minden kis részletről megbízható számítógép-ellenőrzés mondja ki, hogy helyes, akkor már van mire alapozni a következő felfedezéseket. Összességében elmondható, hogy a gépi bizonyítás épp az emberi munka megbízhatóságán javíthat drámaian.
Mi marad az emberi matematikusnak?
Bár a SAT-programok a bizonyítás kulcslépéseit elvégzik, az emberi kreatív ráérzés, a konceptuális megközelítés továbbra is pótolhatatlan. A gépek egyedül nem érnek semmit, ha nincsenek olyan emberek, akik a problémát jól átlátják, új kereteket találnak, és a saját intuíciójukat átadják a rendszernek. Az MI, az automatizált bizonyítások és a matematikusok csak együtt képesek az igazán nagy áttörésekre. A varázslat az együttműködésben rejlik.
