OpenAI tento týždeň naraz zverejnila stovky textov s údajnými riešeniami ťažkých matematických problémov. Namiesto uznania si tým vyslúžila vlnu kritiky: skupina matematikov vedená Fieldsovým medailistom Terencem Taom vyzvala na bojkot firmy a časť matematických dôkazov musela OpenAI deň po zverejnení sama stiahnuť. Spor ukazuje, že otázka, čo znamená „vyriešený“ problém, keď riešenie dodá AI model, zostáva otvorená.
V skratke:
- OpenAI zverejnila 722 textov (manuskriptov) s matematickými dôkazmi, tri z nich musela o deň neskôr stiahnuť, zostalo ich 719.
- Iba 10 zo 719 textov obsahovalo aj postup uvažovania modelu (chain of thought), 42 percent dôkazov neprešlo formálnym overením v jazyku Lean.
- Skupina Association for Human Mathematics pod vedením Terencea Taa vyzvala matematikov, aby s OpenAI prestali spolupracovať.
- Vedci z Cambridge a King’s College v Londýne našli rozdiely medzi slovným a formálnym zápisom dôkazu úlohy odvodenej od Navier-Stokesových rovníc.
Ako to funguje: čo je autoformalizácia
Keď AI model „vyrieši“ matematický problém, najprv vytvorí vysvetlenie v bežnom jazyku a potom sa ho pokúsi zapísať v programovacom jazyku Lean, ktorý vie formálne, krok po kroku, overiť, či je dôkaz logicky správny. Tomuto prevodu sa hovorí autoformalizácia. Problém je, že preklad z ľudského jazyka do kódu Lean nie je vždy presný, takže formálne „overený“ dôkaz môže v skutočnosti riešiť čosi mierne odlišné od toho, čo tvrdí slovný popis.
Presne takéto rozdiely našli vedci z Cambridge a King’s College pri jednej z úloh odvodených od Navier-Stokesových rovníc, ktorú OpenAI prezentovala ako vyriešenú. Rozdiely medzi oboma verziami dôkaz priamo nevyvracajú, ale podľa autorov ukazujú, že výsledkom autoformalizácie by sa nemalo veriť bez rovnakého recenzného procesu, akým prechádzajú bežné matematické práce.
Matematici žiadajú bojkot OpenAI
Poradná skupina Advisory Group on Mathematics and Artificial Intelligence (AGMAI), zložená z deviatich uznávaných matematikov a hostená Institute for Advanced Study na Princetonskej univerzite, koncom septembra vydala odporúčania pre firmy testujúce AI na matematických problémoch. Prvým bodom bolo, aby sa náročné otvorené problémy neskúšali na neverejných, firemných modeloch. OpenAI podľa portálu TechCrunch toto odporúčanie nerešpektovala a svoje interné modely na takýchto problémoch testovala ďalej.
Skupina Association for Human Mathematics (AHM), ktorú vedie Terence Tao, na zverejnenie reagovala vyhlásením, že OpenAI porušila základné normy vedeckej práce, a vyzvala matematikov, aby s firmou prestali spolupracovať. Podľa AHM nejde o „prejav vedeckej práce, ale o prejav sily“. Tao zverejnenie okomentoval aj na sieti Mastodon, kde hovorí o nastupujúcej ére „Math 2.0“, v ktorej by riešenie problémov nemalo byť hlavným cieľom odboru. Informatik Scott Aaronson na svojom blogu situáciu označil za „mathokalypsu“. K predošlému varovaniu sa pridalo aj 24 ďalších držiteľov Fieldsovej medaily, napríklad Peter Scholze, Maryna Viazovska a Martin Hairer, ktorí upozornili na „závažný nesúlad“ medzi cieľmi AI firiem a cieľmi matematiky ako odboru.
Prečo na tom záleží: chýba ľudské pochopenie
Jadrom spora je, že pri klasickom matematickom výsledku autor zaň berie zodpovednosť, publikuje ho, obhajuje na konferenciách a vysvetľuje ostatným. Pri dôkaze, ktorý model vyprodukoval na jeden príkaz, podľa matematičky z Harvardu Melanie Woodovej „v čase zverejnenia neexistuje ľudské pochopenie výsledku, práca sa až potom začína“. AGMAI preto odporúčala, aby OpenAI pomáhala financovať prácu matematikov, ktorí musia dôkazy spätne sprístupniť zvyšku odboru, čo sa podľa kritikov doteraz nestalo. Podobný spor sa odohral aj pri skoršom tvrdení OpenAI o vyriešení problému odvodeného od Navier-Stokesových rovníc, kde firme vyčítal nátlak a snahu o zásluhy matematik z New York University; aiportal.sk o tomto spore informoval už v septembri.
Iný prístup: ako postupuje Anthropic
Aaronson v tejto súvislosti porovnáva prístup OpenAI s tým, ako pracuje konkurenčný Anthropic. Zatiaľ čo OpenAI naraz vypustí stovky surových výstupov modelu a prenesie prácu s ich overením na komunitu zadarmo, Anthropic pri dvoch starých matematických hypotézach spolupracoval s dvojicou výskumníkov, ktorí od firmy dostali honorár a dôkaz, ku ktorému im AI model dodal kľúčovú myšlienku, prepísali do podoby, ktorej môžu rozumieť ostatní ľudia. Aaronson upozorňuje, že ani tento model nie je bezchybný, pretože súkromná firma si sama vyberá, ktorí matematici sa stanú „vyslancami“ výsledku a získajú pri ňom zásluhy. Debata sa rozbehla aj preto, že OpenAI už skôr tvrdila, že jej interný model vyriešil za jediný mesiac vyše sto otvorených matematických problémov; aiportal.sk o tomto tvrdení a vzniku poradného výboru AGMAI písal v septembri.
Čo to znamená pre firmy
Pre firmy, ktoré uvažujú o nasadení AI pri analytickej alebo výskumnej práci, je tento spor pripomienkou, že výstup modelu, aj keď vyzerá formálne overený, ešte nemusí byť spoľahlivý bez toho, aby si ho preveril človek, ktorý danej oblasti rozumie. Platí to v menšom rozsahu aj mimo matematiky, pri analýzach, právnych rozboroch alebo účtovných výpočtoch, kde „formálne správny“ výstup nemusí znamenať výstup správny v reálnom zmysle.
Čo sledovať ďalej: V najbližších týždňoch sa ukáže, koľko matematikov na výzvu AHM naozaj zareaguje a či OpenAI zmení spôsob zverejňovania výsledkov, napríklad doplnením metadát spájajúcich slovný a formálny zápis dôkazov, ako to AGMAI požadovala. Sledovať sa oplatí aj to, či podobný spor vznikne pri ďalšom veľkom tvrdení o vyriešení otvoreného problému, ktoré oznámi niektorá z veľkých AI firiem.
