AI a matematika
Souhrn
Terence Tao ve svém vystoupení na IMO 2024 představuje historický vývoj a současný stav využívání počítačů a umělé inteligence v matematice. Vysvětluje, jak matematici používali výpočetní pomůcky po tisíce let - od abaku přes lidské “počítače” až po moderní systémy. Historicky se počítače využívaly především pro vytváření tabulek a databází, numerické výpočty a řešení složitých algebraických problémů.
V současnosti se matematika proměňuje díky třem hlavním technologickým přístupům: strojovému učení a neuronových sítím, velkým jazykovým modelům a formálním verifikačním systémům. Tao podrobně popisuje formalizaci matematických důkazů pomocí jazyků jako je Lean, což umožňuje kolaborativní ověřování složitých teorií. Uvádí příklady významných matematických problémů řešených s počítačovou pomocí, včetně věty o čtyřech barvách, Keplerovy domněnky a nedávných projektů formalizace komplexních důkazů.
Přepis
Dobrý den všem. Dobrý den. Někteří z vás, milí soutěžící, jste velmi mladí, takže možná nevíte, kdo je profesor Terence Tao. Proto jen pár slov úvodem. Poprvé se zúčastnil IMO, když mu bylo 11 let, a získal bronzovou medaili. Další rok se vrátil a získal stříbrnou medaili. Poté ve věku 13 let získal zlatou medaili. Byl nejmladším účastníkem, který kdy získal zlatou medaili. Potom se, nevím, asi znudil, šel na univerzitu a IMO se už nezúčastnil. Nyní je profesorem na Kalifornské univerzitě v Los Angeles. Mohu říci, že je rozhodně největší hvězdou IMO a samozřejmě jedním z nejvlivnějších matematiků naší doby. Prosím, profesor Terence Tao.
Děkuji. Jsem velmi rád, že jsem zpět na IMO. Čas, který jsem strávil na IMO, byl jedním z nejzábavnějších období mého života. Stále na to rád vzpomínám. Doufám, že jste si to všichni užili, nejen v soutěži, ať už jste získali dobré skóre nebo ne, ale také při společenských aktivitách. Vždy zde připraví opravdu skvělou akci.
Moje přednáška je o umělé inteligenci a obecněji o strojové asistenci v matematice. Všichni jste slyšeli o AI a o tom, jak mění vše. Myslím, že dnes dopoledne byla přednáška od DeepMind o tom, jak vydali nový produkt, Alpha Geometry, který už nyní dokáže odpovídat na některé geometrické otázky IMO. A hned po mé přednášce bude prezentace o AI Matematické olympiádě, takže prosím, zůstaňte po mé přednášce.
Budu mluvit více o tom, jak tyto nástroje začínají měnit výzkumnou matematiku, která se liší od soutěžní matematiky. Místo toho, abyste měli tři hodiny nebo tak nějak na vyřešení problému, trvá to měsíce, a někdy problém nevyřešíte a musíte ho změnit. Rozhodně to není stejné jako matematické soutěže, i když v dovednostech existuje určitý překryv.
Je to všechno velmi vzrušující a začíná to být transformativní. Na druhé straně je tu také pocit kontinuity. Počítače a stroje používáme k matematice už dlouhou dobu. Mění se pouze způsob, jakým to děláme, ale navazuje na dlouhou tradici strojové asistence.
Takže tady je otázka: Jak dlouho používáme stroje k matematice? A odpověď je tisíce let. Tady je stroj, který Římané používali k matematice - abakus, jeden z prvních strojů. Existují i některé starší. Dobře, to je docela nudné. To není opravdu chytrý stroj.
A co počítače? Jak dlouho používáme počítače pro matematiku? To je asi 300, 400 let. To zní možná divně, protože naše moderní počítače neexistovaly do 30. a 40. let 20. století. Ale počítače nebyly vždy elektronické. Předtím byly mechanické a ještě předtím byly lidské. “Počítač” byla ve skutečnosti pracovní profese, někdo, kdo počítá. Zde je skupina počítačů během světové války. Vypočítávali balistiku a další věci. Měli celou skupinu počítačů, což byly převážně dívky, protože muži bojovali ve válce, s velkými mechanickými kalkulačkami. A byli programátoři, kteří v podstatě jen říkali dívkám, co mají dělat. Základní jednotkou výpočetního výkonu v té době nebyl CPU, ale kilogram. Tedy kilogramhodina - kolik výpočtů můžete udělat s 1000 dívkami pracujícími takto po dobu jedné hodiny.
Ale používali jsme počítače už i před tím, jak jsem řekl, od 18. století nebo dokonce dříve. Nejzákladnější využití počítačů v těch dobách bylo vytváření tabulek. Možná jste slyšeli o logaritmických tabulkách Napiera. Pokud jste chtěli vypočítat siny a cosiny a tak dále, použili jste počítač k vytvoření těchto obrovských tabulek. Když jsem byl ještě na střední škole, stále jsme se v našem učebním plánu učili, jak tyto tabulky používat, které se právě vyřazovaly. Měli jsme kalkulačky a teď počítače. V matematickém výzkumu stále používáme tabulky. Říkáme jim teď databáze, ale stále jde o totéž. Existuje mnoho důležitých výsledků v matematice, které byly poprvé objeveny prostřednictvím tabulek v teorii čísel.
Teorie uzlů je docela zábavnou oblastí matematiky. Je to zajímavá oblast, která spojuje mnoho různých oblastí matematiky, které spolu běžně nekomunikují. Uzel je jen smyčka provázku nebo křivky v prostoru, která je uzavřená. Dva uzly jsou ekvivalentní, pokud existuje způsob, jak jeden uzel spojitě deformovat na druhý, přičemž provázek se nesmí překřížit sám se sebou. Základní otázky v teorii uzlů jsou: Kdy jsou dva uzly ekvivalentní? Pokud vám dám dva uzly, existuje způsob, jak jeden převést na druhý?
Běžný přístup k této otázce spočívá ve vývoji tzv. invariantů uzlů. To jsou různá čísla, někdy také polynomy, které lze přiřadit uzlu. Tato čísla se nemění bez ohledu na to, jak spojitě deformujete uzel. Pokud tedy dva uzly mají různé invarianty, nemohou být ekvivalentní. Existuje mnoho typů invariantů uzlů. Existuje něco, co se nazývá signatura, kdy zploštíte uzel a počítáte křížení, zda křížení jdou přes nebo pod, a vytvoříte určitou matici atd. A existuje určité celé číslo zvané signatura. To je jeden typ invariantu uzlu.
Existují také slavné polynomy nazývané Jonesův polynom a HOMFLY polynom, které jsou spojeny s mnoha oblastmi matematiky, ale o těch mluvit nebudu. A pak existují tzv. hyperbolické invarianty, které pocházejí z geometrie. Můžete vzít komplement uzlu a to je ve skutečnosti to, čemu se říká hyperbolický prostor. Má určitou geometrickou strukturu, má pojem vzdálenosti a můžete měřit jeho objem a další invarianty.
Takže každý uzel má nějaké kombinatorické invarianty, jako jsou signatury. A má také geometrické invarianty, jako jsou hyperbolické invarianty. Zde je celý seznam uzlů s různými hyperbolickými invarianty. Existuje něco, čemu se říká hyperbolický objem a homotopický tvar kuspidu atd. Jsou to reálná a komplexní čísla. Nikdo však nevěděl o žádném spojení mezi těmito dvěma přístupy - existovaly dva oddělené způsoby vytváření statistik uzlů a neexistovala mezi nimi žádná spojitost.
Teprve nedávno začali lidé používat strojové učení k řešení tohoto problému. Vytvořili databáze milionů uzlů, což už byl mírně netriviální úkol. Natrénovali na tom neuronovou síť a zjistili, že po tréninku neuronové sítě jí mohli dát všechny hyperbolické geometrické invarianty a asi v 90 % případů správně předpověděla signaturu. Vytvořila tedy černou skříňku, která vám řekne, jak byla signatura nějakým způsobem ukryta v těchto geometrických invariantech. Neřekla vám však, jak to funguje, byla to jen černá skříňka. Ale i tak je to užitečné, protože jakmile máte tuto černou skříňku, můžete si s ní hrát.
To, co udělali dále, je velmi jednoduchá analýza, tzv. analýza významnosti. Tato černá skříňka bere asi 20 různých vstupů, jeden pro každý hyperbolický invariant, a poskytuje jeden výstup - signaturu. Jakmile máte tuto černou skříňku, můžete každý vstup mírně upravit. Řeknete: co když změním jeden vstup? Jak pravděpodobné je, že se změní výstup? Z těch 20 vstupů zjistili, že pouze tři z nich hrály opravdu významnou roli ve výstupu. Ostatních 17 bylo sotva relevantních. A nebyly to ty tři, které očekávali. Očekávali například, že objem bude velmi důležitý, ale ukázalo se, že objem je téměř irelevantní. Nejdůležitější byly tři: něco nazvaného podélná translace a reálné a komplexní části meridiánové translace.
Jakmile identifikovali ty nejdůležitější, mohli přímo vynést signaturu vůči těmto třem konkrétním vstupům a pak mohli vidět vlastníma očima. Místo použití neuronové sítě použili “lidskou síť”, aby viděli, že existují nějaké zřejmé vzory. A tak pouhým pozorováním těchto grafů mohli vytvořit domněnky o tom, co se vlastně děje. Tak vytvořili domněnku založenou na tomto, která se ukázala být nesprávná. Ale použili neuronovou síť, aby ukázali, proč je špatná. A způsob, jakým selhala, jim umožnil opravit ji a našli opravenou verzi domněnky, která skutečně tento fenomén vysvětlovala. A jakmile našli správné tvrzení, byli schopni ho dokázat. Takže mají teoretické vysvětlení, proč signatura úzce souvisí s těmito konkrétními statistikami.
Myslím, že toto je způsob, jakým se strojové učení stále více používá v matematice. Neřeší přímo problém, ale dává vám všechny tyto užitečné nápovědy ohledně spojení a kam se dívat. Ale stále potřebujete člověka, aby skutečně vytvořil ta spojení.
A nakonec máme velké jazykové modely, které jsou nejokázalejší a možná vyvolaly největší rozruch. Víte, neuronové sítě existují již 20 let, jazykové modely jsou tu také již asi pět let, ale teprve nedávno dosáhly v produkci téměř lidské úrovně. Všichni jste pravděpodobně slyšeli o GPT-4, současném modelu ChatGPT.
Když vyšel GPT-4, byl publikován článek popisující jeho schopnosti. Do modelu vložili otázku z Mezinárodní matematické olympiády (IMO) 2022. Jde o mírně zjednodušenou verzi. Když jste dali modelu tuto konkrétní otázku, dal úplné a správné řešení. Skutečně vyřešil otázku z IMO. Bohužel je to extrémně selektivní příklad - testovali stovky otázek na úrovni IMO a měli úspěšnost asi 1 %. Takže tento konkrétní problém dokázali vyřešit a museli problém naformátovat správným způsobem, aby dostali řešení. Ale i tak je to docela úžasné.
Na druhou stranu, vtipné na těchto nástrojích je, že věci, které lidé považují za obtížné, může AI někdy dělat velmi snadno, ale s věcmi, které lidé považují za jednoduché, AI často bojuje. Je to velmi ortogonální způsob řešení problémů.
V souvisejícím příspěvku požádali stejný model o základní aritmetický výpočet: 7 × 4 + 8 × 8. Model, který pouze hádá nejpravděpodobnější výstup na základě vstupu, v podstatě jen uhádl, že odpověď je 120. Pak se zastavil a řekl: “Dobře, možná bych měl vysvětlit, proč je to 120.” Tak provedl výpočet krok za krokem, ale když provedl výpočet krok za krokem, došel ke skutečné odpovědi, která je 92 a ne k odpovědi, se kterou začal. Takže když jste se zeptali: “Počkej, ale řekl jsi, že to bylo 120,” model odpověděl: “Ach, to byl překlep, správná odpověď je 92.”
Takže neřeší problémy z prvních principů, jen odhadují v každém kroku výstupu, co je nejpřirozenější říci dále. A úžasné je, že to někdy funguje, ale často ne. A stále pokračuje snaha, jak to udělat přesnější.
Lidé zkoušejí různé věci. Můžete tyto modely propojit s jiným, spolehlivějším softwarem. Ve skutečnosti uvidíte prezentaci, kde je velký jazykový model připojen - kdy výpočet neděláte sami, ale svěřujete ho v tomto případě Pythonu.
Ale můžete také jazykový model přimět, aby produkoval pouze správné odpovědi tím, že jej donutíte generovat výstup v jednom z těchto formálních jazyků. A pokud se to nezkompiluje, pošlete to zpět do AI a AI to musí zkusit znovu. Nebo se můžete pokusit ji přímo učit. Stejné techniky řešení problémů se používají k řešení problémů IMO - zkuste jednoduché příklady, důkaz sporem, snažte se postupovat krok za krokem atd.
Lidé zkoušejí všechny možné věci. Stále to zdaleka nedokáže vyřešit většinu řekněme matematických olympiádních problémů, natož matematické výzkumné problémy, ale děláme pokroky.
Kromě schopnosti přímo řešit problémy je také užitečné jako múza. Sám jsem tyto modely také používal. Experimentoval jsem s různými problémy. Měl jsem kombinatorický problém, kde jsem zkoušel několik věcí a nefungovaly. Tak jsem zkusil zeptat se GPT: “Jaké další techniky bys doporučil k vyřešení této otázky?” Dal mi seznam 10 technik, z nichž asi pět jsem již vyzkoušel nebo byly zjevně neužitečné. Ale byla jedna technika, kterou jsem nevyzkoušel, a to použití generujících funkcí pro tuto konkrétní otázku, což, jakmile to navrhli, jsem si uvědomil, že je to správný přístup, ale přehlédl jsem ho. Takže jako někdo, s kým lze konverzovat, je to docela užitečné. Není to teď skvělé, ale není to úplně k ničemu.
Existuje další typ AI asistence, která se stala velmi užitečnou pro důkazové asistenty. Jak jsem řekl, psaní formálních důkazů je velmi únavný úkol. Je to jako jakýkoliv opravdu puntičkářský počítačový jazyk - musíte mít přesně správnou syntax. Pokud vynecháte krok, nekompiluje se.
Ale existují nástroje - používám něco, čemu se říká GitHub Copilot, kde můžete napsat polovinu důkazu a on se pokusí uhodnout, co bude na dalším řádku. Asi ve 20% případů skutečně uhádne něco blízkého správnému řešení. A pak můžete říci: “Přijmu to.” V tomto případě jsem se snažil dokázat zde uvedené tvrzení a řádky šedivé jsou ty, které navrhl Copilot. Ukazuje se, že první řádek je zbytečný, ale druhý řádek, který není úplně vidět, vlastně vyřešil tento konkrétní problém.
Takže stále musíte… nemůžete jen přijmout vstup, protože nemusí nutně kompilovat. Ale pokud už víte, jak kód zhruba funguje, ušetří vám to hodně času. Tyto nástroje se stále zlepšují. Takže právě teď mohou, pokud je důkaz dlouhý jeden řádek nebo dva, vyplnit ho automaticky.
Nyní probíhají experimenty s iterací AI, která navrhuje důkaz, pak ho vrátíte do kompilátoru, a pokud se špatně zkompiluje, pošlete zpět chybovou zprávu. A dostáváme se k důkazům, které jsou dlouhé čtyři nebo pět řádků a mohou být vytvořeny touto metodou. Velký důkaz má samozřejmě desetitisíce řádků. Takže to není ani zdaleka v bodě, kdy můžete svůj důkaz okamžitě formalizovat. Ale už je to užitečný nástroj.
Takže kde jsme teď? Existují lidé, kteří doufají, že za několik let budeme moci používat počítače k přímému řešení matematických problémů. Myslím, že jsme od toho stále ještě daleko. Pro velmi úzce zaměřené problémy můžete nastavit specializované AI, které zvládnou velmi úzkou škálu problémů. Ale i tak nejsou zcela spolehlivé. Mohou být užitečné, ale stále…
Takže přinejmenším v příštích několika letech to budou v podstatě velmi užiteční asistenti. A kromě hrubé výpočetní pomoci, kterou už známe, lidé zkouší všechny druhy kreativních věcí.
Myslím, že jeden směr, který považuji za obzvláště zajímavý a který zatím nebyl příliš úspěšný, je naděje, že tyto AI se stanou velmi dobré v generování dobrých domněnek. Už jsme viděli malý příklad s uzly, kde už mohli tak trochu odhadovat spojení mezi dvěma různými statistikami. Existuje tedy naděje, že vytvoříte tyto obrovské datové sady, nahrajete je do AI a ta by automaticky generovala spoustu pěkných spojení mezi různými matematickými objekty. Tohle se ještě pořádně nedělá. Ještě nevíme, jak to dělat, částečně proto, že nemáme tyto masivní datové sady. Ale myslím, že to časem bude možné.
Jedna věc, která mě také nadchla, je typ metody, který ještě neexistuje. Protože dokazování vět je takový bolestivý, pracný proces, dokazujeme jednu větu najednou, nebo možná dvě nebo tři, pokud jste efektivní. Ale s AI si můžete představit, že v budoucnu místo snahy dokázat jeden problém nebo něco podobného vezmete třídu 1000 podobných problémů a řeknete: “Dobře, řeknu vaší AI, zkuste vyřešit těchto 1000 problémů touto technikou a uvidíme. Och, mohl jsem vyřešit 35 % těchto problémů touto technikou. Co tato technika? A můžu vyřešit toto procento problémů. Co když je zkombinuji? Můžu udělat tohle.” Mohli byste začít zkoumat prostor problémů spíše než každý problém samostatně. A to je něco, co právě teď nemůžete dělat, nebo to děláte po celá desetiletí, s desítkami a desítkami článků, které postupně zjišťují, co můžete a nemůžete dělat s různými technikami. Ale s těmito nástroji byste opravdu mohli. Mohli byste začít dělat matematiku v měřítku, které je opravdu bezprecedentní.
Myslím, že budoucnost bude velmi vzrušující. Stále budeme dokazovat věty i po staru. Ve skutečnosti musíme, protože nebudeme schopni řídit tyto AI, pokud sami nebudeme vědět, jak tyto věci dělat. Ale budeme schopni dělat spoustu věcí, které teď dělat nemůžeme.
Dobře, myslím, že tady skončím. Děkuji mnohokrát. Nějaké otázky?
[Následuje sekce otázek a odpovědí, kde diskutuje o různých tématech včetně formalizace matematiky, své osobní vzdělávací cesty a výběru výzkumných projektů.]
Kritické zhodnocení
Terence Tao, uznávaný matematický génius a držitel Fieldsovy medaile, ve svém vystoupení na IMO 2024 přináší vyvážený a informativní přehled o roli umělé inteligence v matematice. Hodnota přednášky spočívá především v propojení historického kontextu s nejnovějšími trendy v této oblasti.
Kvalita a relevance obsahu: Obsah přednášky je mimořádně relevantní vzhledem k probíhající revoluci v oblasti AI. Tao dokázal zasadit současný vývoj do širšího kontextu dlouhodobého využívání technologických pomůcek v matematice, což umožňuje lépe pochopit současné změny. Jeho rozdělení AI přístupů v matematice do tří kategorií (strojové učení, velké jazykové modely a formální verifikační systémy) poskytuje užitečný rámec pro pochopení této komplexní oblasti.
Přesnost a spolehlivost informací: Jako jeden z předních světových matematiků přináší Tao důvěryhodný pohled na téma. Jeho příklady úspěšné aplikace počítačových metod při řešení významných matematických problémů (věta o čtyřech barvách, Keplerova domněnka) jsou fakticky správné a dobře ilustrují potenciál technologií. Zmiňuje konkrétní nástroje jako formalizační jazyk Lean, což dodává jeho výkladu na věrohodnosti.
Prezentační styl a srozumitelnost: Z dostupného přepisu je patrné, že Tao dokázal oslovit různorodé publikum - od soutěžících studentů po zkušené matematiky. Jeho přirozený způsob vyjadřování a skromnost (včetně humorných poznámek o vlastní účasti na IMO) vytváří přístupnou atmosféru i při diskusi o pokročilých konceptech. Přesto bez viditelné části prezentace a z částečného přepisu nelze plně posoudit vizuální prvky a strukturu celého výkladu.
Silné stránky:
- Propojení historické perspektivy se současnými trendy
- Vhled založený na vlastních zkušenostech špičkového matematika
- Vyvážený pohled na potenciál i limity AI v matematice
- Konkrétní příklady úspěšného využití počítačů při řešení významných matematických problémů
Slabé stránky:
- Z dostupného přepisu není jasné, do jaké hloubky jsou některá témata rozvedena
- Chybí podrobnější diskuse o potenciálních rizicích nebo etických otázkách spojených s AI v matematice
- Pro laiky bez matematického základu mohou být některé koncepty obtížně pochopitelné
Vhodnost obsahu: Přednáška je primárně určena pro publikum s matematickým základem - od talentovaných středoškolských studentů (účastníci IMO) po profesionální matematiky. Tao však dokáže přiblížit téma způsobem, který osloví i širší publikum se zájmem o interakci mezi technologií a vědou. Pro úplné začátečníky nebo laiky bez základního porozumění matematickým konceptům by mohly být některé části náročnější, ale obecný rámec diskuse je přístupný i jim.
Celkově Tao nabízí vyvážený a informativní pohled na měnící se roli technologie v matematickém výzkumu, který je obzvláště cenný vzhledem k jeho pozici na špičce matematického světa a schopnosti komunikovat složité myšlenky přístupným způsobem.
