OpenAI zbourala geometrickou domněnku? Technický pohled na to, co se doopravdy stalo
Zprávy hlásí, že model od OpenAI pomohl vyvrátit desítky let starý matematický problém. Než se ale začneme bavit o digitálních matematicích, je potřeba se podívat, co přesně se pod kapotou stalo. Realita je totiž o dost víc o architektuře a lidské verifikaci než o samostatném géniovi v křemíku.
Co se tvrdí a kde je háček
Internetem proběhla zpráva, že AI model, konkrétně upravená verze GPT, našel řešení, které vyvrací jednu z domněnek v diskrétní geometrii. Na první pohled to zní jako zlomový bod. Stroj, který samostatně provádí originální matematický objev. Jenže ono je to složitější.
Klíčové je slovo „pomohl“. Model totiž nevygeneroval finální, neprůstřelný důkaz, ale spíše sérii myšlenek a argumentů v přirozeném jazyce. Byli to až lidští matematici, kdo musel tento výstup vzít, ověřit ho a dotáhnout do konce. To na hodnotě objevu nic neubírá, ale mění to roli AI z „objevitele“ na extrémně výkonného „spoluautora“.
Formální důkaz versus nápad
Pro pochopení je nutné rozlišit mezi neformálním a formálním důkazem. Představte si to jako rozdíl mezi slovním popisem domu a detailním architektonickým plánem. Slovní popis vám dá představu, ale plán můžete strojově zkontrolovat na statické chyby. A přesně tak fungují formální systémy jako Lean nebo Coq.
AI model vyprodukoval ten slovní popis. Velmi dobrý, inspirativní popis, který nasměroval experty správným směrem. Nevygeneroval ale onen „architektonický plán“, který by prošel automatickou kontrolou. A to je zásadní. Současné velké jazykové modely totiž negenerují logiku, ale statisticky nejpravděpodobnější pokračování textu.
Architektura pro kreativitu, ne pro pravdu
Transformer, architektura v srdci většiny dnešních LLM, je geniální v nacházení vzorců v obrovských datasetech. Umožňuje modelu propojit zdánlivě nesouvisející koncepty a vytvořit tak originální myšlenku. To je přesně to, co se stalo tady – model našel cestu, kterou lidé přehlíželi.
Jeho slabinou je ale konzistence a logická přesnost. Model nechápe matematickou pravdu. Chápe jen strukturu textů o matematice. Proto je jeho výstup potřeba brát jako hypotézu, ne jako axiom. Práce na propojení LLM s formálními verifikátory sice běží, ale jsme teprve na začátku.
Výsledek tedy není o tom, že by AI nahradila matematiky. Ukazuje ale, že se stává nástrojem, který dokáže prohledávat obrovské prostory možných řešení a přicházet s nápady, které jsou mimo lidskou intuici. Skutečným cílem teď není vytvořit AI matematika, ale systém, kde kreativní síla LLM a rigorózní přesnost formálních metod spolupracují.