Umělá inteligence na Mezinárodní matematické olympiádě: Jak AlphaProof a AlphaGeometry 2 dosáhly standardu stříbrné medaile

Matematické myšlení je vitální aspekt lidských kognitivních schopností, který pohání pokrok ve vědeckých objevích a technologických vývojích. Při snaze vyvinout umělou obecnou inteligenci, která se rovná lidskému myšlení, je nezbytné vybavit umělou inteligenci pokročilými matematickými rozumovými schopnostmi. Zatímco současné systémy umělé inteligence mohou zvládnout základní matematické problémy, zápasí s komplexním myšlením potřebným pro pokročilé matematické disciplíny, jako je algebra a geometrie. Nicméně, tato situace se může měnit, protože Google DeepMind učinil významné pokroky v rozvoji matematického myšlení umělých inteligencí. Tento průlom byl učiněn na Mezinárodní matematické olympiádě (IMO) 2024. Založena v roce 1959, IMO je nejstarší a nejprestižnější matematická soutěž, která vyzývá studenty středních škol z celého světa, aby řešili problémy z algebry, kombinatoriky, geometrie a teorie čísel. Každý rok týmy mladých matematiků soutěží, aby vyřešily šest velmi náročných problémů. Letos Google DeepMind představil dva systémy umělé inteligence: AlphaProof, který se zaměřuje na formální matematické myšlení, a AlphaGeometry 2, který se specializuje na řešení geometrických problémů. Tyto systémy umělé inteligence vyřešily čtyři z šesti problémů, dosáhnuvší tak úrovně stříbrné medaile. V tomto článku prozkoumáme, jak tyto systémy fungují při řešení matematických problémů.

AlphaProof: Kombinace umělé inteligence a formálního jazyka pro matematické důkazy

AlphaProof je systém umělé inteligence navržen pro důkazy matematických tvrzení pomocí formálního jazyka Lean. Integruje Gemini, předem trénovaný jazykový model, s AlphaZero, algoritmem učení s posilováním, který je proslulý tím, že zvládl šachy, šógi a Go.

Gemini model překládá přirozené jazykové problémové výpovědi do formálních, vytvářející tak knihovnu problémů s různou úrovní obtížnosti. To slouží dvěma účelům: převodu nepřesného přirozeného jazyka do přesného formálního jazyka pro ověření matematických důkazů a využití předpovědních schopností Gemini pro generování seznamu možných řešení s přesností formálního jazyka.

Když AlphaProof narazí na problém, generuje potenciální řešení a hledá důkazové kroky v Lean, aby je ověřil nebo vyvrátil. To je vlastně neuro-symbolický přístup, kde neuronová síť, Gemini, překládá přirozené jazykové instrukce do symbolického formálního jazyka Lean, aby prokázal nebo vyvrátil tvrzení. Podobně jako mechanismus AlphaZero, kde systém učí sám sebe hraním her proti sobě, AlphaProof se učí pokusem o důkazy matematických tvrzení. Každý pokus o důkaz rafinuje jazykový model AlphaProof, s úspěšnými důkazy, které posilují schopnost modelu zvládnout ještě náročnější problémy.

Pro Mezinárodní matematickou olympiádu (IMO) byl AlphaProof trénován důkazy nebo vyvrácením milionů problémů pokrývajících různé úrovně obtížnosti a matematické téma. Tento trénink pokračoval během soutěže, kde AlphaProof rafinoval svá řešení, dokud nenalezl kompletní odpovědi na problémy.

AlphaGeometry 2: Integrace LLM a symbolické umělé inteligence pro řešení geometrických problémů

AlphaGeometry 2 je nejnovější iterace série AlphaGeometry, navržené pro řešení geometrických problémů s vylepšenou přesností a efektivitou. Navazuje na základy svého předchůdce, AlphaGeometry 2 využívá neuro-symbolický přístup, který spojuje neuronové velké jazykové modely (LLM) se symbolickou umělou inteligencí. Tato integrace kombinuje pravidlovou logiku s předpovědní schopností neuronových sítí pro identifikaci pomocných bodů, které jsou nezbytné pro řešení geometrických problémů. LLM v AlphaGeometry předpovídá nové geometrické konstrukce, zatímco symbolická umělá inteligence aplikuje formální logiku pro generování důkazů.

