DeepMindovih devet dokaza: jesu li novi?

Matematički dokaz može biti elegantan, a ipak skrivati propust koji nitko ne primijeti godinama. DeepMindov agent umjetne inteligencije AlphaProof Nexus izradio je dokaze za devet problema koje je postavio Paul Erdős, a računalni je program provjerio svaki korak. Rad je najprije objavljen kao preprint u svibnju (arXiv), a nakon recenzije u časopisu Science 8. listopada (Science). Program je mogao potvrditi logiku dokaza, ali jesu li oni donijeli nešto novo morali su procijeniti matematičari.

Provjeravatelj kojeg stil ne može zavarati

Chatbotovi mogu napisati matematičko obrazloženje koje zvuči uvjerljivo, iako samouvjeren odlomak može prikriti preskočen korak koji će uočiti samo pažljiv čitatelj. AlphaProof Nexus taj problem izbjegava radom u programskom jeziku Lean, u kojem se definicije, tvrdnje i dokazi zapisuju dovoljno precizno da ih računalo može provjeriti.

Zamislite Lean kao recenzenta koji čita svaki redak dovršenog dokaza i primjenjuje unaprijed zadana pravila. Stil mu ne donosi bodove: ako jedan korak ne proizlazi iz prethodnih, dokaz pada, ma koliko ostatak bio elegantan.

Tim opisuje agenta kao sustav koji traži dokaze zapisane u jeziku Lean. Istraživači su mu omogućili i pristup sustavu AlphaProof, ranijem DeepMindovu alatu izrađenom posebno za dokazivanje matematičkih tvrdnji. U testovima tima, isti su rezultati postignuti i jednostavnijom postavom: jezični model uparen s Leanom, bez AlphaProofa, pronašao je svih devet Erdősovih dokaza (The Decoder). Za te se probleme specijalizirani sustav pokazao nepotrebnim.

U radu se navode prihvaćeni dokazi za devet Erdősovih tvrdnji i za 44 pretpostavke iz Online Encyclopedia of Integer Sequences, opsežnog kataloga nizova brojeva (Science). Među Erdősovim rezultatima odgovor je na dvodijelni problem o cijelim brojevima koji su Erdős i András Sárközy postavili 1970. Problem je ostao neriješen više od pola stoljeća (ABC).

Što Lean ne može vidjeti

Leanovo jamstvo ima jasnu granicu: potvrđuje da se tvrdnja dokazuje upravo onako kako je zapisana u kodu. Izvan te provjere ostaju tri pitanja: odgovara li kod onome što je Erdős namjeravao pitati, je li netko na pitanje već davno odgovorio i donosi li rješenje nešto novo.

Problem iz 1970. pokazuje zašto su važna posljednja dva pitanja. Njegov drugi dio podrazumijeva prvi, pa jedan dokaz rješava oba. Nakon što su agentovi dokazi postali dostupni, pokazalo se da i mala izmjena konstrukcije iz izvornog rada iz 1970. odgovara na oba dijela (arXiv). Dokazi agenta bili su točni; problem je samo bio bliži rješenju nego što je sugerirala oznaka „otvoren”.

Za takvu procjenu potrebno je poznavanje područja. Gergely Bérczi, matematičar sa Sveučilišta Aarhus u Danskoj i jedan od autora, pomogao je odabrati prikladne probleme i procijeniti valjanost rješenja (Aarhus University). Pomogao je i u pisanju verzija dokaza koje ljudi mogu pratiti. Lean je potvrdio svaki korak, a Bérczi i njegovi kolege procijenili su što ti koraci znače za matematiku.

Ta podjela posla razlikuje ovu studiju od prošlomjesečnog rezultata. Tada je Claude tvrtke Anthropic zapisao već poznati dokaz Fermatova posljednjeg teorema u Leanu (To Brief). Prijenos slavnog dokaza u Lean ne otvara pitanje novosti. Potraga među tvrdnjama koje se smatraju neriješenima otvara ga, pa provjera novosti postaje ključni dio posla.

Tim je objavio datoteke s dokazima kako bi ih drugi mogli provjeriti istim sustavom (GitHub). Studija pokazuje konkretan pomak: agent umjetne inteligencije izradio je računalno provjerljive dokaze za neke tvrdnje koje su matematičari smatrali neriješenima, a jamstvo se odnosi na te tvrdnje onako kako su zapisane u Leanu. Matematičari koji su dokaze čitali i dalje su morali procijeniti što su oni dodali matematici.