DVA AI AGENTA UMESTO LJUDSKOG ISTRAŽIVAČA
Kineski istraživački tim sa Pekinškog univerziteta razvio je sistem veštačke inteligencije koji je rešio problem iz oblasti komutativne algebre postavljen još 2014. g. Reč je o problemu koji je formulisao američki matematičar Dan Anderson. Koji je godinama ostao otvoren. Pekinški univerzitet je vest o ovom rezultatu objavio u svom medijskom centru. Detalji istraživanja predstavljeni u radu dostupnom na arXiv.
Posebnost ovog sistema nije samo u tome što pokušava da pronađe matematičko rešenje. Posebnost je u tome što je projektovan tako da proverava sopstveni rezultat. Jedan AI agent, poznat kao Rethlas, istražuje matematičku literaturu i razvija moguće strategije rešavanja. Drugi deo sistema formalizuje i proverava predloženi dokaz pomoću sistema Lean 4. Istraživači navode da je čitav proces trajao oko 80 sati i da je sproveden uz minimalnu. Odnosno suštinski nikakvu ljudsku intervenciju.
OD LITERATURE DO FORMALNOG DOKAZA
Sistem je pritom morao da uradi nešto mnogo složenije od prostog pronalaženja poznate formule. Prema opisu istraživanja, AI je pretraživao decenije matematičke literature kako bi pronašao rezultate koji bi mogli da budu ključni za rešavanje Andersonovog problema. Posebno je značajno što je sistem pronašao način da iskoristi raniji matematički rezultat koji prvobitno nije bio napisan kao rešenje ovog konkretnog problema. Zatim ga je uklopio u sopstvenu strategiju.
Problem se nalazi u oblasti komutativne algebre i vezan je za osobine određenih Noetherovih lokalnih prstenova. Prema dostupnom opisu rada, AI je do rešenja došao konstrukcijom kontraprimera koji pokazuje da jedno svojstvo ne mora da povlači drugo, čime je rešena Andersonova pretpostavka. Upravo mogućnost da samostalno poveže ranije objavljene matematičke rezultate sa novom strategijom predstavlja jedan od najzanimljivijih aspekata eksperimenta.
VELIKI KORAK, ALI JOŠ NE I KONAČNA POTVRDA
Ukoliko se rezultat nezavisno potvrdi, ovakav sistem mogao bi da predstavlja važan korak ka automatizaciji dela matematičkog istraživanja. Umesto da AI bude samo pomoćnik koji izračunava, pretražuje ili predlaže moguće korake, ovde se ispituje model u kojem veštačka inteligencija samostalno istražuje problem, razvija dokaz. Zatim ga prevodi u oblik koji može formalno da se proveri. To otvara mogućnost za buduće sisteme koji bi mogli da rade na sve složenijim matematičkim pitanjima.
Ipak, tvrdnju treba posmatrati sa oprezom. Rezultat je za sada objavljen kao preprint i nije prošao nezavisnu recenziju stručnjaka. Konačna procena zahteva proveru drugih matematičara. Sam uspeh takođe ne znači da je veštačka inteligencija spremna da rešava najteže probleme matematike bez ljudske pomoći. Ono što ovaj eksperiment za sada pokazuje jeste da AI sve ozbiljnije ulazi u prostor koji je do nedavno bio gotovo isključivo rezervisan za ljudske istraživače. Pitanje je koliko će brzo ovakvi sistemi moći da pređu sa pojedinačnih uspeha na pouzdano samostalno matematičko istraživanje.