Svet

Sumnje u dokaz OpenAI-ja: Da li je veštačka inteligencija zaista rešila problem veka?

Sumnje u dokaz OpenAI-ja: Da li je veštačka inteligencija zaista rešila problem veka?

Tvrdnja kompanije OpenAI da je njen sistem veštačke inteligencije rešio jedan od čuvenih milenijumskih matematičkih problema našla se pod novim znakom pitanja. Grupa istraživača utvrdila je da računarski proverena verzija dokaza ne odgovara u potpunosti objašnjenju napisanom jezikom razumljivim ljudima.

OpenAI je početkom septembra objavio da je njegov interni sistem pronašao rešenje problema postojanja i glatkoće Navije–Stoksovih jednačina, koji je gotovo 90 godina ostao bez odgovora. Ove jednačine opisuju kretanje tečnosti i gasova i koriste se u vazduhoplovstvu, meteorologiji, medicini i brojnim drugim oblastima. Kompanija tvrdi da je dokazala da čak i prvobitno mirna tečnost, pod dejstvom glatke spoljne sile, može za konačno vreme razviti singularnost – stanje u kojem brzina matematički raste bez granice.

Sistem od oko 10.000 međusobno povezanih AI agenata navodno je do rezultata stigao posle 88 sati rada. Dodatnih 17 sati bilo je potrebno da se dokaz prevede u formalni programski jezik Lean, namenjen mehaničkoj proveri matematičkih tvrdnji. Upravo je ta formalna verifikacija predstavljena kao jedan od najjačih argumenata da je rešenje tačno.

Međutim, istraživači Aleksandar Bastunis sa Kraljevskog koledža u Londonu, Fabijan Čirčeli i Anders Hansen sa Univerziteta Kembridž ukazali su na ozbiljan problem. U radu pod nazivom „Navier–Stokes izgubljen u prevodu“ naveli su da dokaz proveren u Leanu ne odgovara dosledno dokazu napisanom prirodnim matematičkim jezikom. Drugim rečima, računar je možda ispravno proverio formalno zapisanu tvrdnju, ali nije sigurno da je proveravao potpuno istu tvrdnju koju OpenAI predstavlja javnosti.

Autori istraživanja ipak nisu zaključili da je dokaz OpenAI-ja pogrešan. Njihov nalaz pokazuje da automatsko prevođenje matematičkog teksta u formalni jezik može promeniti pretpostavke ili značenje pojedinih delova dokaza. Zato sama oznaka „provereno u Leanu“ još ne garantuje da je i originalno, ljudima razumljivo obrazloženje u potpunosti tačno.

Konačnu reč još nije dao ni Institut za matematiku Klej, koji za rešenje svakog milenijumskog problema nudi nagradu od milion dolara. Za zvanično priznanje neophodni su objavljivanje rada u uglednom stručnom časopisu, protok najmanje dve godine, nezavisna provera i šire prihvatanje rezultata u matematičkoj zajednici. OpenAI je saopštio da ne namerava da traži novčanu nagradu, ali ostaje otvoreno najvažnije pitanje: da li je veštačka inteligencija zaista rešila problem veka ili je dokaz još jedanput „izgubljen u prevodu“?

Language