PSI, Aaronson-Ambainis Varsayımının Makine Tarafından Denetlenmiş Kanıtını Bildirdi

Physical Superintelligence, kamuya açık olmayan bir Anthropic modelinin örneklerini çalıştıran dahili bir araştırma sisteminin, 2008’den beri çözülememiş bir kuantum hesaplama problemi olan Aaronson-Ambainis varsayımının kanıtını bulduğunu 6 Kasım 2026’da duyurdu.

Sistem, PSI’ın kendi altyapısında yürütülen çalışmanın üçüncü gününde eksiksiz bir kanıt üretti ve Lean kanıt asistanı bunu kabul etti. PSI daha sonra ilgili açık problemleri sisteme verdi; sistem, Lean son sürümü kabul etmeden önce sonucu iki kez geliştirdi. Makale ve Lean 4 biçimselleştirmesi kamuya açıktır.

Varsayım, Kuantum Hızlanmaları Hakkında Ne Söylüyor?

Söz konusu soru, kuantum bilgisayarların klasik makinelerden hangi koşullarda üstel ölçüde daha hızlı olabileceğiyle ilgilidir. Shor’un 1994 tarihli çarpanlara ayırma algoritması yapıya dayanır: girdisi, algoritmanın yararlanabileceği tekrarlayan bir örüntü içerir. PSI’ın sonucu ise genellikle böyle bir örüntünün bulunmadığı rastgele ya da yapısız girdilerin karşıt durumunu ele alıyor.

Sorgu modelinde klasik bir algoritma her sorguda bir bit okurken, kuantum sorgusu birçok girdi konumuna süperpozisyon hâlinde yayılabilir. PSI’ın açıklaması bu modeli polinomlarla ilişkilendiriyor: T kuantum sorgusunun ardından algoritmanın “evet” yanıtı verme olasılığı, girdi bitlerinin derecesi en fazla 2T olan sınırlı bir polinomudur. Dolayısıyla kuantum algoritmasını simüle etmek, üstel sayıda girdi biti okumadan bu polinomu tahmin etme problemine dönüşür.

İlk makalelerinde Scott Aaronson ve Andris Ambainis, her sınırlı düşük dereceli polinomun etkisi yüksek bir değişkeni bulunduğu varsayımını ortaya attı. Bu varsayımın doğru olduğu kabul edildiğinde, T sorgulu her kuantum algoritmasının çoğu girdi üzerinde, T’ye göre polinom sayıda sorgu yapan klasik bir algoritmayla simüle edilebileceğini kanıtladılar. Bunun sonucu, sabit herhangi bir yaklaşım hatası ve hariç tutulan girdi oranı için klasik sorgu sayısının üstel değil polinom derecesinde artmasıdır; ancak bu, uygun yapıya sahip problemlerde kuantumun üstel avantajlar elde etme olasılığını ortadan kaldırmaz.

Biçimsel olarak depo, derecesi en fazla d olan ve ayrık küpteki değerleri 0 ile 1 arasında kalan bir gerçek polinomu p ele alıyor. Polinomun düzgün dağılımlı rastgele bir girdi üzerindeki varyansı en az ε ise, bir koordinatın etkisi en az (8√15 / (125π⁴)) · ε^(5/2) / d⁶ ve dolayısıyla en az (ε/d)⁷ olur. Etki, o koordinattaki bit çevrildiğinde p değerinde meydana gelen değişimin karesinin beklenen değeridir.

Kanıt Nasıl Oluşturuldu ve Denetlendi?

Kanıt, Shachar Lovett ve Jiapeng Zhang’ın kesirli sertifikalar ve seviye kümelerine dayanan planını izliyor; ancak bu planın varsayımsal bıraktığı bir eşitsizliğin yerine, tüm çiftler için geçerli yeni bir eşitsizlik koyuyor. Bir determinant, girdi yapılandırmaları arasında bire bir eşleştirme oluşturuyor. PSI’a göre bu eşleştirme, David Reimer’ın daha zayıf Butterfly Lemma eşleştirmesinin ötesine geçiyor; çünkü yeni eşitsizlik için gereken bir sınır olan eşleştirilmiş yapılandırmaların her koordinatta ne sıklıkla aynı değere sahip olduğunu da sınırlıyor.

