ABD merkezli Physical Superintelligence (PSI), 6 Kasım'da Aaronson–Ambainis varsayımının kanıtını ve herkesin yeniden çalıştırabileceği bir Lean 4 biçimselleştirmesini yayımladı. Varsayım 2008'den beri açık ve kuantum sorgu karmaşıklığının merkezî problemlerinden biri sayılıyor. PSI'ye göre kanıtı, şirketin kendi bünyesinde geliştirdiği ve kamuya açık olmayan Anthropic model örnekleriyle çalışan bir araştırma sistemi buldu: koşunun üçüncü gününde tam bir kanıt vardı, Lean kabul etti, ardından sistem ilgili açık problemlere yönlendirildi ve sonucu iki kez iyileştirdi.
Varsayım ne diyor?
Shor algoritması sayıları hızlı çarpanlara ayırır çünkü girdide tekrar eden bir desen saklıdır. Aaronson ve Ambainis daha zor soruyu sordu: böyle bir yapı yokken, rastgele girdilerde kuantum bilgisayar üstel hızlanma sağlayabilir mi? Soruyu saf matematiğe indirdiler. T sorgudan sonra bir kuantum algoritmasının kabul olasılığı, girdi bitlerinde derecesi en fazla 2T olan ve [0,1] aralığında değer alan bir polinomdur. Böyle bir polinomda her zaman etkili bir değişken varsa — yani tek bir bitin çevrilmesi değeri kayda değer ölçüde değiştiriyorsa — klasik bir makine kuantum makineyi polinom sayıda sorguyla taklit edebilir. Rastgele dizgiler üzerinde evet/hayır sorularında üstel kuantum hızlanması yoktur.
PSI'nin yeni eşitsizliği: [0,1] aralığında sınırlı, derecesi d ve varyansı v olan bir f polinomu için bir i biti Inf_i(f) ≥ c·v^(5/2)/d^6 ≥ (v/d)^7 sağlar; burada c = 8√15/(125π⁴) ≈ 0,0025. Önceki genel sınırlar dereceyle birlikte üstel olarak zayıflıyordu; sorunun bu kadar uzun açık kalmasının nedeni tam olarak buydu. Kanıt, Shachar Lovett ve Jiapeng Zhang'ın planını izliyor ve onların varsayım olarak bıraktığı tek eşitsizliği yenisiyle değiştiriyor: anahtar adım, anahtar ayarlarını bir determinant aracılığıyla bire bir eşleştirmek. David Reimer'ın Kelebek Lemması daha zayıf bir eşleştirme veriyor.
Kendiniz neleri kontrol edebilirsiniz?
Biçimselleştirme kamuya açık ve Lean 4.33.0 ile Mathlib v4.33.0 sürümlerine sabitlenmiş. `make check`; içe aktarma kontrolü, statik denetim (kütüphanede `sorry`, `axiom` veya `native_decide` yok), derleme ve aksiyom raporu çalıştırıyor: dört nihai teorem yalnızca propext, Classical.choice ve Quot.sound'a dayanıyor. `make replay` çekirdeği leanchecker ile yeniden denetliyor; README tek iş parçacığıyla yaklaşık 7,4 GB ve 11 dakika bildiriyor. lean4lean adlı ikinci bir çekirdek ve bir karşılaştırma koşusu da raporlanıyor. Depo, ilk analizler yayımlandığında tek commit ve altı yıldıza sahipti; lisansı Apache 2.0.
Lean'in kontrol edemedikleri
- **İfade sadakati.** README, Lean'deki `PrintedConjecture` ifadesinin basılı varsayımla eşleşip eşleşmediğini insan okuyucuya bırakıyor. İnce bir farkla daha zayıf bir ifadenin geçerli kanıtı, yanlış şeyi kanıtlar. - **Biçimselleştirilmemiş bir girdi.** Agarwal ve Ben-David'in `FbsDegreeBound` hipotezi bir teoremin girdisi ve kendisi biçimselleştirilmedi. - **Makale.** Metin makine tarafından denetlenmiyor; model taslağı yazdı, sistemi çalıştıran kişi gözden geçirdi. - **Hakem değerlendirmesi.** Yok. Kanıtı içeride Jim Halverson denetledi, biçimselleştirmeye Phiala Shanahan yorum yaptı. - **Koşunun tekrarlanabilirliği.** Model kamuya açık değil; yalnızca çıktı incelenebilir, süreç değil.
Ne Scott Aaronson ne de Andris Ambainis kamuoyu önünde yorum yaptı. Ağustos'ta sabit sayıda paralel tur kullanan algoritmalar için özel bir durumu kanıtlayan dört Stanford araştırmacısı — Guy Blanc, Jordan Docter, Carmen Strassle ve Li-Yang Tan — PSI'nin sayfasında aktarılan sözlerinde sonucu "muazzam" diye niteliyor ve kanıtın birkaç çalışma hattını "oldukça büyülü bir biçimde" bir araya getirdiğini söylüyor. Bu alıntıları araştırmacıların kendisi değil, PSI iletmiş durumda.
Teoremin ötesinde neden önemli?
Bu, PSI'nin bir ay içindeki aynı kalıptaki üçüncü yayını: herkesin doğrulayabileceği biçimsel bir artefakt, henüz kimsenin yakından okumadığı bir iddianın etrafına sarılmış. Bu kalıp bir şablona dönüşüyor ve mühendisler için iyi bir şablon: araç zincirini sabitle, aksiyomları denetle, yeniden oynatma hedefi sun ve kontrol edilmeyenlerin açık listesini yayımla. Kalan boşluk teknik değil. Biçimsel ifadenin insanların önemsediği problem olduğunu göstermek için gereken haftalar süren uzman okuması.
Üç işaret konuyu netleştirecek: Aaronson veya Ambainis'ten kamuya açık bir değerlendirme, Stanford grubunun hazırladığı söylenen daha kısa anlatım ve bir arXiv ya da dergi başvurusu. O zamana kadar dürüst tanım şu: ifadesi hâlâ bir insanın varsayımla eşleştirmesini bekleyen, makine tarafından denetlenmiş bir kanıt.
