Microsoftin tutkija ja yhteistyökumppani todistivat 31 vuotta vanhan KLS-konjektuurin

Microsoft Research ilmoitti 21. lokakuuta 2026, että sen koneoppimisen ja optimoinnin ryhmän vanhempi tutkija Xinzhi Zhang ja yhteistyökumppani Zhao Song ovat todistaneet Kannanin–Lovászin–Simonovitsin konjektuurin, joka on 31 vuotta vanha korkeaulotteisen geometrian ja todennäköisyyslaskennan ongelma. Todistus syntyi ihmisen ohjaamassa agenttipohjaisessa tekoälytutkimusprosessissa.

Konjektuuri ja uusi yläraja

Todistus esitetään 140-sivuisessa artikkelissa O(1)-raja KLS-vakiolle, jonka kirjoittajiksi on merkitty Zhao Song ja Xinzhi Zhang. Artikkeli lähetettiin ensimmäisen kerran arXiviin 1. lokakuuta 2026 ja sitä tarkistettiin 4. lokakuuta 2026; lähettävänä kirjoittajana oli Zhang. Tiivistelmän mukaan kirjoittajat osoittavat, että KLS-vakio ψ_n on ylhäältä rajoitettu universaalilla vakiolla C, mikä ratkaisee konjektuurin. Lisäksi he todistavat universaalin ylärajan jokaisen isotrooppisen log-koveran todennäköisyysmitan Poincarén vakiolle.

Muodollisesti vuonna 1995 esitetty konjektuuri kysyy, onko jokaisen n-ulotteisen avaruuden isotrooppisen log-koveran todennäköisyysmitan Cheegerin vakio alhaalta rajoitettu universaalilla positiivisella vakiolla. Microsoft Researchin julkaisun yksinkertaisemman selityksen mukaan kysymys on siitä, onko laajassa korkeaulotteisten todennäköisyysjakaumien luokassa paras tasomainen eli hyperpinnan muodostama leikkaus aina lähes yhtä tehokas kuin minkä tahansa muotoinen paras leikkaus: niiden tehokkuus saa erota toisistaan enintään universaalin vakion verran ulottuvuuksien lukumäärästä riippumatta. Koska näiden leikkausten geometria määrää, kuinka nopeasti satunnaiskulut voivat tutkia jakaumaa, konjektuuri on keskeisessä asemassa korkeaulotteisen otannan teoriassa.

Ennen tätä työtä paras tunnettu tulos oli Brayden Letwinin 21-sivuinen artikkeli KLS-vakio on O(log^{1/4} n), joka lähetettiin 27. heinäkuuta 2026. Siinä osoitettiin, että ψ_n on enintään vakion ja log^{1/4} n:n tulo. Microsoft Researchin julkaisussa huomautetaan, että tämä yläraja kasvoi silti hitaasti ulottuvuuksien määrän kasvaessa. Uudessa työssä saadaan kiinteä yläraja, joka ei riipu ulottuvuudesta.

Konjektuurin merkitys tunnustettiin jo kauan ennen sen ratkeamista. Julkaisun mukaan Mathematical Sciences Research Instituten vuosikertomuksessa 2017–18 KLS-konjektuuria kutsuttiin korkeaulotteisen konveksin geometrian keskeiseksi avoimeksi ongelmaksi, Simons Institute kuvaili sitä yhdeksi konveksin geometrian tärkeimmistä avoimista ongelmista, ja Ronen Eldan toi esiin sen laaja-alaiset vaikutukset vuoden 2022 kansainvälisen matemaatikkokongressin julkaisuissa.

Ihmisen ohjaama agenttipohjainen tutkimusprosessi

Julkaisun mukaan kirjoittajat alkoivat pyrkiä parantamaan heinäkuun 2026 tulosta. Jäsennellyssä, ihmisen ohjaamassa prosessissa tekoälyagenttien kanssa he tutkivat yli 100 mahdollista lähestymistapaa, joista moniin liittyi pitkiä korkeamman kertaluvun tensoreita koskevia laskelmia, ja kehittivät uuden matemaattisen kriteerin, josta tuli lopullisen todistuksen perusta.

Kirjoittajat havaitsivat sitten, että kriteeriä voitiin soveltaa rekursiivisesti: jokainen parannettu yläraja sijoitettiin takaisin samaan päättelyyn, jolloin saatiin vielä tiukempi yläraja. Artikkelin 1. lokakuuta 2026 päivätyssä versiossa riippuvuus ulottuvuudesta pieneni iteratiiviseen logaritmiin, joka kasvaa erittäin hitaasti mutta kuitenkin ulottuvuuden kasvaessa, joten konjektuuri ei vielä ratkennut. Viimeisessä vaiheessa koko rekursiivinen tarkennus toistettiin sen sijaan, että se olisi tehty vain kerran. Julkaisun mukaan ajatus sai innoituksensa kirjoittajien aiemmasta työstä lineaarisen optimoinnin nopeiden algoritmien parissa. Kirjoittajat osoittivat, että kussakin vaiheessa syntyvät pienet virheet pienenevät niin nopeasti, että niiden summa pysyy ulottuvuudesta riippumattoman universaalin vakion rajoissa. Näin todistus saatiin valmiiksi artikkelin 4. lokakuuta 2026 päivätyssä versiossa.

