Zdroj: Freepik
Umelá inteligencia môže čoskoro produkovať stovky matematických dôkazov, ktoré budú vyzerať úplne správne, no budú obsahovať skryté chyby. Alebo budú také zložité, že ich ľudia nedokážu overiť. Ako potom zistíme, či sú naozaj pravdivé?
Na tajnom stretnutí v roku 2025 sa skupina popredných svetových matematikov zišla, aby otestovala nový jazykový model OpenAI s názvom o4-mini.
Účastníkov prekvapilo, ako presvedčivo model znel pri prezentovaní zložitého dôkazu, takmer ako skutočný matematik.
„Nikdy som pri modeloch nevidel takýto typ uvažovania,“ povedal vtedy Ken Ono, profesor teórie čísel na Univerzite vo Virgínii. „Takto pracuje vedec.“
Otázka však znie: nedostala umelá inteligencia viac uznania, než si zaslúži? A nehrozí, že začneme prijímať dôkazy vytvorené AI bez toho, aby sme im skutočne rozumeli?
Ono sám pripustil, že model môže ponúkať presvedčivé, no potenciálne nesprávne odpovede.
„Ak niečo poviete s dostatočnou autoritou, ľudia sa jednoducho zľaknú,“ povedal. „Myslím si, že o4-mini zvládol dôkaz zastrašovaním, všetko hovorí s obrovskou sebadôverou.“
V minulosti bola sebadôvera dobrým signálom. Iba najlepší matematici dokázali formulovať presvedčivé argumenty a ich uvažovanie bolo spravidla správne. To sa však zmenilo.
„Ak ste boli zlý matematik, boli ste aj zlý autor, zdôrazňovali ste nesprávne veci,“ povedal pre Live Science Terry Tao z UCLA, držiteľ Fieldsovej medaily z roku 2006. „AI však tento signál narušila.“
Matematici sa preto obávajú, že ich umelá inteligencia môže zahltiť dôkazmi, ktoré budú vyzerať prísne a logicky. No budú obsahovať ťažko odhaliteľné chyby.
Tao varuje, že takéto argumenty môžu byť prijaté práve preto, že pôsobia rigorózne.
„AI je, žiaľ, oveľa lepšia v tom, aby znela presvedčivo, než v tom, aby mala pravdu, či už správnu alebo nesprávnu,“ povedal. „Vždy bude pôsobiť presvedčivo.“
Preto vyzýva na opatrnosť pri prijímaní AI „dôkazov“. „Jedna vec, ktorú sme sa naučili, je, že ak im dáte cieľ, budú podvádzať ako o život, aby ho dosiahli.“
Hoci sa môže zdať, že ide o abstraktnú debatu, dôsledky sú veľmi reálne. Ak nedokážeme dôkazu dôverovať, nemôžeme na ňom stavať ďalšie matematické nástroje ani techniky.
Príkladom je slávny problém P verzus NP. Otázka, či sa problémy, ktorých riešenia vieme rýchlo overiť, dajú aj rýchlo nájsť. Dôkaz by mohol zásadne zmeniť plánovanie, logistiku, návrh čipov či vývoj liekov. Zároveň by však mohol ohroziť dnešné kryptografické systémy. V hre teda nie je len teória.
Dôkaz je sociálny konštrukt
Možno to prekvapí, no matematické dôkazy boli vždy do istej miery sociálnym konštruktom. Ich cieľom bolo presvedčiť ostatných matematikov, že argumenty sú správne. Dôkaz sa považuje za pravdivý, keď ho odborná komunita preskúma a uzná. To však neznamená, že je nevyvrátiteľne pravdivý. Andrew Granville z Univerzity v Montreale dokonca naznačuje, že problémy môžu existovať aj v niektorých známych dôkazoch.
Existujú na to príklady. „Boli slávne práce, ktoré sa ukázali ako nesprávne pre drobné jazykové nepresnosti,“ povedal.
Najznámejším prípadom je dôkaz poslednej Fermatovej vety od Andrewa Wilesa. Veta tvrdí, že hoci existujú celé čísla, kde súčet dvoch štvorcov sa rovná tretiemu, pre vyššie mocniny to neplatí.
Wiles pracoval sedem rokov takmer v izolácii a v roku 1993 predstavil dôkaz v Cambridgei. Po jeho posledných slovách „Myslím, že tu skončím“ nasledoval potlesk a oslava. Médiá po celom svete hlásili víťazstvo nad 350-ročným problémom.
Počas recenzného procesu však vyšla najavo závažná chyba. Wiles strávil ďalší rok jej opravou. Istý čas teda svet veril v dôkaz, ktorý ešte nebol správny.
Systémy matematického overovania
Práve preto vznikla snaha posilniť dôkazy pomocou tzv. jazykov formálnej verifikácie.
Najznámejší z nich, Lean, vyžaduje, aby matematici zapísali dôkazy do presného formátu. Počítač následne kontroluje každý krok podľa prísnej logiky. Ak narazí na problém, zastaví proces. Tým sa eliminuje priestor pre jazykové nedorozumenia.
Kevin Buzzard z Imperial College London patrí medzi najväčších zástancov tejto metódy. „Začal som sa tomu venovať, pretože som sa obával, že ľudské dôkazy sú neúplné a zle zdokumentované,“ povedal.
Formálne overovanie by mohlo byť ešte účinnejšie, ak sa spojí s AI. „Ak prinútime AI generovať dôkazy vo formálne overiteľnom jazyku, väčšina problému sa tým vyrieši,“ myslí si Tao.
Buzzard si predstavuje dialóg medzi AI a systémom Lean. Lean by označoval chyby a AI by ich opravovala. Takáto spolupráca by mohla umožniť riešiť problémy presahujúce ľudskú kreativitu.
„AI je veľmi dobrá v hľadaní prepojení medzi oblasťami matematiky, ktoré by nás možno ani nenapadlo spojiť,“ hovorí Marc Lackenby z Oxfordu.
Dôkaz, ktorému nik nerozumie?
Ak tento trend dotiahneme do extrému, môžeme sa ocitnúť v situácii, keď AI vytvorí objektívne správne dôkazy, ktorým však nikto nerozumie.
To je pre matematikov znepokojujúce z iného dôvodu. Aký má zmysel dôkaz, ktorému nikto nerozumie? A možno hovoriť o prínose pre ľudské poznanie?
Takéto situácie však nie sú úplne nové. „Existujú práce s dvadsiatimi autormi, kde každý rozumie len svojej časti,“ povedal Buzzard. „Nikto nerozumie celku. A to je v poriadku.“
Počítačom asistované dôkazy tu máme už desaťročia. Príkladom je veta o štyroch farbách. Problém, ktorý bol v 70. rokoch rozdelený na tisíce prípadov a overený počítačom.
Prvý takýto dôkaz bol publikovaný v roku 1977, neskôr nasledovali vylepšené a formálne overené verzie. Dnes je tento dôkaz bežnou súčasťou učebníc. „Ľudia boli z toho spočiatku pobúrení,“ pripomína Buzzard. „Dnes je to normálne.“
Nezmapované územie
To všetko sa však líši od situácie, keď AI sama navrhuje, testuje aj overuje dôkaz, ktorému človek nemusí nikdy porozumieť.
AI už teraz mení povahu matematiky. Po stáročia boli dôkazy určené ľuďom. Blížime sa k situácii, keď stroje budú vytvárať nepriestrelnú logiku, ktorej ľudia nebudú rozumieť.
Ak AI zvládne celý proces, od návrhu po overenie, „potom ste vyhrali,“ povedal Lackenby. „Niečo ste dokázali.“
Zostáva však filozofická otázka: ak dôkazu rozumie iba počítač, zostáva matematika ľudskou disciplínou? Alebo sa mení na niečo úplne iné? A aký je potom jej zmysel?
About the Author
