Microsoft pētnieki ar MI aģentu palīdzību pierāda 31 gadu veco KLS hipotēzi

Microsoft Research 21. oktobrī savā blogā paziņoja, ka atrisināta Kanana–Lovāsa–Simonoviča jeb KLS hipotēze, viena no centrālajām neatrisinātajām problēmām augstas dimensijas ģeometrijā. Pierādījumu izstrādājuši Microsoft pētnieks Sjiņdži Džans (Xinzhi Zhang) un neatkarīgais pētnieks Džao Songs (Zhao Song). Darbs publicēts priekšpublikāciju vietnē arXiv un vēl nav izgājis recenzēšanu.

Hipotēze izvirzīta 1995. gadā. Vienkāršoti tā apgalvo, ka plašai augstas dimensijas varbūtību sadalījumu klasei labākais taisnais jeb plaknes griezums vienmēr ir gandrīz tikpat efektīvs kā labākais jebkuras formas griezums, un atšķirība nepārsniedz universālu konstanti neatkarīgi no dimensiju skaita. No šo griezumu ģeometrijas atkarīgs, cik ātri nejaušas pastaigas algoritmi spēj izpētīt sadalījumu, tāpēc rezultāts ir svarīgs statistikā, optimizācijā un teorētiskajā datorzinātnē. Microsoft norāda, ka daudzus rezultātus, kas līdz šim balstījās uz KLS kā pieņēmumu, tagad var formulēt bez šī nosacījuma.

Pēc Microsoft teiktā, pētnieki strādāja ar MI aģentiem strukturētā, cilvēka vadītā procesā. Vairāki aģenti paralēli pētīja idejas variantus, bet pētnieks izvērtēja starprezultātus, atmeta neperspektīvos virzienus un labāko nodeva nākamajai kārtai. Kopumā izmēģināti vairāk nekā 100 pieejas varianti, līdz radās jauns matemātisks kritērijs. Uzņēmums uzsver, ka rekursīvā metode un pierādījums, ka uzkrātās kļūdas paliek ierobežotas, ir pašu pētnieku ieguldījums, bet MI palīdzēja ar aprēķiniem, manuskripta sagatavošanu un iekšējām pārbaudēm.

Microsoft arī ziņo par kontroleksperimentu: atkārtoti mēģinājumi atrisināt to pašu problēmu ar vairākiem vadošajiem MI modeļiem bez cilvēka vadības, izmantojot aptuveni tādu pašu kopējo resursu apjomu, mērķi nesasniedza.

Pierādījuma galīgā versija arXiv parādījās 4. oktobrī. Tajā pašā dienā, nedaudz agrāk, matemātiķi Pjērs Bizels, Boass Klartags un Žozefs Leeks publicēja savu pierādījumu, kura izšķirošais solis, kā norādīts darba kopsavilkumā, ir Songa un Džana kritērijs no viņu pirmās, 1. oktobra versijas. Šī darba pateicību sadaļā autori raksta, ka lielāko daļu pierādījumu un matemātisko ideju atradis ChatGPT, bet autoru loma bijusi galvenokārt tos izprast un uzlabot izklāstu.

Microsoft uzskata neatkarīgos pierādījumus un vēlāk publiskoto formalizāciju programmā Lean 4 par apstiprinājumu, ka rezultāts nebalstās uz vienu spriedumu ķēdi. Tehnoloģiju izdevums CTOL Digital Solutions gan norāda, ka publiski pieejamā mašīnpārbaude balstās galvenokārt uz Bizela, Klartaga un Leeka pieeju. Microsoft autori ziņo, ka saīsinājuši savu pierādījumu un pārbaudījuši to Lean, un plāno abus publicēt pēc galīgās pārskatīšanas, taču datums nav paziņots.