DeepMindovih devet dokazov na preizkusu novosti

Matematični dokaz je lahko videti brezhiben, pa v njem leta nihče ne opazi vrzeli. Agent umetne inteligence AlphaProof Nexus družbe Google DeepMind je pripravil dokaze za devet problemov, ki jih je zastavil Paul Erdős, programska oprema pa je preverila vsak korak. Delo je bilo najprej objavljeno v majski predobjavi (arXiv), po strokovnem recenziranju pa 8. oktobra še v reviji Science (Science). Programska oprema je lahko potrdila pravilnost dokazov, o tem, ali prinašajo kaj novega, pa so presojali matematiki.

Preverjevalnik, ki ga ni mogoče očarati

Klepetalniki znajo napisati matematiko, ki zveni prepričljivo. Samozavesten odstavek lahko prikrije manjkajoči korak, ki ga opazi le pozoren bralec. AlphaProof Nexus se tej pasti izogne, ker dela v jeziku Lean, v katerem so definicije, trditve in dokazi zapisani tako natančno, da jih lahko preveri računalnik.

Lean si lahko predstavljamo kot sodnika, ki prebere vsako vrstico končanega dokaza in preverja, ali sledi določenim pravilom. Slog ne prinaša točk. Če kak korak ne izhaja iz prejšnjih, dokaz pade, pa naj bo preostanek še tako eleganten.

Ekipa opisuje agenta kot sistem, ki išče dokaze, zapisane v jeziku Lean. Raziskovalci so mu omogočili tudi uporabo AlphaProofa, prejšnjega sistema DeepMinda, zasnovanega posebej za dokazovanje. V preizkusih ekipe je preprostejša postavitev dala enak rezultat: jezikovni model v kombinaciji z Leanom, brez AlphaProofa, je prav tako našel dokaze za vseh devet Erdősovih problemov (The Decoder). Za te probleme se je specializirana komponenta izkazala za nepotrebno.

Članek poroča o sprejetih dokazih za Erdősove trditve in 44 domnev (trditev, za katere velja, da so resnične, vendar še niso dokazane) iz Online Encyclopedia of Integer Sequences, obsežnega kataloga številskih vzorcev (Science). Med Erdősovimi rezultati je tudi dvodelno vprašanje o celih številih, ki sta ga Erdős in András Sárközy zastavila leta 1970. Odgovor nanj je manjkal več kot pol stoletja (ABC).

Česa preverjevalnik ne more videti

Jamstvo Leana ima natančno določene meje: potrdi, da dokaz velja za trditev natanko tako, kot je zapisana v kodi. Ne more pa odgovoriti na tri vprašanja: ali koda zajame to, kar je imel v mislih Erdős, ali je kdo na vprašanje odgovoril že pred tem in ali rešitev prinaša novo spoznanje.

Problem iz leta 1970 kaže, zakaj sta pomembni zadnji dve vprašanji. Njegov drugi del pomeni tudi rešitev prvega, zato en dokaz razreši oba. Ko so agentovi dokazi zaokrožili, se je pokazalo, da na oba dela odgovori že manjša prilagoditev konstrukcije iz izvirnega članka iz leta 1970 (arXiv). Dokazi agenta so bili pravilni; problem je bil bliže rešitvi, kot je nakazovala oznaka »odprt«.

Za takšno presojo so potrebni ljudje, ki poznajo področje. Gergely Bérczi, matematik na Univerzi v Aarhusu na Danskem in eden od avtorjev, je pomagal izbrati primerna vprašanja in potrditi rešitve (Aarhus University). Pomagal je tudi pripraviti različice dokazov, ki jim lahko sledijo človeški bralci. Lean je potrdil vsak korak, Bérczi in njegovi sodelavci pa so presodili, kaj ti koraki pomenijo kot celota.

Ta razdelitev dela loči študijo od pomembnega dosežka prejšnjega meseca. Tedaj je Claude družbe Anthropic že znani dokaz Fermatovega zadnjega izreka pretvoril v zapis za Lean (To Brief). Pri prevodu znanega dokaza novost ni vprašljiva. Iskanje med trditvami, ki veljajo za nerešene, jo postavi v ospredje, zato preverjanje novosti postane glavni del presoje.

Ekipa je objavila datoteke z dokazi, zato jih lahko drugi preverijo z istim sodnikom (GitHub). Študija kaže omejeno, a konkretno zmožnost: agent umetne inteligence je pripravil strojno preverljive dokaze za nekatere trditve, ki so jih matematiki obravnavali kot nerešene. Jamstvo velja za te trditve, zapisane v Leanu. Kaj je posamezni dokaz prispeval k matematiki, so še vedno presojali matematiki, ki so ga prebrali.