Microsoft tyrėjas ir jo bendradarbis sujungė naujas matematines idėjas su žmogaus valdomu dirbtiniu intelektu ir išsprendė centrinę aukštamatės geometrijos ir tikimybių teorijos problemą
Trumpai
- Esminis mokslinis proveržis: tyrėjai įrodė Kannano–Lovászo–Simonovitso (KLS) hipotezę – 31 metus neįveiktą problemą, plačiai laikomą vienu svarbiausių neatsakytų aukštamatės geometrijos klausimų, kurio pasekmės siekia statistiką, optimizavimą, algoritmus ir informatiką.
- Universalus geometrinis principas: rezultatas nustato universalų log-iškilųjų skirstinių geometrinį principą: paprasti plokšti pjūviai gali nustatyti siauriausias tokių skirstinių „kakleliu“ su pastoviu koeficientu, nepriklausomai nuo dimensijų skaičiaus.
- Žmogaus ir DI bendradarbiavimas: proveržis gimė žmogaus valdomame agentiniame tyrimo procese, kuriame DI sistemos tyrinėjo matematines galimybes, o tyrėjai vertino, atsijojo ir nukreipė paiešką.
- Nepriklausomas patvirtinimas: keli nepriklausomi tyrėjai patikrino šį darbą ir nurodė jo pagrindinį kriterijų kaip esminį proveržį, o vėliau rezultatas buvo patvirtintas mašininiu formaliuoju patikrinimu.
Dešimtmečius pagrindinis klausimas apie skaičiavimų sudėtingumą aukštamatėse erdvėse nepasidavė įrodymui. Naujas tyrimas šį klausimą išsprendžia ir pašalina didelę teorinę kliūtį suprasti atsitiktinių algoritmų, naudojamų visame moksle ir skaičiavimuose, efektyvumą.
Kannano–Lovászo–Simonovitso (KLS) hipotezė buvo iškelta 1995 metais. Ji klausia, ar plačios aukštamačių tikimybinių skirstinių klasės atveju geriausias plokščias pjūvis (hiperplokštuma) visada yra beveik toks pat veiksmingas kaip geriausias bet kokios formos pjūvis. Tiksliau, KLS numato, kad šie du dydžiai skiriasi ne daugiau nei universalia konstanta, nepriklausomai nuo dimensijų skaičiaus. Tai nustatytų nuo dimensijų nepriklausomą geometrinį principą, svarbų aukštamatei geometrijai, tikimybių teorijai ir teorinei informatikai. Kadangi šių pjūvių geometrija lemia, kaip greitai atsitiktiniai klaidžiojimai gali ištyrinėti skirstinį, KLS taip pat vaidina pagrindinį vaidmenį aukštamačio mėginių ėmimo teorijoje.
Paaiškinimas: Aukštamatė erdvė – tai erdvė, kurioje objektai aprašomi labai daugeliu parametrų (koordinačių), todėl įprasta geometrinė intuicija joje dažnai nebegalioja. Tokios erdvės būdingos duomenų analizei ir mašininiam mokymuisi.
Nuo 1995 metų matematikai kaupė įrodymų, kad hipotezė teisinga, tačiau pilno įrodymo trūko. Dabar du tyrėjai, tarp jų Xinzhi Zhang iš Microsoft Research Mašininio mokymosi ir optimizavimo grupės, įrodė KLS hipotezę (atidaroma naujame skirtuke). Jie parodė, kad šis sąryšis galioja su pastoviu rėžiu, nesvarbu, kiek dimensijų turi figūra. Prieš šį darbą geriausias žinomas rezultatas (atidaroma naujame skirtuke), gautas 2026 m. liepos mėnesį, leido šiam rėžiui lėtai augti didėjant dimensijų skaičiui. Šis darbas nustato esminį geometrinį principą: aukštamatės erdvės yra geriau „valdomos“, nei buvo manyta, o kliūtys jose judėti neauga be ribų didėjant dimensijoms.
KLS hipotezės svarba buvo pripažįstama visoje srityje dar gerokai prieš ją išsprendžiant. Savo 2017–18 m. metinėje ataskaitoje Matematikos mokslų tyrimų institutas (MSRI) (atidaroma naujame skirtuke) pavadino ją „centrine neišspręsta aukštamatės iškilosios geometrijos problema“. Simonso institutas (atidaroma naujame skirtuke) apibūdino ją kaip „vieną svarbiausių neišspręstų iškilosios geometrijos problemų“. 2022 m. Tarptautinio matematikų kongreso (ICM) (atidaroma naujame skirtuke) darbuose Ronenas Eldanas atkreipė dėmesį į plačias hipotezės pasekmes aukštamatei iškilajai ir skaičiuojamajai geometrijai. „Quanta Magazine“ (atidaroma naujame skirtuke) rašė, kad KLS „yra daugelio statistikos ir informatikos klausimų pagrindas“.
Techninės detalės
Autoriai pradėjo nuo 2026 m. liepos rezultato patobulinimo, siekdami tiksliau nustatyti matematinį rėžį. Dirbdami su DI agentais struktūruotame, žmogaus valdomame procese, jie išnagrinėjo daugiau nei 100 galimų metodų, iš kurių daugelis apėmė ilgus skaičiavimus su aukštesnės eilės tenzoriais. Taip buvo gautas naujas matematinis kriterijus, tapęs galutinio įrodymo pagrindu.
Vėliau autoriai atrado, kad naująjį kriterijų galima taikyti rekursyviai. Kiekvieną patobulintą rėžį galima vėl įtraukti į tą patį samprotavimą ir gauti dar griežtesnį. 2026 m. spalio 1 d. darbo versijoje tai sumažino priklausomybę nuo dimensijos iki iteruotojo logaritmo. Ši funkcija auga nepaprastai lėtai, bet vis tiek didėja kartu su dimensija, todėl hipotezės dar visiškai neišsprendė.
Paskutinis žingsnis buvo pakartoti visą rekursyvų tobulinimą, o ne taikyti jį tik vieną kartą. Ši idėja kilo iš ankstesnio autorių darbo apie greitus tiesinio programavimo algoritmus. Autoriai įrodė, kad kiekviename etape atsirandančios mažos paklaidos mažėja pakankamai greitai, todėl jų suma lieka apribota universalia konstanta, nepriklausoma nuo dimensijos. Taip buvo pašalinta priklausomybė nuo dimensijų skaičiaus ir 2026 m. spalio 4 d. darbo versijoje įrodymas buvo užbaigtas.
Rekursyvus metodas, jo kartotinis taikymas ir įrodymas, kad susikaupusios paklaidos išlieka apribotos, yra originalus tyrėjų indėlis. DI įrankiai padėjo tyrinėti galimus metodus, atlikti detalius išvedimus, parengti rankraštį ir atlikti vidinius įrodymo patikrinimus. Tyrėjai nustatė matematinę kryptį, atrinko perspektyvias idėjas, sujungė jas į galutinį samprotavimą ir patikrino įrodymą.
Nepriklausomas patvirtinimas
Tą pačią dieną, kai autoriai paskelbė savo pilną įrodymą, atskira pirmaujančių ekspertų grupė paskelbė pilną įrodymą (atidaroma naujame skirtuke), kurį parengė lygiagrečiai. Jų darbas rėmėsi pirmojoje Microsoft straipsnio versijoje (atidaroma naujame skirtuke) pateiktais rezultatais, kuriuos jie pavadino „lemiamu įrodymo žingsniu“. Trečiasis įrodymas (atidaroma naujame skirtuke), tą pačią dieną pasirodęs atskirai, remiasi glaudžiai susijusia idėja. Be to, vėliau buvo išleistas Lean 4 formalizavimas (atidaroma naujame skirtuke), jungiantis pagrindinį pirmojo Microsoft straipsnio kriterijų su papildomais tyrimais.
Paaiškinimas: Lean yra programa, padedanti formaliai ir mašininiu būdu patikrinti matematinius įrodymus: ji patvirtina, kad kiekvienas samprotavimo žingsnis logiškai išplaukia iš ankstesnių.
Nepriklausomi įrodymai yra viena stipriausių matematikos patvirtinimo formų, nes rodo, kad rezultatas nesiremia viena samprotavimo grandine. Vėliau atsiradę alternatyvūs metodai ir formalus patikrinimas dar labiau stiprina pasitikėjimą, kad sritis atrado tikrą pagrindinį principą, o ne trapų techninį argumentą. Autoriai taip pat sutrumpino savo įrodymą ir supaprastintą samprotavimą patikrino Lean aplinkoje; abu variantus jie ketina paskelbti po galutinės peržiūros. Visi šie pokyčiai kartu sudaro vienas kitą papildančius patvirtinimo būdus.
Žmogaus ir DI vadovavimas
Įrodydamas KLS, šis tyrimas taip pat parodo, kokia galinga gali būti tyrėjų vadovaujama DI veikla, o ne paprastas prašymas DI išspręsti sudėtingą uždavinį vienu nuosekliu pažangiausio modelio ar agento paleidimu. Autoriai taikė agentinį paieškos procesą su pakartotiniu, žmogaus padedamu „genėjimu“: kol keli agentai lygiagrečiai tyrinėjo vienos idėjos variantus, tyrėjas nagrinėjo jų tarpinius rezultatus, atmesdavo neperspektyvias kryptis, o perspektyviausią rezultatą perduodavo kitam etapui. Prieš atsirandant esminiam proveržiui buvo ištirta maždaug šimtas tyrimo trajektorijų.
Atskiroje projekto dalyje autoriai pakartotinai bandė be vadovavimo išspręsti tą pačią problemą su keliais pirmaujančiais DI modeliais, naudodami maždaug tą patį bendrą žetonų biudžetą kaip ir pagrindiniame procese. Šios pastangos tikslo nepasiekė. Galutinė sėkmė priklausė tiek nuo DI sistemų galimybių, tiek nuo tyrėjų matematinio sprendimo.
Išvada
Apibendrinant, KLS išsprendimas užbaigia centrinę aukštamatės geometrijos problemą. Daugybę rezultatų, kurie anksčiau rėmėsi hipoteze kaip prielaida, dabar galima formuluoti besąlygiškai. Todėl įrodymas suteikia tvirtesnį pagrindą iškilosios geometrijos, tikimybių teorijos ir teorinės informatikos tyrimams.
Darbas taip pat rodo, kaip kruopščiai vadovaujamas žmogaus ir DI bendradarbiavimas gali prisidėti prie tikrų mokslinių atradimų, o ne pakeisti žmogaus įžvalgą, o ją sustiprinti. Jis pabrėžia nuolatinę mokslinio sprendimo svarbą nustatant perspektyvias kryptis, atpažįstant koncepcines sąsajas ir suprantant, kada dalinė įžvalga veda prie gilesnio rezultato. Šiuo metu autoriai supaprastina įrodymą ir plečia jo formalųjį patikrinimą, kad matematikos ir teorinės informatikos bendruomenės galėtų lengviau išnagrinėti rezultatą ir juo remtis.
Padėkos
Microsoft dėkoja bendraautoriui Zhao Song už indėlį į šį darbą, taip pat Victorui Reisui (atidaroma naujame skirtuke) ir Ishai Menache už naudingas diskusijas viso projekto metu.
