AI model o4-mini impresionirao je matematičare sposobnošću da formuliše uverljive dokaze, ali stručnjaci upozoravaju da takva samouverenost ne znači i tačnost. Rešenje može biti primena formalnih verifikacionih jezika kao što je Lean, koji mašinski proverava svaki korak. Ako AI naučimo da radi zajedno sa formalnim proverama, može rešavati izuzetno složene probleme — ali to otvara i filozofska pitanja o smislu dokaza koje ljudi ne razumeju.
„Dokaz zastrašivanjem“? Kako AI (o4-mini) generiše uverljive — ali ponekad pogrešne — matematičke dokaze
AI is becoming very, very good at solving math proofs, raising the specter that at some point, it will be able to find solutions that even the world's best mathematicians will struggle to understand. . | Credit: James Boldry for Live Science
Na tajnom skupu 2025. godine grupa vodećih svetskih matematičara testirala je najnoviji veliki jezički model kompanije OpenAI, o4-mini. Mnogi su bili zatečeni koliko su odgovori modela zvučali kao izlaganje pravog matematičara: strukturisano, autoritativno i prikladno tehničko.
Zabrinutosti: Uverljiv Stil, Moguće Greške
Iako su komentari bili puni priznanja, pojavila se i važna opreza. Ken Ono, profesor teorije brojeva na Univerzitetu Virdžinije, primetio je da model »iznosi sve s tolikom sigurnošću« da to može dovesti do preuranjenog poverenja. Terence (Terry) Tao iz UCLA upozorio je da je AI dobar u tome da zvuči kao da ima tačan odgovor, ali da ta samouverenost ne garantuje ispravnost.
Fermat proposed what's now known as his "last" theorem in 1637. The 1670 book "Arithmetica" includes Fermat's commentary, which was published after his death. | Credit: Wikimedia Commons
„Ako nešto kažete sa dovoljno autoriteta, ljudi se uplaše. Mislim da je o4-mini savladao 'dokaz zastrašivanjem',“ rekao je Ken Ono.
„Nažalost, AI je mnogo bolji u tome da zvuči kao da ima tačan odgovor nego da ga zapravo ima… uvek će delovati uverljivo,“ upozorio je Terry Tao.
Zašto je to ozbiljno?
Ako matematika ne može da proveri ili razume dokaze, ne možemo iz njih izvesti sigurne nove tehnike. Primera radi, dokaz za problem P vs. NP imao bi ogromne praktične posledice — od optimizacije industrijskih procesa do sigurnosti kriptografije. Ako takvi dokazi potiču iz sistema koje ljudi ne razumeju ili kojima ljudi slepo veruju, to stvara rizik.
Istorijski kontekst i formalna verifikacija
Ljudi često zaboravljaju da su i ljudski dokazi ponekad bili diskutabilni ili nepotpuno dokumentovani. Andrew Granville i drugi ukazuju na slučajeve u kojima su »jezičke nejasnoće« dovele do grešaka. Najpoznatiji primer je rad Endrjua Vajlsa na Fermatovoj poslednjoj teoremi: prvobitno izloženi dokaz je imao ozbiljan propust, koji je kasnije ispravljen.
Andrew Wiles describing his proof of the Taniyama-Shimura Conjecture in 1993. His initial proof contained an error, but he ultimately found a final solution which would lead to him proving Fermat's last theorem. | Credit: Science Photo Library
Da bi se smanjio rizik prihvatanja netačnih ili dvosmislenih rezultata, raste interes za formalnim verifikacionim sistemima kao što je Lean. U formalnoj verifikaciji svaki korak mora biti zapisan u preciznom formalnom jeziku, a mašina proverava logičku doslednost bez jezičkih tumačenja.
„Ako primoramo AI da isporučuje rezultate u formalno verifikovanom jeziku, to bi, u principu, rešilo većinu problema,“ rekao je Tao.
Kevin Buzzard sa Imperial College London zamišlja povratnu petlju u kojoj AI predlaže dokaz, prevodi ga u Lean, Lean prijavljuje greške, a AI pokušava da ih ispravi — proces koji bi mogao ubrzati proveru i popravke.
The four color theorem states that any map can be colored in with just four colors, such that none of the same colors touch each other. It was formally proven, largely using a computer, by 2005. | Credit: Science Photo Library
Posledice: Nove Mogućnosti, Nova Filozofska Pitanja
Ako se AI poveže sa formalnim proverama, može pomoći da se otkriju neočekivane veze između oblasti matematike i da se reše veoma složeni problemi. Marc Lackenby sa Oksforda ističe da AI može uočiti veze koje ljudima ne bi pale na pamet.
S druge strane, postoji realna mogućnost da se razviju »objektivno tačni« dokazi koji su toliko složeni da ih nijedan čovek u potpunosti ne razume. To otvara filozofsko pitanje: ako rezultat više ne možemo razumeti, koliko doprinosi ljudskom znanju i kakva je uloga matematičara u takvom procesu?
Istorija pokazuje da su i ranije postojali slučajevi gde nijedan pojedinac ne razume ceo dokaz — timovi sa desetak ili dvadeset autora gde svako razume svoj deo. I računarski asistirani dokazi (npr. teorema o četiri boje) već su ušli u matematičku praksu. Ipak, razlika je u tome što AI sada može predlagati, prilagođavati i verifikovati dokaze autonomno.
Zaključak
AI menja prirodu matematičkog dokazivanja: od socijalnog procesa ubeđivanja stručnjaka ka potencijalno automatizovanom, formalno verifikovanom procesu. To obezbeđuje moćne alate, ali i zahteva jasno razumevanje granica, odgovornosti i filozofskih implikacija — posebno kada dokazi postanu nerazumljivi ljudima ili kada samouverenost sistema nadjača stvarnu ispravnost.
Pomozite nam da budemo bolji.
