Kai ukrainiečių matematikas Maryna Viazovska gavo a Fieldso medalis– plačiai vertinamas kaip Nobelio matematikos premija – 2022 m. liepos mėn. tai buvo didelė naujiena. Ji ne tik buvo antroji moteris, atsiėmusi šį apdovanojimą per 86 metų istoriją, bet ir atsiėmė medalį praėjus vos mėnesiams po to, kai jos šalį užpuolė Rusija. Po beveik ketverių metų Viazovska vėl kelia bangas. Šiandien, in dėl žmonių ir dirbtinio intelekto bendradarbiavimo, Viazovskos įrodymai buvo anksčiau patikrinti, o tai rodo greitą AI gebėjimų padėti matematikai pažangą.kaliniai tyrimai.
„Šie nauji rezultatai atrodo labai, labai įspūdingi ir neabejotinai rodo tam tikrą sparčią pažangą šia kryptimi“, – sako AI samprotavimo ekspertas ir Prinstono universiteto doktorantas Liamas Fowlas, kuris nedalyvavo darbe.
Savo Fields medaliu laimėjusiame tyrime Viazovska sprendė dvi sferos pakavimo problemos versijas, kurios klausia: kaip tankiai gali būti supakuoti identiški apskritimai, sferos ir kt. n-dimensinė erdvė? Dviejų matmenų korys yra geriausias sprendimas. Trijų matmenų sferos, sukrautos į piramidę, yra optimalios. Tačiau po to tampa nepaprastai sunku rasti geriausią sprendimą ir įrodyti, kad jis iš tikrųjų yra geriausias.
2016 metais Viazovska problemą išsprendė dviem atvejais. Naudodama galingas matematines funkcijas, žinomas kaip (kvazi)modulinės formos, ji įrodė, kad simetriškas išdėstymas, žinomas kaip E.8 yra geriausias 8 dimensijų įpakavimas ir netrukus su bendradarbiais įrodė, kad kitas sferinis sandariklis, vadinamas Leech grotelėmis, yra geriausias pagal 24 matmenis. Nors atrodo abstraktus, šis rezultatas gali padėti išspręsti kasdienes problemas, susijusias su tankiu sferos pakavimu, įskaitant klaidų taisymo kodus, naudojamus išmaniuosiuose telefonuose ir kosminiuose zonduose.
Įrodymai buvo patikrinti matematikos bendruomenės ir pripažinti teisingais, todėl buvo pripažintas Fields medalis. Tačiau formalus patikrinimas – įrodymo galimybė patikrinti kompiuteriu – yra visai kitas žvėris. Nuo 2022 m. padaryta didelė pažanga atliekant AI padedamą oficialų įrodymų patikrinimą.
Serendipity veda į formalizavimo projektą
Po kelerių metų atsitiktinis trečiojo kurso bakalauro Sidharto Hariharano ir Viazovskos susitikimas Lozanoje, Šveicarijoje, vėl paskatins jos susidomėjimą sferų pakavimo įrodymais. Nors Hariharanas dar buvo labai ankstyvas, jis jau buvo įgudęs formalizuoti įrodymus.
„Oficialus įrodymo patikrinimas yra kaip guminis antspaudas“, – sako Fowl. „Tai tam tikras bona fide sertifikatas, patvirtinantis, kad jūs žinote, kad jūsų samprotavimai yra teisingi.
Hariharanas papasakojo Viazovskai, kaip naudojo įrodymų formalizavimo procesą, kad išmoktų ir iš tikrųjų suprastų matematines sąvokas. Atsakydama Viazovska išreiškė susidomėjimą formalizuoti savo įrodymus, daugiausia dėl smalsumo. Iš to 2024 m. kovo mėn. gimė projektas Formalizing Sphere Packing in Lean. Lean yra populiari programavimo kalba ir „įrodymų asistentas“, leidžiantis matematikams rašyti įrodymus, kurių absoliutus teisingumas vėliau patikrinamas kompiuteriu.
Bendradarbiaujant ekspertams Bhavik Mehta (Londono imperatoriškasis koledžas), Christopheris Birkbeckas (Rytų Anglijos universitetas, Anglija), Seewoo Lee (Kalifornijos universitetas, Berklis) ir kiti, projektas apėmė žmonėms skaitomo „projekto“, kurį būtų galima panaudoti 8 dimensijos įrodymo žemėlapiui sudaryti ir kurie vėliau nebuvo formalizuoti ir/kurios buvo formalizuotos jų sudedamosios dalys. įrodant ir įforminant tuos trūkstamus Lean elementus.
„Projekto saugyklą kūrėme maždaug 15 mėnesių, kai 2025 m. birželio mėn. suteikėme viešą prieigą“, – prisimena Hariharanas, dabar pirmą kartą studijuojantis mokslų daktaras. studentas Carnegie Mellon universitete. „Tada spalio pabaigoje pirmą kartą išgirdome iš Math, Inc.“.
AI pagreitis
„Math, Inc.“ yra startuolis, kuriantis „Gauss“ – dirbtinį intelektą, specialiai sukurtą automatiškai formalizuoti įrodymus. „Tai yra tam tikros rūšies kalbos modelis, vadinamas samprotavimo agentu, kuris turi įterpti tradicinius natūralios kalbos samprotavimus ir visiškai formalizuotus samprotavimus“, – aiškina Jesse Han, „Math, Inc.“ generalinis direktorius ir vienas iš įkūrėjų. „Taigi jis gali atlikti literatūros paieškas, iškviesti įrankius ir naudoti kompiuterį, kad užsirašytų Lean kodą, užsirašytų pastabas, susuktų tikrinimo įrankius, paleistų Lean kompiliatorių ir kt.
„Math, Inc.“ pirmą kartą pateko į antraštes, kai paskelbė, kad „Gauss“ baigė „Lean“ formalizavimą pirminio skaičiaus teorema (PNT) per tris savaites praėjusią vasarą – užduotį, kurią atliko Fields medalininkas Terence’as Tao ir Alexas Kontorovičius. Panašiai „Math, Inc.“ susisiekė su Hariharanu ir kolegomis, kad praneštų, kad Gaussas įrodė kelis faktus, susijusius su jų sferos pakavimo projektu.
„Jie mums pasakė, kad baigė 30 „atsiprašau“, o tai reiškė, kad jie įrodė 30 tarpinių faktų, kuriuos norėjome įrodyti“, – aiškina Hariharanas. Dalis šių atsiprašymų buvo pasidalinta su projekto komanda ir sujungta su jų pačių darbu. „Vienas iš jų padėjo mums nustatyti rašybos klaidą mūsų projekte, kurią vėliau ištaisėme“, – priduria Hariharanas. „Taigi tai buvo gana vaisingas bendradarbiavimas“.
Nuo 8 iki 24 matmenų
Tačiau vėliau sekė radijo tyla. Math, Inc. prarado susidomėjimą. Tačiau kol Hariharanas ir jo kolegos tęsė meilės darbą, Math, Inc. kūrė naują ir patobulintą Gauss versiją. „Kažkada sausio viduryje padarėme mokslinių tyrimų proveržį, kuris sukūrė daug stipresnę Gauso versiją“, – sako Hanas. „Ši nauja versija atkartojo mūsų trijų savaičių PNT rezultatą per dvi ar tris dienas.
Po kelių dienų naujasis „Gauss“ buvo nukreiptas atgal į sferos pakavimo formalizavimą. Remdamasis neįkainojamu jau esamu planu ir darbu, kuriuo dalijosi Hariharanas ir bendradarbiai, Gaussas ne tik automatiškai formalizavo 8 matmenų atvejį, bet ir per penkias dienas rado ir ištaisė rašybos klaidą paskelbtame dokumente.
„Kai jie susisiekė su mumis sausio pabaigoje, sakydami, kad, švelniai tariant, baigė, buvome labai nustebinti“, – sako Hariharanas. „Tačiau galų gale tai yra technologija, dėl kurios mes labai džiaugiamės, nes ji gali padaryti puikių dalykų ir puikiai padėti matematikams.
Saulei leidžiantis už Carnegie Mellon Hamerschlag salės, Hariharanas dirbo su sferos pakavimo įrodymu.Sidhartas Hariharanas
Vien tik 8 dimensijos sferos pakavimo įrodymas formalizavimas, paskelbtas vasario 23 d., yra takoskyros momentas automatiniam formalizavimui ir dirbtinio intelekto bei žmogaus bendradarbiavimui. Tačiau šiandien Math, Inc. atskleidė dar įspūdingesnis pasiekimas: Gaussas vos per dvi savaites automatiškai formalizavo Viazovska 24 dimensijų sferos pakavimo įrodymą – visas 200 000 ir daugiau kodo eilučių.
8 ir 24 matmenų atvejai turi bendrų bruožų, kalbant apie pagrindinę teoriją ir bendrą įrodymo architektūrą, o tai reiškia, kad kai kurie kodai iš 8 dimensijų gali būti perdaryti ir panaudoti pakartotinai. Tačiau Gaussas neturėjo iš anksto sukurto plano, kuriuo galėtų dirbti. „Ir tai iš tikrųjų buvo daug labiau įtraukta nei 8 matmenų korpusas, nes trūko daug foninės medžiagos, kuri turėjo būti įtraukta į daugelį Leech grotelių savybių, ypač jos unikalumo“, – aiškina Han.
Nors 24 matmenų atvejis buvo automatizuotas darbas, tiek Hanas, tiek Hariharanas pripažįsta daugybę žmonių, padėjusių šio pasiekimo pamatus, vertindami tai kaip bendrą žmonių ir dirbtinio intelekto pastangą.
Tačiau Hanui tai reiškia dar daugiau: revoliucinės matematikos transformacijos, kur itin didelio masto formalizavimas yra įprastas dalykas, pradžią. „Anksčiau programuotojas buvo tas, kuris išmušdavo skylutes kortelėse, bet vėliau programavimo veiksmas atsiskyrė nuo bet kokio materialaus substrato, kuris buvo naudojamas programoms įrašyti“, – apibendrina jis. „Manau, kad tokios technologijos galutinis rezultatas leis matematikams daryti tai, ką jie moka geriausiai, ty svajoti apie naujus matematinius pasaulius.
Iš jūsų svetainės straipsnių
Susiję straipsniai visame internete
Nuoroda į informacijos šaltinį
