Devyni DeepMind įrodymai tikrinami dėl naujumo

Matematinis įrodymas gali būti parašytas įtaigiai ir vis tiek slėpti spragą, kurios niekas nepastebi metų metus. „Google DeepMind“ dirbtinio intelekto agentas „AlphaProof Nexus“ pateikė devynių Paulo Erdošo suformuluotų uždavinių įrodymus, o programinė įranga patikrino kiekvieną žingsnį. Tyrimas pirmiausia paskelbtas gegužę kaip išankstinis straipsnis (arXiv), o po recenzavimo spalio 8 d. publikuotas žurnale „Science“ (Science). Programinė įranga galėjo patvirtinti įrodymų logiką, tačiau spręsti, ar jie pateikė ką nors nauja, teko matematikams.

Tikrintojas, kurio neįtikinsi gražiu tekstu

Pokalbių robotai moka kurti įtikinamai skambančius matematinius argumentus. Užtikrinta pastraipa gali paslėpti trūkstamą žingsnį, kurį pastebės tik atidus skaitytojas. „AlphaProof Nexus“ šios problemos išvengia, nes veikia „Lean“ aplinkoje. Tai programavimo kalba, kuria apibrėžtys, teiginiai ir įrodymai užrašomi taip tiksliai, kad kompiuteris gali juos patikrinti.

Įsivaizduokime „Lean“ kaip recenzentą, tikrinantį kiekvieną užbaigto įrodymo eilutę pagal nustatytas taisykles. Įrodymo stilius nieko nelemia. Jei bent vienas žingsnis neišplaukia iš ankstesnių, įrodymas atmetamas, kad ir kaip sklandžiai būtų parašytas likęs tekstas.

Tyrėjai agentą apibūdina kaip sistemą, ieškančią „Lean“ kalba užrašytų įrodymų. Jie taip pat suteikė jam prieigą prie „AlphaProof“ – ankstesnės „DeepMind“ sistemos, sukurtos būtent įrodymams rasti. Per bandymus paprastesnė sąranka davė tokius pat rezultatus: kalbos modelis kartu su „Lean“, bet be „AlphaProof“, vis tiek rado visų devynių Erdošo uždavinių įrodymus (The Decoder). Šiems uždaviniams specializuoto komponento neprireikė.

Straipsnyje pateikiami devynių Erdošo teiginių įrodymai ir 44 spėjimų iš „Online Encyclopedia of Integer Sequences“ – didžiulio skaičių dėsningumų katalogo – įrodymai (Science). Tarp Erdošo uždavinių – dviejų dalių klausimas apie sveikuosius skaičius, kurį 1970 m. iškėlė Erdošas ir Andrašas Šarkezis. Jis liko neišspręstas daugiau nei pusę amžiaus (ABC).

Ko tikrintojas nemato

„Lean“ garantija turi aiškias ribas: ji patvirtina, kad įrodymas pagrindžia būtent taip, kaip parašytas kode, suformuluotą teiginį. Tačiau lieka trys klausimai: ar kodas perteikia tai, ką turėjo omenyje Erdošas, ar kas nors į šį klausimą jau atsakė anksčiau ir ar atsakymas suteikia naujų žinių.

1970 m. uždavinys parodo, kodėl svarbūs du paskutiniai klausimai. Antroji jo dalis leidžia išvesti pirmąją, todėl vienu įrodymu galima išspręsti abi. Agentui paskelbus įrodymus, paaiškėjo, kad abiem dalims atsakyti pakanka šiek tiek pakeisti konstrukciją iš 1970 m. straipsnio (arXiv). Agento įrodymai buvo teisingi. Tiesiog uždavinys buvo arčiau sprendimo, nei rodė jo „neišspręsto“ statusas.

Tokius dalykus gali pastebėti savo sritį išmanantys žmonės. Gergelis Bėrcis, Danijos „Aarhus University“ matematikas ir vienas iš straipsnio autorių, padėjo atrinkti tinkamus uždavinius ir patikrinti sprendimus (Aarhus University). Jis taip pat padėjo parengti įrodymų versijas, kurias galėtų sekti žmonės. „Lean“ patvirtino kiekvieną žingsnį, o Bėrcis su kolegomis vertino, ką šie žingsniai parodė.

Šis darbo pasidalijimas tyrimą skiria nuo praėjusį mėnesį pasiekto rezultato. Tuomet „Anthropic“ sistema „Claude“ į „Lean“ kalbą perkėlė jau žinomą Ferma paskutinės teoremos įrodymą (To Brief). Žinomo įrodymo perkėlimas nekelia abejonių dėl naujumo. O kai sistema ieško atsakymų į klausimus, laikomus neišspręstais, naujumo patikra tampa pagrindiniu darbu.

Tyrėjai paskelbė įrodymų failus, kad kiti galėtų juos patikrinti ta pačia sistema (GitHub). Šis tyrimas parodo konkretų pasiekimą: dirbtinio intelekto agentas pateikė kompiuteriu patikrinamus įrodymus kai kuriems teiginiams, kuriuos matematikai laikė neišspręstais. „Lean“ garantija galioja būtent taip, kaip tie teiginiai užrašyti kode. Ką šie įrodymai pridėjo prie matematikos, vis tiek sprendė juos skaitę matematikai.