Julkaisun mukaan rekursiivinen menetelmä, sen toistuva soveltaminen ja virheiden rajaamista koskeva perustelu ovat tutkijoiden omia alkuperäisiä saavutuksia. Tekoälytyökalut auttoivat mahdollisten lähestymistapojen tutkimisessa, yksityiskohtaisten johdantojen tekemisessä, käsikirjoituksen valmistelussa ja todistuksen sisäisissä tarkistuksissa. Tutkijat puolestaan määrittivät matematiikan suunnan, valitsivat lupaavat ideat, kokosivat niistä lopullisen päättelyn ja tarkistivat todistuksen. Julkaisussa menetelmää kuvaillaan agenttipohjaiseksi etsinnäksi, jossa ihminen karsi vaihtoehtoja iteratiivisesti: useiden agenttien tutkiessa idean eri muunnelmia rinnakkain tutkija tarkasteli välituloksia, hylkäsi epäonnistumisen uhalla olevat suunnat ja siirsi lupaavimman tuloksen seuraavaan kierrokseen. Ennen keskeisen läpimurron syntymistä tutkittiin noin sataa tutkimuspolkua.

Projektin erillisessä osassa kirjoittajat yrittivät toistuvasti ratkaista saman ongelman ilman ohjausta useilla johtavilla tekoälymalleilla. Tähän käytettiin suunnilleen samaa kokonaismerkkimäärän budjettia kuin pääprosessiin, mutta julkaisun mukaan yritys ei yltänyt tavoitteeseen. Julkaisun mukaan lopullinen onnistuminen edellytti sekä tekoälyjärjestelmien kyvykkyyttä että tutkijoiden matemaattista arvostelukykyä. Julkaisussa kiitetään Songia hänen panoksestaan työhön sekä Victor Reisiä ja Ishai Menachea projektin aikana käydyistä keskusteluista.

Riippumattomat todistukset ja koneellinen varmennus

4. lokakuuta 2026, samana päivänä kun täydellinen todistus julkaistiin, Pierre Bizeul, Boaz Klartag ja Joseph Lehec julkaisivat rinnakkain kehittämänsä 32-sivuisen todistuksen nimeltä Kannan–Lovász–Simonovitsin konjektuurin todistuksen esittely. Artikkelin tiivistelmässä todetaan, että ”todistuksen ratkaiseva askel on Songin ja Zhangin aivan äskettäin esittämä kriteeri, joka koskee kallistettujen keskiarvojen korkea-asteisia derivaattoja”. ArXiv-kommenteissa mainitaan, että artikkelissa on kappale, jossa kuvataan tekoälyn käyttöä. Tiivistelmä nostaa KLS-konjektuurin rinnalle Bourgainin leikkausongelman ja varianssikonjektuurin ja nimeää ne viime vuosikymmenten korkeaulotteisen geometrian matemaattisen kehityksen vetureiksi.

Krishnakumar Balasubramanian ja Shiva Kasiviswanathan julkaisivat erillisen todistuksen Isotrooppisten log-konkavien mittojen Poincarén vakiolle ulottuvuudesta riippumattoman ylärajan. Se lähetettiin ensimmäisen kerran 6. lokakuuta 2026, ja sitä tarkistettiin 8. lokakuuta 2026. Tiivistelmässä kuvataan deterministinen variaatiotodistus, jossa minkä tahansa isotrooppisen log-konkaviin todennäköisyysmitan Poincarén vakiolle saadaan eksplisiittinen 25:n yläraja.

Seuraavaksi julkaistiin KLS500-niminen Lean 4 -formalisaatio, jossa formalisoidaan ulottuvuudesta riippumaton tulos: jokaisen isotrooppisen log-konkaviin todennäköisyysjakauman Poincarén vakio on enintään 500. Tietovaraston mukaan kehitystyö perustuu pääasiassa Bizeulin, Klartagin ja Lehecin kumulantti- ja suspensiolähestymistapaan, johon on yhdistetty Songin ja Zhangin kallistus-spektrikriteeri. Varmennuksessa rakennettiin uudelleen 1 710 matemaattista moduulia ytimen luottamustasolla nolla. Lean-varmennus läpäistiin myös OpenAI:n määrittelemälle täsmälliselle KLS-konjektuurin väittämälle, jossa käytetään yleispätevää Poincarén vakiota 500. Projekti on lisensoitu Apache 2.0 -lisenssillä.

Microsoft Researchin julkaisussa riippumattomia todistuksia kuvataan yhdeksi matematiikan vahvimmista validoinnin muodoista, sillä ne osoittavat, ettei tulos nojaa vain yhteen päättelyketjuun. Konjektuurin ratkettua tulokset, jotka aiemmin perustuivat siihen oletuksena, voidaan julkaisun mukaan nyt esittää ehdottomina. Kirjoittajat ovat lyhentäneet todistustaan ja varmentaneet virtaviivaistetun päättelyn Leanilla, ja julkaisussa kerrotaan heidän aikovan julkaista molemmat lopullisen tarkistuksen jälkeen.