Od nagađanja do formalnih dokaza: OpenAI Astra rešava matematičke probleme uz Lean verifikaciju

OpenAI je objavio da je novi model Astra samostalno rešio 10 otvorenih problema u matematici i teorijskom računarstvu. Rešenja su u potpunosti formalizovana kroz matematički sistem Lean, čime je eliminisan problem halucinacija koji je godinama pratio generativne modele. Ceo proces zahtevao je izuzetno niske računarske resurse, što otvara novo poglavlje u primeni veštačke inteligencije u teorijskim naukama.

Šta je tačno rešeno?

Model Astra uspeo je da pruži kompletna i proverljiva rešenja za teorijske zagonetke koje su decenijama bile nerešene. Među postignutim rezultatima nalaze se ključni proboji u nekoliko različitih matematičkih oblasti:

• Rešavanje kompleksnih problema pakovanja sfera u višim dimenzijama.
• Novi rezultati u proučavanju takozvanih ne-sofičkih grupa.
• Uspešno rešavanje specifičnih problema koje je postavio čuveni matematičar Paul Erdős.

Za razliku od standardnih jezičkih modela koji generišu tekst na osnovu statističke verovatnoće naredne reči, Astra je generisala formalni kod koji direktno komunicira sa softverom za verifikaciju dokaza.

Kraj halucinacijama kroz Lean verifikaciju

Glavni nedostatak velikih jezičkih modela u egzaktnim naukama bila je sklonost ka uverljivom izmišljanju činjenica i netačnih logičkih koraka. OpenAI je ovaj problem prevazišao integracijom modela Astra sa sistemom Lean.

Lean funkcioniše kao rigorozni interaktivni dokazivač teorema. On automatski proverava svaki pojedinačni korak u izvođenju dokaza, primenjujući striktna aksiomatska pravila. Ukoliko postoji i najmanja logička greška, sistem odbacuje celo rešenje. Činjenica da su svi dokazi modela Astra dobili Lean sertifikate garantuje stopostotnu matematičku tačnost, bez potrebe za ljudskim nagađanjem da li je model negde napravio previd.

Trošak od samo 2.000 dolara

Osim teorijskog proboja, podjednako je značajna i ekonomska efikasnost ovog poduhvata. Ukupan trošak inferencije za rešavanje svih deset otvorenih problema iznosio je svega 2.000 dolara putem Sol API platforme.

Ova brojka pokazuje da formalno dokazivanje uz pomoć veštačke inteligencije više ne zahteva višemilionske budžete niti superkompjutere rezervisane isključivo za uski krug istraživačkih laboratorija. Time je omogućen prelazak sa klasičnog prepoznavanja obrazaca na automatizovano, rigorozno i jeftino deduktivno zaključivanje.

Širi kontekst za nauku

Ovakav uspeh odmah je pokrenuo rasprave unutar globalne matematičke zajednice. Otvorena su važna pitanja o prirodi naučnog autorstva kada softver samostalno kreira formalni dokaz od početka do kraja.

Dok jedni istraživači vide Lean i modele poput Astre kao ultimativne alate koji će ubrzati otkrića u fizici, kriptografiji i računarstvu, drugi ukazuju na potrebu redefinisanja uloge matematičara. Umesto ručnog izvođenja koraka, uloga naučnika se sve više pomera ka postavljanju pravih pitanja i kreiranju hipoteza koje mašine zatim mogu formalno da potvrde ili opovrgnu.