DeepMind deviņi pierādījumi: vai tie ir jauni?

Matemātisks pierādījums var būt eleganti uzrakstīts, bet tajā tik un tā var slēpties kļūda, ko gadiem neviens nepamana. Google DeepMind mākslīgā intelekta aģents AlphaProof Nexus sagatavoja pierādījumus deviņiem Pola Erdoša uzdevumiem, un programmatūra pārbaudīja katru soli. Pētījums maijā vispirms parādījās kā priekšpublikācija (arXiv), bet pēc recenzēšanas 8. oktobrī tika publicēts žurnālā Science (Science). Programmatūra varēja apstiprināt pierādījumu loģiku, bet to, vai tā dod ko jaunu, vērtēja matemātiķi.

Pārbaudītājs, ko nepārliecina daiļrunība

Tērzēšanas roboti prot radīt matemātiskus tekstus, kas izklausās pareizi. Pārliecinošs formulējums var noslēpt izlaistu pierādījuma soli, ko pamana tikai rūpīgs lasītājs. AlphaProof Nexus no šīs problēmas izvairās, strādājot ar Lean — programmēšanas valodu, kurā definīcijas, apgalvojumus un pierādījumus var pierakstīt tik precīzi, ka tos pārbauda dators.

Lean var iztēloties kā tiesnesi, kas izskata katru gatavā pierādījuma rindu un piemēro fiksētus noteikumus. Par stilu punktus nedod. Ja viens solis neizriet no iepriekšējiem, pierādījums neiztur pārbaudi, lai cik eleganti būtu pārējie.

Pētnieki aģentu raksturo kā sistēmu, kas meklē Lean valodā uzrakstītus pierādījumus. Viņi tam deva piekļuvi arī AlphaProof — agrākai DeepMind sistēmai, kas izstrādāta tieši pierādījumu meklēšanai. Pētnieku testos vienkāršāks risinājums deva to pašu rezultātu: valodas modelis kopā ar Lean, neizmantojot AlphaProof, ieguva visus deviņus Erdoša uzdevumu pierādījumus (The Decoder). Šiem uzdevumiem specializētais komponents izrādījās lieks.

Rakstā aprakstīti pierādījumi, ko programmatūra pieņēma par korektiem, deviņiem Erdoša apgalvojumiem un 44 pieņēmumiem no Online Encyclopedia of Integer Sequences — plaša skaitļu virkņu kataloga. Pieņēmumi ir apgalvojumi, ko uzskata par patiesiem, bet kas vēl nav pierādīti (Science). Viens no Erdoša rezultātiem atbild uz divdaļīgu jautājumu par nenegatīviem veseliem skaitļiem, ko Erdošs un Andrašs Sārkezi uzdeva 1970. gadā. Tas palika neatrisināts vairāk nekā pusgadsimtu (ABC).

Ko pārbaudītājs nespēj izvērtēt

Lean garantijai ir skaidras robežas: tā apliecina, ka pierādījums pierāda tieši to apgalvojumu, kas uzrakstīts kodā. Taču tā neatbild uz trim jautājumiem: vai kods precīzi atspoguļo Erdoša ieceri, vai kāds uz jautājumu nav atbildējis jau sen un vai atbilde dod ko jaunu.

1970. gada uzdevums parāda, kāpēc svarīgi ir pēdējie divi jautājumi. Atbilde uz otro daļu atrisina arī pirmo. Kad aģenta pierādījumi kļuva pieejami, atklājās, ka abas daļas var atrisināt arī ar nelielu labojumu konstrukcijā no sākotnējā 1970. gada raksta (arXiv). Aģenta pierādījumi bija korekti, bet uzdevums bija tuvāk atrisinājumam, nekā liecināja tā statuss „neatrisināts”.

Lai to pamanītu, vajadzīgi attiecīgās nozares speciālisti. Gergeljs Bērci, Dānijas Orhūsas Universitātes matemātiķis un viens no pētījuma autoriem, palīdzēja izvēlēties piemērotus uzdevumus un pārbaudīt risinājumus (Aarhus University). Viņš palīdzēja arī sagatavot pierādījumu versijas, kurām var izsekot cilvēks. Lean pārbaudīja katra soļa loģisko korektumu, bet Bērci un kolēģi vērtēja, ko pierādījumi nozīmē matemātikai.

Šāds darba sadalījums atšķir šo pētījumu no pagājušā mēneša sasnieguma. Toreiz Anthropic modelis Claude Lean valodā pārrakstīja jau zināmo Ferma pēdējās teorēmas pierādījumu (To Brief). Jau zināma pierādījuma pārnešana jaunā pieraksta valodā nerada jautājumu par tā novitāti. Meklējot risinājumus apgalvojumiem, ko uzskata par neatrisinātiem, vispirms jānoskaidro, vai tie tiešām vēl ir neatrisināti.

Pētnieki publicējuši pierādījumu failus, lai citi varētu tos pārbaudīt ar to pašu programmatūru (GitHub). Šis pētījums parāda konkrētu iespēju: mākslīgā intelekta aģents sagatavoja datorā pārbaudāmus pierādījumus dažiem apgalvojumiem, ko matemātiķi uzskatīja par neatrisinātiem. Garantija attiecas uz šo apgalvojumu formulējumu Lean valodā. Savukārt to, ko katrs pierādījums devis matemātikai, joprojām vērtēja matemātiķi, kas tos izlasīja.