PSI: Yayımlanmamış bir Anthropic modeliyle çalışan sistemimiz Aaronson-Ambainis sanısını ispatladı, ispat Lean’de doğrulandı

Duyuru

Physical Superintelligence PBC (PSI), 6 Kasım’da “Aaronson-Ambainis sanısı artık bir teorem” diyerek kuantum karmaşıklık kuramındaki bir sanının ispatını duyurdu. İspatın GitHub deposu aynı gün 03.19 UTC’de açıldı; şirketin X’teki duyuru dizisi 14.05 UTC’de geldi. Şirkete göre ispatı, PSI’da geliştirilen ve “yayımlanmamış bir Anthropic modeliyle çalışan” bir araştırma sistemi buldu.

PSI’ın anlatımına göre koşuda bu modelin birden fazla örneği kullanıldı. Sistem koşunun üçüncü gününde sanının tam ispatına ulaştı ve ispat Lean ispat doğrulayıcısından geçti. Modelin adı ve PSI’ın modele nasıl eriştiği açıklanmadı. Anthropic’in sonuçla ilgili bir açıklaması bulunamadı.

Physical Superintelligence@psipbc

Physical Superintelligence PBC bugün, kuantum karmaşıklığının temel açık problemlerinden biri olan ve kuantum hesaplamadaki hızlanma için önemli sonuçlar doğuran Aaronson-Ambainis sanısının ispatını duyuruyor.

psi.inc/research/aaron…

Dizi 👇

İngilizceden çevrildi·Orijinalini göster

Sanı ne söylüyor

Sorgu karmaşıklığında bir algoritmanın girdiye kaç kez eriştiği sayılır. Klasik bilgisayar her sorguda girdinin tek bir bitini okur. Kuantum bilgisayarın sorgusu ise süperpozisyonda birçok konuma yayılabilir. Shor’un 1994’teki algoritması gibi büyük kuantum hızlanmaları, girdideki bir yapıya, örneğin tekrar eden bir desene dayanır. Sanı, girdi tamamen rastgele olduğunda kuantum bilgisayarın evet/hayır sorularında üstel derecede az sorguyla yetinip yetinemeyeceğiyle ilgili.

Beals ve arkadaşları 1998’de, T sorgu yapan bir kuantum algoritmanın “evet” deme olasılığının derecesi en fazla 2T olan bir polinom olduğunu gösterdi. Aaronson ve Ambainis, değerleri 0 ile 1 arasında kalan böyle bir polinomda etkisi büyük bir bitin her zaman bulunduğunu öne sürdü. Sanı doğruysa klasik bir algoritma etkili bitleri sırayla okuyabilir. Böylece kuantum algoritmanın sonucunu çoğu girdide polinom sayıda sorguyla tahmin edebilir. Yani yapısız problemlerde kuantum hızlanma en fazla polinom düzeyinde kalır.

Bu sonuç kuantum bilgisayarların işe yaramadığı anlamına gelmiyor. Yapılı problemlerde üstel, yapısız problemlerde ise polinom düzeyinde hızlanma hâlâ mümkün. The Quantum Insider da sonucun yalnızca sorgu sayısıyla ilgili olduğunu, toplam hesaplama süresi ya da ticari değer hakkında bir şey söylemediğini vurguluyor.

İspat ve Lean doğrulaması

Makaleye göre değeri sabit olmayan, değerleri 0 ile 1 arasında kalan d dereceli bir polinomda etkisi en az c·v^(5/2)/d^6 olan bir bit var. Burada v polinomun varyansı; c = 8√15/(125π⁴), yani yaklaşık 0,0025. Bu sınır en az (v/d)^7 ediyor. Sanı (v/d)^O(1) biçiminde bir sınır istiyordu; önceki genel sınırlar ise derece büyüdükçe üstel olarak küçülüyordu.

Makalenin ekine göre ilk tam ispatta üs 22’ydi. “Level” entegrasyonuyla üs 11’e, ardından koordinatlar üzerinden ortalama alınarak 7’ye indi. Üç sürümün üçü de Lean’de kontrol edildi.