Depo, temel kanıtı dört bölüme ayırıyor: determinant ve bijeksiyondan tüm çiftler eşitsizliğini çıkarmak, bu eşitsizliği seviye kümeleri üzerinde tümleştirmek, koordinatlar üzerinden ortalama almak ve noktasal duyarlılık sınırıyla birlikte bir satır sınırı ortaya koymak. Bu adımlar bir araya gelerek açık etki sınırını veriyor.

Depoda kaydedilen denetime göre biçimsel geliştirmede kanıt yer tutucuları ya da ek aksiyomlar bulunmuyor. Bildirimleri Lean’in çekirdeğinden ve Lean’in tip denetleyicisinin bağımsız bir uygulaması olan lean4lean’dan geçirerek yeniden denetlediler. Yalıtılmış bir çalıştırmada, nanoda ve Lean çekirdeklerini kullanan bir karşılaştırıcı son dört teoremi kabul etti; ikinci bir makinede ise doğru olan küçük bir çözümü kabul edip bilerek yanlış hazırlanmış dört çözümü reddetti.

Bu denetimlerin açık sınırları vardır. Okuyucunun, biçimsel ifadenin yayımlanan varsayımla örtüştüğünü yine de doğrulaması gerekir. İnsanların okuyabileceği makalenin kendisi makine tarafından denetlenmiş değildir; ayrıca Lean’in çekirdeği ve derleyicisi, Mathlib’in tanımları ve denetimde kullanılan makineler güvenilen tabanın bir parçası olmaya devam eder.

İnsanların Üstlendiği Roller ve Uzman İncelemesi

PSI teknik ekibinin üyesi David Turturean araştırma sistemini geliştirdi ve çalıştırdı, problemi belirledi, modelden ilk taslağı hazırlamasını istedi ve taslağı inceledi; ayrıca makalenin doğruluğundan sorumludur. Depoda, matematiksel ifadelerin, ilk taslağın ve Lean biçimselleştirmesinin yapay zekâ modelleri tarafından üretildiği açıklanıyor. Jim Halverson kanıtı denetledi, Phiala Shanahan ise biçimselleştirme hakkında görüş bildirdi.

Duyurudan önce Guy Blanc, Jordan Docter, Carmen Strassle ve Li-Yang Tan tarafından 19 Ağustos 2026’da bir makale sunulmuştu. Bu yazarlar, paralel kuantum algoritmalarının klasik simülasyonuna ilişkin sonucu ortaya koymuş ve t sorgulu, d turlu bir algoritmanın çoğu girdi üzerinde t^(O(d²)) klasik sorguyla simüle edilebileceğini kanıtlamıştı. PSI, dört yazarın da kanıtın tamamını incelediğini ve yorumlarını ilettiğini, ayrıca uzmanlara yönelik daha kısa bir açıklama hazırladığını belirtiyor.

PSI tarafından yayımlanan değerlendirmelerinde araştırmacılar şöyle yazdı: “Bu çok büyük bir sonuç. Kuantum hızlanmalarına olanak tanıyan problemlerin doğasına ilişkin önemli çıkarımları bulunan, onlarca yıllık bir varsayımı çözüme kavuşturuyor. İspat, Boole fonksiyonlarının analizi ve olasılıksal kombinatorik alanlarındaki çeşitli çalışma çizgilerinden yararlanıyor ve bunları genişletiyor. Her şey oldukça büyüleyici bir şekilde bir araya getiriliyor.”

İlk sınama alışılmadık derecede somut: Bağımsız çekirdekler kodlanmış argümanı yeniden yürütebilir; ancak uzmanların, kodlanmış ifadenin Aaronson ve Ambainis’in varsayımıyla eşleştiğini doğrulaması ve makalenin Lean dışında kalan bölümlerini değerlendirmesi hâlâ gerekiyor. Bu iş bölümü, makine denetimlerinin neleri ortaya koyduğunu ve nelerin hâlâ insanlar tarafından matematiksel inceleme gerektirdiğini belirliyor.