OpenAI rešil na stotine matematičnih problemov

Če smo še pred mesecem dni pisali, da je OpenAI s svojim agentom rešil enega najbolj znanih matematičnih problemov, lahko to pot predmet postavimo v množino. OpenAI je z internim modelom, ki še ni dostopen javnosti, objavil dokaze več sto matematičnih problemov. Matematiki jih še niso ročno preverili, prve analize s formalnim jezikom Lean pa kažejo, da bi dokazi lahko bili pravilni. OpenAI seveda ni nič bolj naklonjen matematiki kot kakšnim drugim vedam, a izkorišča njeno prednost. Za razvoj in testiranje svojih modelov potrebuje čim težje probleme, matematični izzivi pa imajo zelo jasno pot za preveritev rezultata. Težko je reči, ali je model napisal boljši sonet od Prešerena, medtem ko je matematični dokaz mogoče formalno in rigorozno preveriti. Nerešeni problemi v matematiki so zato dragocena vadbišča za modele. In tako je OpenAI na GitHub odložil dokaze za 372 problemov. Večino je Lean že preveril in potrdil, zato je sedaj žogica na strani matematikov. OpenAI dodaja, da je interni model, ki je primerljiv z najdražjimi dostopnimi komercialnimi modeli (ki stanejo 500 dolarjev mesečno), večino problemov rešil z enim samim pozivom v nekaj urah razmišljanja za vsak problem. To je precej drugače od rešitve Navier-Stokesove domneve, za kar so potrošili 15 milijonov dolarjev, ko je 10.000 agentov trlo oreh. Ključno vprašanje je, kam to vodi. Matematičnih problemov ne rešujemo samo zato, ker nas zanima rešitev, temveč tudi ker se ob tem kaj novega naučimo, bodisi kot skupnost bodisi novi rodovi matematikov. Umetna inteligenca nas tega oropa, a po drugi strani so njeni dokazi lahko povsem nepričakovani in povežejo veje matematike, ki jih ljudje še niso. Nekateri matematiki, denimo Terrence Tao, so zato do umetne inteligence močno kritični. Drugi pa poudarjajo, da morajo biti podjetja transparentna in razkriti delovanje modelov. A dejstvo je, da je duh ušel iz steklenice.[st.slika 76673]