Henüz yayınlanmamış bir Anthropic modeli kullanan yapay zekâ sistemi Aaronson-Ambainis sanısını kanıtladı, Lean ile doğrulandı

Yapay zekâ odaklı fizik laboratuvarı Physical Superintelligence (PSI), 6 Kasım 2026'da, dahili bir araştırma sisteminin, 2008'den beri açık kalan kuantum karmaşıklık teorisi sorunu olan Aaronson-Ambainis sanısını kanıtladığını duyurdu. Sistem, halka açılmamış bir Anthropic modelinin örneklerini çalıştırdı ve dev.to'da aktarılan duyuruya göre argümanı Lean proof assistant kabul etti. Makale ve Lean 4 formalizasyonu kamuya açıldı; makale ise henüz hakem incelemesinden geçmedi.

Sanı neyi söylüyor

Scott Aaronson ve Andris Ambainis, sanıyı 2008'de temel bir soruyu ele almak için ortaya attı: kuantum bilgisayarlar sıradan bilgisayarlardan ne zaman üstel derecede hızlı olabilir? Peter Shor'un 1994 tarihli çarpanlara ayırma algoritması gibi çarpıcı hızlanmalar yapıya bağlıdır — girdinin belirli bir örüntü gizlediğine dair bir söz. Kuantum makinelerinin, böyle bir yapıyı neredeyse hiç taşımayan rastgele girdilerde üstel derecede kazanıp kazanamayacağı bilinmiyordu. Aaronson ve Ambainis soruyu polinomlar üzerine bir ifade olarak yeniden çerçeveledi ve sanının doğru olması durumunda kuantum bilgisayarların rastgele girdilerde klasik bilgisayarlardan en çok polinomsel derecede hızlı olacağını gösterdiler.

Sistem kanıtı nasıl buldu

PSI'ye göre eksiksiz bir kanıt, şirketin kendi altyapısında yapılan bir çalıştırmanın üçüncü gününde geldi. Ardından sistem ilgili açık problemlere yönlendirildi, sonucu iki kez iyileştirdi ve Lean son sürümü kabul etti. Argüman, problemi tek bir eşitsizliğe indirgemiş ve bunu sanı olarak açık bırakmış olan Shachar Lovett ve Jiapeng Zhang'ın ortaya koyduğu bir planı izliyor. PSI'nin kanıtı, David Reimer'ın Butterfly Lemma'sı üzerine kurulan bir eşleştirme yapısıyla makalede kanıtlanan yeni bir eşitsizlik koyuyor.

PSI teknik ekibinden David Turturean çalışmaya öncülük etti: araştırma sistemini geliştirdi, problemi kapsamlandı, ilk taslağı oluşturması için modele prompt verdi, taslağı inceledi ve makalenin doğruluğundan sorumlu kişi olarak adı geçiyor. PSI danışmanlarından Jim Halverson kanıtı denetledi, danışmanlardan Phiala Shanahan ise Lean formalizasyonu hakkında yorum yaptı. PSI, matematiksel ifadelerin, makalenin ilk taslağının ve Lean formalizasyonunun tamamının yapay zekâ modelleri tarafından üretildiğini belirtiyor.

Sonuç neyi ortaya koyuyor

Ana eşitsizlik somut: bir polinom v kadar değişiyorsa ve derecesi d ise, c yaklaşık 0.0025 olmak üzere — yani en az (v/d)^7 — tek bir girdi bitinin etkisi en az c·v^(5/2)/d^6 oluyor. Pratikte bu, sıradan bir bilgisayarın, rastgele girdilerin küçük bir bölümü dışındaki tümü için, kuantum makinesinkine göre en çok polinomsel olarak artan sayıda girdi okumasıyla, kuantum bilgisayarın evet deme olasılığını küçük bir hataya kadar öngörebileceği anlamına geliyor. Rastgele veriler üzerine evet-hayır sorularında, girdi nadir bir örüntü gizlemedikçe üstel kuantum kazançları olanaksız. Bu bir sınırlar sonucudur, mühendislik sonucu değil: kuantum hızlanmalarının geçerli olduğu çarpanlara ayırma gibi yapısal problemler hakkında hiçbir şey söylemiyor.

Doğrulama ve kalan uyarılar

Doğrulamanın açık sınırları var. Kanıt hakem incelemesinden geçmedi, insan tarafından okunabilir makalenin kendisi makine tarafından doğrulanmadı ve okuyucuların, Lean'in doğruladığı formal ifadenin basılı sanıyla eşleştiğini teyit etmesi hâlâ gerekiyor. Unite.AI'ya atıf yapan dev.to haberi, formal geliştirmenin hiçbir kanıt yer tutucusu veya ek aksiyom içermediğini ve tanımlamaların Lean'in çekirdeği ile Lean'in tip denetleyicisinin bağımsız bir uygulaması olan lean4lean üzerinden yeniden çalıştırıldığını ekliyor.

Stanford'daki bir grup — Guy Blanc, Jordan Docter, Carmen Strassle ve Li-Yang Tan — sanının öngörüsünün özel bir durumunu Ağustos 2026'da çözdü ve tam kanıtı okuyarak bunu "büyük bir sonuç" olarak niteledi ve uzmanlar için daha kısa bir anlatım hazırlıyor.

Neden önemli

Sonuç aynı anda iki hikâye taşıyor. Kuantum bilişimi açısından alanın merkezî açık problemlerinden birini kapatıyor ve net bir sınır çiziyor: üstel avantaj girdide yapı gerektiriyor. Yapay zekâ açısından ise bu, insan matematikçilere 18 yıl direnen bir problemin, halkın kullanamadığı bir model tarafından üretilmiş ve makine tarafından doğrulanmış bir kanıtı — dahili araştırma sistemlerinin halka açık olanlardan ne kadar ileriye gittiğinin bir işareti. dev.to haberi ayrıca METR'nin Kasım tahminine dikkat çekiyor: Anthropic'in yetenekleri önceki döneme göre kabaca iki kat hızla gelişiyor ve bu hızlanmanın büyük bölümünü yapay zekânın kendisi sürüklüyor.

Açık kalan ise insan işi: formal ifadenin özgün sanıyla eşleşip eşleşmediği ve bununla birlikte 6 Kasım 2026'nın bir sanının teoreme dönüştüğü gün mü yoksa makine tarafından doğrulanmış bir argümanın tam olarak neyi kanıtladığını söylemek için hâlâ insanlara ihtiyaç duyulan gün mü olacağı.