DeepMindi üheksa tõestust vajavad uudsuse kontrolli

Matemaatiline tõestus võib olla ladus ja ikkagi sisaldada viga, mida keegi aastaid ei märka. Google DeepMindi tehisintellektiagent AlphaProof Nexus tõestas üheksa Paul Erdősi püstitatud väidet ning tarkvara kontrollis iga sammu. Uurimus ilmus esmalt mais eeltrükina (arXiv) ja pärast eelretsenseerimist 8. oktoobril ajakirjas Science (Science). Tarkvara sai kontrollida loogikat, kuid otsustada, kas tõestus lisab midagi uut, jäi matemaatikute ülesandeks.

Kontrollija, keda ei saa ära rääkida

Vestlusrobotid oskavad kirjutada matemaatikat, mis kõlab õigesti. Enesekindel tekst võib peita puuduva sammu, mille märkab vaid tähelepanelik lugeja. AlphaProof Nexus väldib seda probleemi, töötades Leanis. See on programmeerimiskeel, milles saab definitsioone, väiteid ja tõestusi esitada nii täpselt, et arvuti saab need üle kontrollida.

Leani võib kujutleda retsensendina, kes loeb valmis tõestuse iga rida ja kontrollib seda kindlate reeglite järgi. Stiil punkte ei anna. Kui üks samm ei tulene eelmistest, kukub tõestus läbi, olgu ülejäänud tekst kui tahes elegantne.

Uurijate sõnul otsib agent Leanis kirjutatud tõestusi. Teadlased andsid sellele kasutada ka AlphaProofi, varasemat DeepMindi süsteemi, mis loodi spetsiaalselt tõestuste leidmiseks. Tiimi katsetes andis sama tulemuse lihtsam lahendus: keelemudel koos Leaniga leidis kõik üheksa Erdősi tõestust ka AlphaProofita (The Decoder). Nende ülesannete puhul osutus spetsiaalne komponent tarbetuks.

Artiklis esitatakse üheksa Erdősi väite ja 44 Online Encyclopedia of Integer Sequences’i oletuse tõestused. Need oletused on väited, mida peetakse tõeseks, kuid mida pole seni tõestatud. Entsüklopeedia koondab arvujadasid ja nende mustreid (Science). Erdősi tulemuste seas on kaheosaline täisarvude ülesanne, mille tema ja András Sárközy püstitasid 1970. aastal. See jäi lahendamata üle pooleks sajandiks (ABC).

Mida kontrollija ei näe

Lean tagab täpselt ühe asja: tõestus kinnitab väidet nii, nagu see on koodis kirjas. Kolm küsimust jäävad sellest välja: kas kood väljendab seda, mida Erdős mõtles, kas keegi lahendas ülesande juba ammu ja kas tulemus lisab matemaatikale midagi.

1970. aasta ülesanne näitab, miks kaks viimast küsimust tähtsad on. Teise osa lahendus annab vastuse ka esimesele. Pärast agendi tõestuste levikut selgus, et mõlemale osale vastab ka väike muudatus algse 1970. aasta artikli konstruktsioonis (arXiv). Agendi tõestused olid korrektsed. Ülesanne oli lihtsalt lahendusele lähemal, kui selle „lahtine“ staatusest paistis.

Selliste varasemate lahenduste leidmiseks on vaja valdkonda tundvaid inimesi. Gergely Bérczi, Taanis asuva Aarhus University matemaatik ja üks artikli autoreid, aitas valida sobivaid ülesandeid ning lahendusi kontrollida (Aarhus University). Ta aitas kirjutada ka tõestuste versioone, mida inimene saab jälgida. Lean kontrollis iga sammu, Bérczi ja tema kolleegid hindasid, mida need sammud kokku tähendavad.

See töö erineb eelmisel kuul kirjeldatud saavutusest. Siis vormistas Anthropic’u Claude Leanis Fermat’ suure teoreemi juba tuntud tõestuse (To Brief). Tuntud tõestuse teisendamine ei tekita küsimust selle uudsusest. Lahtiseks peetud väidete puhul tuleb aga kontrollida, kas tulemus on tõesti uus. Seetõttu sai uudsuse hindamisest töö keskne osa.

Tiim avaldas tõestuste failid, et teised saaksid neid sama tarkvaraga kontrollida (GitHub). Uuringu tulemus on konkreetne: tehisintellektiagent koostas masinaga kontrollitavad tõestused mõnele väitele, mida matemaatikud olid pidanud lahendamata küsimusteks. Garantii kehtib nende väidete kohta nii, nagu need Leanis kirja pandi. Matemaatikutele jäi hinnata, mida iga tõestus valdkonda lisas.