OpenAI během necelého měsíce podruhé vypouští do světa matematické rukopisy, tentokrát navíc s velkými nároky na informatiku a fyziku. Neumím posoudit důkaz z teorie kvantových polí — sotva jsem se smířila s tím, že kvantová mechanika není název metalové kapely — ale způsob, kterým se výsledky ověřují a zveřejňují, je možná stejně důležitý jako samotné titulky.
Tři tvrzení, u kterých nestačí zatleskat
První materiál se týká matematického problému zvaného local smoothing conjecture pro vlnovou rovnici. Zjednodušeně jde o tvrzení o tom, jak se vlny v prostoru lokálně „vyhlazují“. OpenAI píše, že model vytvořil důkaz ve všech dimenzích alespoň dvě a že z něj plynou i výsledky pro Kakeyův problém a Steinovu restrikční domněnku.
Druhý výsledek míří do teoretické informatiky: má vyvracet Exponential Time Hypothesis neboli ETH. Jde o dlouho používaný předpoklad, že určitou třídu logických úloh, včetně 3-SAT, nelze přesně řešit výrazně rychleji než exponenciálním časem. Zveřejněný postup údajně nabízí deterministický algoritmus pro přesné počítání řešení formulí CNF v subexponenciálním čase a tím ETH vyvrací. To zní obrovsky, jenže slovo „údajně“ tu není kosmetická brzda: důkaz musí projít cizíma očima.
Třetí tvrzení je zatím nejméně veřejné. Má jít o matematicky rigorózní důkaz existence některých interagujících kvantových teorií pole ve čtyřech rozměrech, včetně teorií s kalibračními poli a fermiony. Plné podklady k fyzice zveřejněné nejsou, takže z nich jako běžná čtenářka nemám co kontrolovat. A vlastně ani odborníci bez materiálů.
Ověřování není příloha pod čarou
U informatiky má práci posuzovat skupina vedená Russellem Impagliazzem, Ramamohanem Paturim a Ryanem Williamsem. Impagliazzo a Paturi přitom patřili mezi autory původní formulace ETH z roku 1999. U fyziky má podobnou roli skupina vedená Davidem Grossem. OpenAI pro tyto externí odborníky používá označení „shepherds“, tedy lidé, kteří mají výsledek provést odborným terénem a vysvětlit ho komunitě.
Tenhle model mi přijde rozumnější než představa, že firma vydá několik stovek AI rukopisů a akademici si mají prostě poradit. Kontrola, opravy, zjednodušení důkazu a jeho výklad nejsou druhořadá administrativa. U složitých výsledků jsou to často celé roky práce, bez níž nikdo pořádně neví, co vlastně bylo dokázáno.
Pro informatický výsledek jsou navíc zveřejněny zápis modelového výstupu i důkaz v Lean. Lean je systém pro formální ověřování důkazů: matematické kroky se do něj zapíšou tak přesně, aby jejich logickou správnost mohl stroj zkontrolovat. Ani to automaticky nevyřeší, zda formalizace zachycuje přesně zamýšlené tvrzení, ale je to podstatně lepší start než oslnivý PDF soubor, kterému rozumí pět lidí na planetě.
Férový přístup ke strojovým objevům se teprve hledá
Celá věc má i trochu nepříjemnou společenskou vrstvu. Poradní panel AGMAI, který OpenAI sestavila pro matematiku, den před tímto oznámením doporučil AI firmám, aby neurčovaly několik vybraných lidí s přednostním přístupem k výstupům. Rizika jsou jasná: nerovný přístup, propůjčování reputace i zaujatý výběr těch, kteří dostanou možnost být u výsledku první.
Panel naopak navrhuje zveřejňovat výstupy ve vědeckých repozitářích, přikládat Lean-formalizované důkazy, vysvětlit výběr problému a finančně podpořit lidi, kteří budou výsledky rozebírat. Mně osobně připadá důležité hlavně to poslední. Jestli AI dokáže chrlit materiály rychleji, než je lidská komunita stihne promyslet, pak problém není jen výkon modelu. Problém je, kdo zaplatí pomalou, trpělivou a neviditelnou kontrolu.
OpenAI u informatického výsledku zveřejnila i otevřený dopis s otázkami k pravidlům raného přístupu, střetu zájmů a rozdělování zásluh. To nejsou drobnosti na konec tiskové zprávy. Pokud mají AI systémy přinášet seriózní vědecké poznatky, potřebujeme vědět nejen co našly, ale také kdo to ověřil, kdo tomu porozuměl a komu zůstane možnost nesouhlasit.
Zatím tedy neberu tři výsledky jako hotové medaile pro model. Beru je jako velmi zajímavý test: zda akademická komunita dokáže nezávisle rozebrat mimořádně složité AI výstupy — a zda jí k tomu firmy dají materiály, čas i férové podmínky.
