Lean kinnitas Claude’i hiiglasliku Fermat’ tõestuse

Maailma matemaatikute kasutatav tõestuste kontrollimise tarkvara Lean kinnitas Fermat’ suure teoreemi täieliku formaalse tõestuse. Anthropic Claude’i süsteemiga loodud ja avalikus repositooriumis avaldatud formaliseeringus pole lahendamata vaheetappe, täiendavaid aksioome ega arvutuslikke otseteid väljaspool Leani standardseid aluseid (repository). Imperial College Londoni matemaatik Kevin Buzzard, kes juhtis oma formaliseerimisprojekti, kompileeris töö sõltumatult ja kinnitas, et Lean võtab tõestuse vastu. Buzzard nimetas tulemust „erakordseks autoformaliseerimise saavutuseks” (Buzzard).

Matemaatiline küsimus lahendati juba ammu. Andrew Wiles tõestas teoreemi 1995. aastal ning matemaatikute seas ei olnud tulemuse õigsuses sisulist kahtlust. Puudu oli tõestuse esitamine sõnasõnalisele kontrolliprogrammile arusaadavate juhistena, koos kõigi definitsioonide ja vaheetappidega, mille inimene võib tekstis vaikimisi eeldada. Anthropicu teatel tegid kümned tehisintellektiagendid selle töö augustis 11 päevaga, kasutades paralleelseks tegutsemiseks platvormi Prove2Me (Anthropic).

11-päevast tööprotsessi ei saa kõrvalised osapooled siiski korrata. Avalikustatud pole sisemist mudelit, agentide juhtimise taristut, operaatorite otsuseid ega kasutatud arvutusressurssi. Korratav on lõpptulemus: piisava riistvaraga saab igaüks Leani projekti uuesti kompileerida ja kontrollida, kas tõestus läbib kontrolli. Anthropicu Rustis kirjutatud eraldiseisev kontrollprogramm jõudis sama formaalse artefakti puhul samale tulemusele ning kinnitas kõigi 1 052 234 deklaratsiooni kooskõla (technical report). Tegemist on sama teksti teise kontrolliga, mitte 11-päevase tööprotsessi sõltumatu kordamisega.

Kuidas agendid töötasid

Tõestuse formaliseerimisel kirjutatakse matemaatiku arutluskäik ümber kujule, milles matemaatilise vaistuta programm saab kontrollida iga loogilist sammu. Teoreemi väide ise on petlikult lihtne: kui täisarvuline astendaja on vähemalt kolm, ei leidu positiivseid täisarve, mille korral aⁿ + bⁿ = cⁿ. Tõestus liigub aga läbi arvuteooria süvakihtide ja ulatub sadadele lehekülgedele.

Claude ei avastanud uut matemaatikat. Süsteem formaliseeris Wilesi tõestuseni viiva teadaoleva tulemuste ahela, lähtudes matemaatikute Henri Darmoni, Fred Diamondi ja Richard Taylori käsitlusest (Anthropic, technical report). Loominguline läbimurre kuulus Wilesile ja tema eelkäijatele. Claude teisendas nende mõttekäigu ligikaudu 10,5 miljoniks reaks masinloetavaks koodiks (technical report).

Anthropicu teaduri Tianyi Pengi ja Columbia University kaastöötajate loodud Prove2Me jagas tõestuse sõltuvusgraafiks, mis koosnes umbes 29 511 eraldiseisvast väitest (technical report). Agendid valisid väiteid, mille eeldused olid juba tõestatud, kirjutasid neile Leani tõestused ning kontrollisid üksteise sõnastatud väiteid. Paralleelse töö käigus genereeris sisemine uurimismudel ligikaudu kuus miljardit väljundtokenit (technical report).

Anthropicu sõnul ei kirjutanud inimesed töö käigus Leani koodi. Operaatorid valisid siiski teoreemi ja teadaoleva tõestuskäigu, kujundasid agentide taristu ning muutsid aeg-ajalt ülesannete prioriteete (Anthropic). Operaatorite täielikku tegevuslogi ega arvutusressursi maksumust ettevõte ei avaldanud.

Tulemus tugines aastatepikkusele inimtööle

Töö tugines Mathlibile, kogukonna hallatavale mahukale formaliseeritud matemaatika teegile, ning kasutas otseselt kahe varasema projekti tulemusi. Buzzardi töörühm Imperial College’is oli Fermat’ suure teoreemi Leani-formaliseeringut arendanud alates 2023. aasta lõpust. Projekti rahastas 1 miljoni naela suuruse toetusega EPSRC ning töö pidi kestma 2029. aastani (EPSRC award). Eraldi kogukonnaprojekt oli teoreemi osa juhtumeid juba formaliseerinud. Anthropicu omistamisfaili järgi sisaldab 106 faili nendest töödest võetud või nende põhjal kohandatud materjali (attribution).

Paralleeltöö tõttu ei saa 11 kalendripäeva võrrelda Buzzardi meeskonna töötundidega. Claude’i töö alguseks oli inimeste projekt saanud rahastust ligikaudu 22 kuud (EPSRC award). Anthropic ei avaldanud kasutatud graafikaprotsessorite töötunde ega energiakulu.

Enne Anthropicu töö avaldamist oli Fermat’ suur teoreem viimane formaliseerimata tulemus Freek Wiedijki saja olulise teoreemi nimekirjas, millega on formaliseerimise arengut jälgitud kaks aastakümmet (Buzzard).

Meetodi üldistatavuse kõige nõudlikum proov on uuemate ja vähem dokumenteeritud matemaatiliste tulemuste formaliseerimine olukorras, kus puuduvad valmis tegevuskava, küpsed teegid ja varasem formaliseerimistöö. Praegune katse käsitles kuulsat teoreemi, mille jaoks oli suur osa taristust juba olemas. Tulemus näitab, et teadaoleva tõestuskäigu ja varasema formaliseerimistöö toel suudavad tehisintellektiagendid koostada tervikliku tõestuse, mille Lean vastu võtab ja mida kõrvalised osapooled saavad kontrollida. Avaldatud materjalist ei piisa aga tõestuse loomise protsessi kordamiseks.