Sonuç olarak T sorgulu bir kuantum algoritmanın kabul olasılığı, girdilerin 1-δ kesrinde ε hatayla tahmin edilebiliyor. Bunun için en fazla (4T)^8·ε^-14·δ^-8 sorgu yapan deterministik bir klasik algoritma yetiyor. Böylece Aaronson ve Ambainis’in sanıya bağlı üç sonucu koşulsuz hale geliyor. Bunlardan biri, P = P^#P ise rastgele bir kâhin (oracle) için BQP’nin AvgP içinde kalması.

Biçimlendirme Lean 4.33.0 ve Mathlib ile yapıldı: 84 modül, 648 teorem ve 113 tanım var, eklenmiş aksiyom yok. Dört son teorem yalnızca propext, Classical.choice ve Quot.sound aksiyomlarını kullanıyor. İspat lean4lean ve nanoda adlı iki bağımsız çekirdekte yeniden oynatıldı, Comparator ile de kontrol edildi. Depo kapsam dışında kalanları da yazıyor. Biçimlendirilen ifadenin gerçekten sanıyla aynı olduğunu okurun doğrulaması gerekiyor ve makale metni makine kontrolünden geçmedi. Depo Apache 2.0 lisanslı; makalenin telif hakkı yazarda.

Yapay zekanın ve ekibin rolü

Makalenin yapay zeka beyanına göre matematiksel ifadeleri yapay zeka modelleri üretti. Model örnekleri sistem içinde mevcut fikirleri aramak, yeni fikirler önermek, bunları birleştirip test etmek ve diğer örnekleri denetlemek için kullanıldı. İlk taslağı model yazdı; Lean biçimlendirmesini de yapay zeka modelleri üretti. David Turturean taslağı gözden geçirip düzenledi ve doğruluğundan sorumlu olduğunu belirtiyor.

Çalışmayı PSI’da teknik ekip üyesi olan Turturean yönetti; makalenin tek yazarı da Turturean. Danışman Jim Halverson ispatı denetledi, danışman Phiala Shanahan ise Lean biçimlendirmesine yorum yaptı. PSI bir kamu yararı şirketi (PBC). Şirket 26 Ekim’de kuantum bilgi kuramında “uzun süredir açık beş problemi” çözdüğünü duyurmuştu. Sitesine göre Breakthrough Energy Ventures liderliğinde 58 milyon doları aşkın yatırım aldı; CEO’su Matthew Pines.

Tarihçe ve tepkiler

Aaronson’ın anlatımına göre problem 1999 civarında Fortnow ve Rogers’ın bir sorusuyla başladı; Aaronson sanıyı 2008 civarında fark etti. “The Need for Structure in Quantum Speedups” makalesinin ilk sürümü 5 Kasım 2009’da arXiv’e kondu. Makale ICS 2011 konferansında sunuldu ve 2014’te Theory of Computing dergisinde yayımlandı. 2019’da Nathan Keller ve Ohad Klein bir ispat öne sürdü. Ancak Paata Ivanisvili’nin Lemma 5.3’te bulduğu hata nedeniyle ön baskı geri çekildi.

Guy Blanc, Jordan Docter, Carmen Strassle ve Li-Yang Tan, Ağustos 2026’da sanının özel bir durumunu çözmüştü. 19 Ağustos tarihli makalelerine göre t sorgulu, d turlu paralel kuantum algoritmalar t^O(d²) klasik sorguyla simüle edilebiliyor. Ekip PSI’ın ispatını okudu, yorumlarını gönderdi ve uzmanlar için kısa bir anlatım hazırlıyor. Ekip, PSI’ın aktardığı yorumunda sonucu “çok büyük bir sonuç” diye niteliyor ve onlarca yıllık bir sanıyı çözdüğünü söylüyor. Ekibe göre ispat, Boole fonksiyonlarının analizi ve olasılıksal kombinatorikteki çalışmalardan yararlanıyor ve onları genişletiyor.

Sonuç henüz hakem değerlendirmesinden geçmedi ve arXiv’de değil; makale yalnızca GitHub’da PDF olarak yayımlandı. Scott Aaronson, 8 Kasım sabahı itibarıyla PSI’ın ispatı hakkında yorum yapmadı.