MI Történik?

A Google DeepMind kutatói megalkották az AlphaGeometry-t, „egy tételbizonyítót az euklideszi síkgeometriához, amely megkerüli az emberi bemutatók szükségességét azáltal, hogy több millió tételt és bizonyítást szintetizál különböző összetettségi szinteken”. A tesztek során az AlphaGeometry 25 diákolimpiai szintű matematikai geometriai feladatot oldott meg, „túlteljesítve a korábbi legjobb módszert, amely csak tíz feladatot oldott meg, és megközelítve egy átlagos Nemzetközi Matematikai Diákolimpia (IMO) aranyérmes teljesítményét.” Ez azért nagy jelentőségű, mert az IMO-feladatok megoldása algoritmus-szintű mesterségbeli tudást és bizonyos fokú kreativitást is igényel. Az AlphaGeometry létrehozásához a kutatóknak egy hatalmas szintetikus adatkészletet kellett felépíteniük a nyelvi modell előtanításához. Ennek során a hagyományos szimbolikus motorokat párosították nyelvi modellekkel. Pontosabban, szimbolikus rendszerek segítségével emberi mennyiségű szintetikus tételt és bizonyítást generáltak, majd egy nyelvi modellt használtak a bizonyítások kiterjesztésére. „A generált bizonyítások tisztán olyan dedukciós lépésekből állnak, amelyeket a rendkívül hatékony DD + AR szimbolikus dedukciós motor már elér. A diákolimpiai szintű feladatok megoldásához azonban a legfontosabb hiányzó láncszem az új bizonyítási kifejezések generálása” – írják. „Magas szinten a bizonyításkeresés egy hurok, amelyben a nyelvi modell és a szimbolikus dedukciós motor felváltva fut.” A Google DeepMind ezután előtanított egy nyelvi modellt a fenti technikákkal generált nagyméretű szintetikus adatkészleten, majd finomhangolta azt a specifikus problémakörre, amelynek megoldására szánták (bár nem magukra a konkrét kérdésekre és válaszokra).