Miután a Google DeepMind mindenben legyőzte az embereket Játssz Ugrás a stratégiai társasjátékokhoz,
most azt állítja, hogy a világ legjobb diákjait legyőzi a matematikai feladatok megoldásában.

A londoni székhelyű Gépi tanulás A cég július 25-én jelentette be, hogy mesterséges intelligencia (AI) rendszerei a 2024-es Nemzetközi Matematikai Olimpián (IMO) az egyesült királyságbeli Bathban tanuló diákoknak adott hat feladat közül négyet megoldottak. A mesterséges intelligencia szigorú, lépésről lépésre végzett bizonyítékokat szolgáltatott, amelyeket két kiváló matematikus értékelt, és 28/42-es pontszámot ért el – ez mindössze egy pont az aranyérem területéhez képest.

„Ez nyilvánvalóan nagyon jelentős előrelépés” – mondja Joseph Myers, az Egyesült Királyságbeli Cambridge-i matematikus, aki a Fields-érmes Tim Gowers-szel együtt áttekintette a megoldásokat, és segített kiválasztani az eredeti problémákat az idei IMO számára.

A DeepMind és más cégek versenyben állnak, hogy végül a gépeket olyan bizonyítékokkal szolgáltassák, amelyek számítanak Kutatási kérdések megoldása matematikából. Az IMO-n, a fiatal matematikusok számára rendezett világelső versenyen bemutatott problémák a cél elérése felé tett előrehaladás mércéjévé váltak, és „nagy kihívásnak” tekintik a gépi tanulás számára – közölte a vállalat.

„Ez az első alkalom, hogy egy mesterséges intelligencia rendszer érem szintű teljesítményt ér el” – mondta Pushmeet Kohli, a DeepMind tudományos AI-ért felelős alelnöke egy sajtótájékoztatón. "Ez egy fontos mérföldkő a fejlett bizonyítékok nyomozóinak felépítésében" - mondta Kohli.

Kiterjesztés

Alig néhány hónapja, januárban a DeepMind rendszer AlphaGeometry érem szintű eredmények egyfajta IMO-probléma megoldásában ért el, nevezetesen az euklideszi geometriában. Az első mesterséges intelligencia, aki aranyérmes szinten teljesít az átfogó teszten – beleértve az algebrai, kombinatorikai és számelméleti kérdéseket, amelyeket általában nagyobb kihívásnak tartanak, mint a geometriát –, 5 millió dolláros díjat, az AI matematikai olimpiai díjat (AIMO) kaphat. (A díjra szigorú kritériumok vonatkoznak, mint például a forráskód közzététele és a korlátozott számítási teljesítménnyel való munka, ami azt jelenti, hogy a DeepMind jelenlegi erőfeszítései nem minősülnek jogosultnak.)

Legutóbbi kísérletükben a kutatók az AlphaGeometry2 segítségével 20 másodperc alatt megoldották a geometriai problémát; a mesterséges intelligencia a rekordrendszerük továbbfejlesztett és gyorsabb változata, mondja a DeepMind számítógépes specialistája, Thang Luong.

A többi kérdéstípushoz a csapat egy teljesen új rendszert fejlesztett ki AlphaProof néven. Az AlphaProof két algebrai feladatot oldott meg a versenyen és egy számelméletben, ami három napig tartott. (A tényleges IMO résztvevőinek két, egyenként 4,5 órás ülésük van.) Nem tudta megoldani a két feladatot a kombinatorikában, a matematika másik területén.


Nahaufnahme einer Goldmedaille, gewonnen bei der 63. Internationalen Mathematik-Olympiade von einem rumänischen Teilnehmer.

A kutatók vegyes eredményeket értek el, amikor matematikai kérdéseket válaszoltak meg nyelvi modellekkel – olyan rendszerekkel, amelyek a chatbotokat, például a ChatGPT-t működtetik. Néha a modellek adják a helyes választ, de nem tudják racionálisan megmagyarázni érvelésüket, néha pedig hülyeségeket röhögnek.

