OpenAI, ETH’yi Çürüten Sonuçları ve Lean Kanıtını Yayımladı; Anthropic de Materyalleri Paylaştı

OpenAI, üstel zaman varsayımını (ETH) çürüten sonuçlarını ve Lean ile biçimselleştirilmiş kanıt materyallerini yayımladı. Anthropic de ilgili makaleyi ve biçimselleştirme materyallerini deposunda paylaştı.

OpenAI, 26 Ekim’de sisteminin ETH’yi çürüten sonuçlar elde ettiğini ve biçimselleştirilmiş kanıtı Lean ile doğruladığını açıkladı. Sonuçların anlamı ve kapsamı dış uzmanlardan oluşan bir grup tarafından incelenecek. Şirket ayrıca bilgisayar bilimcilerinin sonuçları doğrulayıp açıklayacağı bir iş birliği grubu kuracağını duyurdu. OpenAI’ın resmî duyurusunda sonuçlara ve inceleme planına yer verildi.

Anthropic, Claude tarafından yazılan makaleyi ve ilgili biçimselleştirme materyallerini kamuya açık deposunda yayımladı. Depoda, tatmin edici atamaların sayısını hesaplayan bir algoritma ve ETH ile ilgili biçimselleştirme projesi sunuluyor. Ancak deponun açıklaması, uzmanların bağımsız incelemesinin tamamlandığını göstermiyor.

Üstel zaman varsayımı (ETH), 3-SAT probleminin değişken sayısına göre üstel zamandan daha hızlı çözülemeyeceğini öne süren hesaplama karmaşıklığı varsayımıdır. 3-SAT, her koşulun en fazla üç mantıksal terimden oluştuğu bir ifadede tüm koşulları doğru kılan bir değişken atamasının bulunup bulunmadığını sorar. Bu iddianın özü, problemi polinom zamanda çözmek değil; üstel zamandan daha yavaş büyüyen, yarı üstel zamanlı bir algoritma sunmaktır.

Yarı üstel zamanlı bir algoritma, üstel zamandan hızlı olsa da gerçek hesaplamalarda hemen pratik bir hız sağlayacağını garanti etmez. Dolayısıyla bu sonuç, tüm zor hesaplamaların hızla yapılabileceği anlamına gelmiyor. Ayrıca, yanıtı hızlıca doğrulanabilen tüm problemlerin hızlıca çözülüp çözülemeyeceğini soran P-NP probleminin çözüldüğü anlamına da gelmiyor.

OpenAI’ın biçimselleştirme kapsamı belgesi, belirli bir yöntemle kodlanmış mantıksal ifadelerin tatmin edici atamalarını tam olarak sayan bir algoritmayı açıklıyor. Belgede, Lean ile biçimselleştirilmiş çalışma zamanı sınırının yayımlanan ayrı bir makaledeki sınırdan farklı olabileceği belirtiliyor. Anthropic’in deposu da tatmin edici atamaları sayan deterministik bir Turing makinesini ve ETH ile ilgili biçimselleştirme materyallerini tanıtıyor.

Lean doğrulaması, bilgisayarın biçimselleştirilmiş bir önermenin kanıtını kontrol etmesi sürecidir. Bu kontrol tek başına, biçimselleştirilen önermenin asıl problemi doğru biçimde ifade edip etmediğini veya sonucun önceki çalışmalar açısından ne anlama geldiğini belirlemez. Bunlar için matematiksel kanıtın incelenmesi ve sonuçların kapsamının ayrıca değerlendirilmesi gerekir.

Üstel zaman varsayımı; çizge teorisi, hesaplamalı biyoloji ve veritabanları gibi alanlarda problemlerin zorluğunu ele alan koşullu sonuçlarda öncül olarak kullanılageldi. OpenAI, iddia bağımsız incelemeden geçse bile daha hızlı algoritmalara veya pratik iyileştirmelere dönüşmesi için ek araştırma gerektiğini belirtti. Önceki çalışmaların dayandığı varsayımların değişebilmesi ile uygulamalı problemlerin hemen kolaylaşacağı iddiasını birbirinden ayırmak gerekiyor.

Üstel zaman varsayımının kısaltması ETH, Ethereum’un ETH koduyla aynı olsa da burada hesaplama karmaşıklığı teorisindeki varsayımı ifade ediyor. Bu araştırma Ethereum ağıyla ilgili değil. Yayımlanan sonuçlar, Bitcoin’in veya Ethereum’un kriptografik sistemlerinin kırıldığı sonucunu destekleyen bir kanıt da sunmuyor. Bağımsız inceleme, şu ana kadar yayımlanan kanıt ve biçimselleştirme materyalleri üzerinden sürüyor.