Když je AlphaGeometry konfrontován s geometrickým problémem, jeho LLM vyhodnocuje řadu možností, předpovídající konstrukce, které jsou klíčové pro řešení problému. Tyto předpovědi slouží jako cenné nápovědy, směrující symbolický motor k přesným dedukcím a blížící se k řešení. Tento inovativní přístup umožňuje AlphaGeometry řešit komplexní geometrické výzvy, které sahají za konvenční scénáře.

Jedním z hlavních vylepšení v AlphaGeometry 2 je integrace modelu Gemini LLM. Tento model je trénován od začátku na výrazně více syntetických datech než jeho předchůdce. Tento rozsáhlý trénink umožňuje mu zvládnout ještě náročnější geometrické problémy, včetně těch, které zahrnují pohyb objektů a rovnice úhlů, poměrů nebo vzdáleností. Kromě toho AlphaGeometry 2 disponuje symbolickým motorem, který funguje dvakrát rychleji, umožňujícím mu prozkoumat alternativní řešení s bezprecedentní rychlostí. Tyto pokroky činí z AlphaGeometry 2 mocný nástroj pro řešení složitých geometrických problémů, stanovující nový standard v oboru.

AlphaProof a AlphaGeometry 2 na IMO

Letos na Mezinárodní matematické olympiádě (IMO) byli účastníci testováni šesti rozmanitými problémy: dvěma z algebry, jedním z teorie čísel, jedním z geometrie a dvěma z kombinatoriky. Výzkumníci z Google přeložili tyto problémy do formálního matematického jazyka pro AlphaProof a AlphaGeometry 2. AlphaProof řešil dva algebraické problémy a jeden problém z teorie čísel, včetně nejobtížnějšího problému soutěže, který vyřešilo pouze pět lidských soutěžících letos. Zatímco AlphaGeometry 2 úspěšně vyřešil geometrický problém, ale nezvládl dvě kombinatorické výzvy.

Každý problém na IMO je hodnocen sedmi body, což činí maximální možný počet 42 bodů. AlphaProof a AlphaGeometry 2 získaly 28 bodů, dosáhnuvší tak perfektní skóre na problémech, které vyřešily. To je umístilo na vyšší úrovni kategorie stříbrné medaile. Práh pro zlatou medaili letos byl 29 bodů, kterého dosáhlo 58 ze 609 soutěžících.

Další skok: Přirozený jazyk pro matematické výzvy

AlphaProof a AlphaGeometry 2 prokázaly působivé pokroky v schopnostech umělé inteligence při řešení matematických problémů. Nicméně, tyto systémy stále závisí na lidských odbornících pro překlad matematických problémů do formálního jazyka pro zpracování. Kromě toho není jasné, jak tyto specializované matematické dovednosti mohou být začleněny do jiných systémů umělé inteligence, jako je prozkoumání hypotéz, testování inovativních řešení dlouhodobých problémů a efektivní správa časově náročných aspektů důkazů.

Aby se tyto omezení překonala, výzkumníci z Google vyvíjejí systém přirozeného jazykového myšlení založený na Gemini a jejich nejnovějším výzkumu. Tento nový systém má za cíl posunout schopnosti řešení problémů bez požadavku na překlad do formálního jazyka a je navržen tak, aby se hladce integroval s jinými systémy umělé inteligence.

Závěrečné shrnutí

Výkon AlphaProof a AlphaGeometry 2 na Mezinárodní matematické olympiádě je významným pokrokem ve schopnostech umělé inteligence při řešení komplexního matematického myšlení. Obě systémy prokázaly výkon na úrovni stříbrné medaile, řešíce čtyři z šesti náročných problémů, a prokázaly významné pokroky ve formálním důkazu a řešení geometrických problémů. Přes jejich úspěchy, tyto systémy umělé inteligence stále závisí na lidském vstupu pro překlad problémů do formálního jazyka a čelí výzvám integrace s jinými systémy umělé inteligence. Budoucí výzkum se zaměřuje na další vylepšení těchto systémů, potenciálně začleněním přirozeného jazykového myšlení, aby se rozšířily jejich schopnosti napříč širším spektrem matematických výzev.