Csak a múlt héten a Numina és a HuggingFace szoftvercégek kutatói egy nyelvi modell segítségével megnyerték az IMO-problémák egyszerűsített változatain alapuló köztes AMIO „fejlődési díjat”. A vállalatok teljes rendszerüket nyílt forráskódúvá tették, és elérhetővé tették más kutatók számára, hogy letölthessék. De a győztesek azt mondtákTermészet, hogy a nyelvi modellek önmagukban valószínűleg nem lennének elegendőek a nehezebb problémák megoldására.

Csak osztály

Az AlphaProof egy nyelvi modellt egyesít egy megerősítő tanulási technológiával, amely az „AlphaZero” motort használja, amelyet a vállalat sikeresen használt olyan támadójátékokhoz, mint a Go és néhány konkrét matematikai problémák használt. A megerősítő tanulás során a neurális hálózat próba és hiba útján tanul. Ez akkor működik jól, ha a válaszai objektív mércével értékelhetők. Ebből a célból az AlphaProofot arra képezték ki, hogy a Lean nevű formális nyelven bizonyítást olvasson és írjon, amelyet a matematikusok körében népszerű, azonos nevű „Proof Assistant” szoftvercsomagban használnak. Ehhez az AlphaProof a Lean csomagban futtatva tesztelte, hogy a kimenetei helyesek-e, ami segített a kód egyes lépéseinek kitöltésében.

A nyelvi modell betanítása hatalmas mennyiségű adatot igényel, de a Leanben kevés matematikai bizonyíték állt rendelkezésre. Ennek a problémának a leküzdésére a csapat egy további hálózatot fejlesztett ki, amely megkísérelte lean nyelvre lefordítani a természetes nyelven írt, de ember által írt megoldások nélküli, millió probléma létező rekordját – mondja Thomas Hubert, a DeepMind gépi tanulással foglalkozó kutatója, az AlphaProof fejlesztésének egyik vezetője. „Az volt a megközelítésünk, hogy megtanulhatunk-e bizonyítani akkor is, ha eredetileg nem az ember által írt bizonyításokon tanultunk?” (A cég hasonló megközelítést alkalmazott a Go-hoz, ahol a mesterséges intelligencia úgy tanulta meg a játékot, hogy önmaga ellen játszik, nem pedig abból, ahogyan az emberek csinálják.)

Mágikus kulcsok

A Lean fordítások közül sok nem volt értelmes, de elég jó volt ahhoz, hogy az AlphaProof arra a pontra jusson, ahol elkezdhette megerősítő tanulási ciklusait. Az eredmények a vártnál sokkal jobbak voltak – mondta Gowers a sajtótájékoztatón. "Az IMO-nál sok probléma rendelkezik ezzel a varázskulcs-tulajdonsággal. A probléma először nehéznek tűnik, amíg nem talál egy varázskulcsot, amely kinyitja" - mondta Gowers, aki a párizsi Collège de France-ban dolgozik.

Egyes esetekben úgy tűnt, hogy az AlphaProof képes biztosítani a kreativitás további lépését azáltal, hogy egy végtelenül nagy lehetséges megoldásból egy helyes lépést biztosít. De további elemzésre van szükség annak megállapítására, hogy a válaszok kevésbé voltak-e meglepőek, mint amilyennek látszott – tette hozzá Gowers. Hasonló diskurzus alakult ki a meglepő után "37-es vonat", a DeepMinds AlphaGo bot az övénél híres 2016-os győzelem a világ legjobb emberi Go játékosa felett tett – fordulópont az AI számára.

Hogy a technikák tökéletesíthetők-e a matematika kutatási szintjére, az még várat magára, mondta Myers a sajtótájékoztatón. „Kiterjedhet-e más matematikai típusokra is, amelyekre esetleg nincs több millió probléma kiképezve?”

"Ott tartunk, ahol nemcsak nyitott kutatási problémákat tudnak bizonyítani, hanem olyan problémákat is, amelyek nagy kihívást jelentenek a világ legjobb fiatal matematikusai számára" - mondta David Silver, a DeepMind számítástechnikai specialistája, aki a 2010-es évek közepén az AlphaGo fejlesztésének vezető kutatója volt.