Microsoft araştırmacısı Xinzhi Zhang ve Zhao Song, 1995’ten beri açık KLS sanısını insan yönlendirmeli yapay zeka ajanlarıyla ispatladı

KLS sanısı 1995’te Kannan, Lovász ve Simonovits tarafından ortaya atıldı. Sanıya göre izotropik log-içbükey dağılımlarda en iyi düz kesim, her biçimdeki en iyi kesime yakın sonuç veriyor; aradaki fark boyuttan bağımsız bir sabitle sınırlı. Sanı, dışbükey cisimlerde rastgele yürüyüşlerin hızını, dolayısıyla örnekleme ve hacim hesaplama algoritmalarını belirliyor. Microsoft Research’ten Xinzhi Zhang ile bağımsız araştırmacı Zhao Song’un makalesi bu sabitin evrensel olarak sınırlı olduğunu gösteriyor. 1 Ekim’deki ilk sürüm sınırı çok yavaş büyüyen bir fonksiyona indirdi, 4 Ekim’deki ikinci sürüm sanıyı tamamen çözdü. Microsoft çalışmayı 21 Ekim’de duyurdu.

Makalenin yapay zeka beyanına göre yazarlar 28 Temmuz’dan itibaren GPT-6 Astra, GPT-5.6 Sol, Claude Fable 5 ve Fable 5.1 ile 100’den fazla yaklaşım denedi. Microsoft’a göre ajanlar bir fikrin türevlerini paralel işledi, araştırmacı zayıf yolları eledi. Yinelemeli yöntem, tekrar tekrar uygulanması ve hataların sınırlı kaldığının ispatı yazarlara ait. Yapay zeka arama, türetme, makale hazırlığı ve iç kontrollerde kullanıldı. Aynı token bütçesiyle önde gelen modellerle yapılan yönlendirmesiz denemeler hedefe ulaşamadı.

Pierre Bizeul, Boaz Klartag ve Joseph Lehec 4 Ekim’de bağımsız bir ispat yayımladı ve Song-Zhang ölçütünü “ispatın can alıcı adımı” diye niteledi. Bu makalenin teşekkür bölümünde ispatların ve fikirlerin çoğunu ChatGPT’nin bulduğu yazıyor. Krishnakumar Balasubramanian ve Shiva Kasiviswanathan 6 Ekim’de ayrı bir ispat paylaştı. GitHub’daki KLS500 projesi, ağırlıkla Bizeul, Klartag ve Lehec’in yaklaşımına dayanarak boyuttan bağımsız bir sınırı Lean 4’te doğruladı. Çalışmaların hepsi arXiv ön baskısı; yazarlar kısaltılmış ve Lean’de doğrulanmış ispatlarını son incelemeden sonra yayımlayacak.