Ne oldu?
Fizik araştırma şirketi PSI, 2008'de ortaya atılan Aaronson-Ambainis varsayımının kendi araştırma sistemi tarafından üç günde kanıtlandığını duyurdu. Şirkete göre sistem, Anthropic'in kamuya açık olmayan bir modelini kendi altyapısında çalıştırdı ve ortaya çıkan kanıt, matematiksel argümanların mantıksal doğruluğunu denetleyen Lean yazılımı tarafından kabul edildi. Sistem kanıtı iki kez daha iyileştirdi ve son sürüm de Lean'den geçti.
Varsayım neyi soruyor?
Aaronson-Ambainis varsayımı, belirli bir matematiksel yapıya sahip kuantum algoritmalarının klasik bilgisayarlarca verimli biçimde yaklaşık olarak hesaplanıp hesaplanamayacağını inceliyor. Varsayım doğruysa, klasik makineler bu tür kuantum algoritmalarını rastgele seçilen girdilerde yalnızca polinom düzeyinde ek yükle simüle edebilir. Bu, bazı kuantum algoritmalarının neden üstel bir hız avantajı sunmayabileceğini açıklamaya yardımcı olur; ancak Shor'un büyük sayıları çarpanlara ayırma algoritması gibi özel amaçlı yöntemleri geçersiz kılmıyor.
Henüz kesinleşmedi
PSI, çalışmayı David Turturean'ın yürüttüğünü, Jim Halverson'ın kanıtı denetlediğini ve Phiala Shanahan'ın Lean biçimlendirmesine yorum yaptığını belirtti. Stanford Üniversitesi'nden Guy Blanc, Jordan Docter, Carmen Strassle ve Li-Yang Tan da sonucu inceliyor; ekip ağustosta varsayımın özel bir durumunu kanıtlamıştı ve şimdi PSI'nin tam kanıtının daha kısa bir açıklamasını hazırlıyor. Lean, bir kanıtın belirtilen varsayımlardan mantıksal olarak çıkıp çıkmadığını denetler; ancak biçimlendirilen ifadenin özgün varsayımı doğru yansıtıp yansıtmadığı ayrıca uzmanlarca değerlendirilmeli. PSI, Eylül 2026'da kamuya açılmış ve kendisini bilimsel keşif için otomatik sistemler geliştiren bir fizik araştırma şirketi olarak tanımlıyor.
