Kompanija Anthropic saopštila je da je njen AI model Claude za 11 dana, radeći najvećim delom samostalno, napisao prvi potpuno proverljiv, kompjuterski proveren dokaz Fermatove poslednje teoreme u programskom jeziku Lean. Rezultat je objavljen 4. septembra, a nezavisno ga je proverio matematičar Kevin Buzzard sa Imperijal koledža u Londonu, čiji je raniji rad Claude koristio kao osnovu.
Fermatova poslednja teorema, formulisana još 1637. godine, ostala je nerešena tri i po veka dok je britanski matematičar Endru Vajls nije dokazao 1995. u radu od 129 strana. Formalizacija tog dokaza, odnosno njegovo prevođenje u kod koji softver za proveru dokaza Lean može automatski da potvrdi, smatrana je zadatkom za koji bi ljudskim matematičarima bile potrebne godine.
Kako je nastao dokaz od 13 miliona linija koda
Za posao je korišćen interni istraživački model uporediv sa Claude Fable 5.1, koji je radio preko platforme Prove2Me. Reč je o otvorenoj kolaborativnoj platformi za formalizaciju matematike koju su napravili Tianji Peng i saradnici sa Univerziteta Kolumbija. Prove2Me održava usmereni acikličan graf matematičkih tvrđenja i koordiniše rad više Claude agenata istovremeno, dodeljujući im teoreme na dokazivanje prema tome koje su već dostupne kao gradivni blokovi.
Ljudski doprinos sveden je na povremene instrukcije visokog nivoa, poput napomene da je prioritet dokazati Jakobijan kao šemu ili ubrzati rad na Mazurovoj teoremi. Sve ostalo, uključujući strategiju dokazivanja i ispravljanje sopstvenih grešaka, agenti su obavili sami. Krajnji rezultat ima 13 miliona linija Lean koda, pet puta više od biblioteke Mathlib, sadrži 30.300 dokazanih teorema od kojih je 29.500 iskorišćeno u finalnom dokazu, a proces je potrošio oko šest milijardi izlaznih tokena.
Šta dokaz zapravo predstavlja
Claude nije otkrio novu matematiku, već je formalizovao pojednostavljenu verziju Vajlsovog dokaza koju su ranije razvili Anri Darmon, Fred Dajmond i Ričard Tejlor. Formalizacija ne menja sadržaj dokaza, ali eliminiše mogućnost ljudske greške u proveri i omogućava matematičarima da tvrđenja proveravaju automatski, umesto da mesecima ručno prelaze stranicu po stranicu. Kevin Buzzard je ocenio da rezultat „dokazuje Fermatovu poslednju teoremu bez ijedne pretpostavke sem aksioma matematike”.
Anthropic je naveo i ograničenja rada. Oko sedam odsto linija koda koje nisu čist šablon poteklo je iz neuspešnih pokušaja koje je model kasnije morao da ispravi, a sam dokaz je, zbog načina na koji ga je AI generisao, verovatno duži nego što bi morao da bude da ga je pisao čovek. Buzzard je ipak poručio da su „artefakti AI autoformalizacije sada dovoljno pouzdani da se na njima može graditi dalje”. U matematičkoj zajednici i dalje se vodi rasprava o tome koliko formalizovani dokazi menjaju svakodnevni rad matematičara, budući da najveći deo discipline i dalje počiva na intuiciji i saradnji koju kod, makar i proveren, ne zamenjuje.
Deo šireg zamaha Anthropica ka nauci
Projekat se uklapa u niz poteza kojima Claude poslednjih meseci sve češće izlazi iz uloge asistenta za pisanje i programiranje i ulazi u istraživački rad. Anthropic je ranije tvrdio da je Claude dizajnirao proteine bolje od stručnjaka, a kompanija je i besplatan pristup Claude-u ponudila za 10.000 naučnika kako bi podstakla upravo ovakve primene. Kompanija tim demonstracijama gradi argument da njeni modeli mogu da ubrzaju stvarni naučni rad, u trenutku kada priprema javno podnošenje IPO dokumentacije i mora investitorima da pokaže konkretnu vrednost izvan chatbota. Slične poteze poslednjih meseci povlače i konkurenti, pa se demonstracije autonomnog istraživačkog rada sve više koriste kao argument u utrci za poverenje kako investitora tako i naučnih institucija.
Često postavljana pitanja
Šta je Fermatova poslednja teorema?
Tvrđenje iz 1637. godine da jednačina x na n plus y na n jednako z na n nema rešenja u celim brojevima različitim od nule kada je n veće od dva. Dokazao ju je Endru Vajls tek 1995. godine.
Šta znači da je dokaz formalizovan?
Formalizacija je prevođenje matematičkog rezonovanja u kod koji softver za proveru dokaza, u ovom slučaju Lean, može automatski i sa apsolutnom sigurnošću da potvrdi, bez oslanjanja na ručnu proveru recenzenata.
Da li je Claude otkrio novu matematiku?
Ne. Model je formalizovao već poznat, pojednostavljeni oblik Vajlsovog dokaza, koji su ranije razvili drugi matematičari. Doprinos je u brzini i preciznosti formalizacije, ne u novom matematičkom otkriću.
Ko je proverio da je dokaz tačan?
Sam Lean sistem je automatski proverio ispravnost svake teoreme, a matematičar Kevin Buzzard sa Imperijal koledža u Londonu nezavisno je pregledao rezultat i potvrdio njegovu validnost.
Da li je Prove2Me javno dostupan?
Da, reč je o otvorenoj platformi koju su razvili Tianji Peng i saradnici sa Univerziteta Kolumbija, a namenjena je koordinaciji AI agenata i ljudi na zajedničkim projektima formalizacije matematike.
