OpenAI ve Anthropic Üstel Zaman Hipotezini Çürüttü mü? 3-SAT İddiaları ve Lean 4 Doğrulamasının Sınırı

Teknoloji 17 dk
Merkezdeki kristale kehribar ve camgöbeği ışık yansıtan iki cam kule ve kristali ölçen pirinç kumpas illüstrasyonu
İki laboratuvar birkaç saat arayla, 16 Ekim'de bulunan alt-üstel 3-SAT sayma algoritmalarını ve Lean formalizasyonlarını yayımladı. Sonuç P ve NP sorusunu çözmüyor, pratik çözücüleri hızlandırmıyor ama makine doğrulamasının sınırını net biçimde gösteriyor.

İki büyük yapay zekâ laboratuvarı aynı hafta içinde, üstelik birkaç saat arayla teorik bilgisayar biliminin en kritik dayanaklarından birini yıktığını iddia etti: Üstel Zaman Hipotezi (Exponential Time Hypothesis, kısaca ETH) yanlış. İlk duyuru 26 Ekim 2026’da OpenAI’ın akademik işbirliği yazısıyla geldi ve ilgili makale openai/math reposuna eklendi. WebProNews’un aktardığına göre, iki ekibin 26 Ekim’deki GitHub commit saatleri arasında yaklaşık altı saat vardı (OpenAI ABD Doğu saatiyle 16:52, Anthropic 23:07). Ertesi gün, 27 Ekim’de Anthropic kendi formal-math reposunu ve Hexagon preprint kaydını açarak yazar hanesine doğrudan Claude adını yazdı.

İşin daha çarpıcı tarafı, her iki laboratuvarın da çekirdek algoritmanın keşif tarihi olarak aynı günü, 16 Ekim 2026’yı işaret etmesi. İki çalışma da k-CNF formüllerinin sağlayan atamalarını sayan deterministik alt-üstel (subexponential) algoritmalar sunuyor ve ikisi de iddiasını Lean teorem kanıtlayıcısıyla doğrulanmış formal kodlarla destekliyor. Ortada henüz hakem denetiminden geçmiş birer makale yok, dolayısıyla her iki yayını da kesinleşmiş teorem yerine doğrulanmayı bekleyen iddialar olarak okumak gerekiyor. Yine de aynı gün keşfedilen iki bağımsız çalışma, sosyal medyadaki “P ve NP çözüldü mü” gürültüsünden çok daha derin bir soruyu gündeme taşıyor: Bir kanıtı makine doğruladığında, makinenin neyi söylediğini kim doğrulayacak?

Üstel Zaman Hipotezi (ETH) Nedir ve Neden Yüzlerce Makale Ona Dayanıyor?

Üstel Zaman Hipotezi (ETH), Russell Impagliazzo ve Ramamohan Paturi’nin (Francis Zane ile birlikte) ortaya attığı ve 3-SAT probleminin 2^{o(n)} gibi alt-üstel bir sürede çözülemeyeceğini savunan temel karmaşıklık varsayımıdır. Eğer bu hipotez gerçekten yanlışsa, P ve NP eşitliği çözülmese bile 800’den fazla akademik makaledeki koşullu zorluk alt sınırlarının dayanağı ortadan kalkar.

Konuyu anlamak için bilgisayar biliminin en klasik problemine, yani 3-SAT’a dönmek gerekiyor. Elinizde n mantıksal değişken ve m cümlecikten (clause) oluşan bir formül olduğunu düşünün. Her cümlecik en fazla üç değişkenin VEYA (OR) bağlacıyla birleşiminden oluşuyor ve bu cümleciklerin tamamı VE (AND) ile birbirine bağlanıyor (genel adıyla k-CNF). Karar problemi olan 3-SAT, tüm formülü doğru (true) yapan en az bir atama olup olmadığını sorar. Onun sayma versiyonu olan #3-SAT ise daha zor bir iş ister: Olası 2^n atamanın tam olarak kaç tanesi bu formülü sağlar?

Kaba kuvvet (brute force) yöntemi 2^n ihtimalin tamamını tek tek dener. On yıllar boyunca araştırmacılar bu üstel tabanı küçültmeyi başardı ama üssün n ile doğrusal büyümesinden kurtulamadı. Anthropic’in makale PDF’inde sıralanan önceki rekorlara baktığımızda, deterministik 3-SAT için en iyi sınırın O(1.328^n) (Liu, 2018), rastgeleleştirilmiş PPSZ hattındaki rekorun O(1.308^n) ve #3-SAT sayma rekorunun O(1.6423^n) (Kutzkov, 2007) olduğunu görüyoruz. Hepsinde taban 1’den büyük bir sabit olarak kalıyor.

Impagliazzo ve Paturi’nin ortaya attığı Üstel Zaman Hipotezi, tam da bu duvarın aşılamaz olduğunu varsayar. Hipoteze göre 3-SAT, 2^{o(n)} gibi alt-üstel bir sürede çözülemez ve üs kısmında mutlaka pozitif bir sabit kalır. Bilgisayar bilimciler bu varsayımı çok sevdi, çünkü P ≠ NP varsayımı tek başına “şu problem n^2 süreden daha hızlı çözülemez” gibi hassas alt sınırlar (fine-grained complexity) kanıtlamaya yetmiyordu.

OpenAI’ın duyurusuna göre ETH, çizge teorisinden hesaplamalı biyolojiye, veritabanlarından hesaplamalı geometriye kadar yüzlerce makalede koşullu zorluk kanıtlarının temel taşı olarak kullanıldı. Anthropic’in makalesinde Claude tarafından yapılan literatür taraması ise ETH’ye veya onu gerektiren daha güçlü hipotezlere (SETH, Gap-ETH) dayanan en az bir teorem içeren 800’den fazla makale tespit etti. Eğer ETH gerçekten yanlışsa, bu 800’ü aşkın makaledeki koşullu alt sınırların temeli boşa düşüyor.

Sekizgen halkalardan geçerek düzenli altın bir kristal kafese dönüşen karmaşık bakır ve turkuaz düğüm ağı diyagramı
Anthropic makalesi, 3-SAT çözüm sayma problemini bir tensör ağı daraltmasına dönüştürüyor ve kesişen kısıtları sadeleştirmek için oktonyonların sekiz kare özdeşliğini kullanıyor.

OpenAI ve Anthropic Tam Olarak Ne İddia Ediyor?

Her iki laboratuvar da şirket içi yapay zekâ modellerinin 16 Ekim 2026’da her sabit k genişliği için k-CNF formüllerinin çözümlerini alt-üstel sürede sayan deterministik algoritmalar bulduğunu iddia ediyor. OpenAI polinom uzayda (n+m)^{O_k(1)} 2^{n/(log n)^{1/2+o(1)}} çalışma süresi verirken, Anthropic #3-SAT için 2^{O(n log log n / √log n)} sınırını 1.050 Lean 4 modülüyle paylaşıyor.

İki laboratuvarın repolarını ve preprint metinlerini yan yana okuduğumda ilk dikkatimi çeken detay, iki modelin de 3-SAT karar problemiyle yetinmeyip her sabit k ≥ 2 için daha zor olan #k-SAT sayma problemini alt-üstel sürede çözdüğünü iddia etmesi oldu.

OpenAI’ın openai/math reposunda yer alan CONTENTS.md dosyası artık 373 sonuç ailesini kapsayan 721 taslak listeliyor (Ekim başındaki ilk paketi OpenAI’ın 722 matematik makalesi ve Lean incelememizde ele almıştık). ETH çürütmesi bu listede 378 numaralı kayıt altında, 25 Ekim 2026 tarihli klasör içinde “The Exponential Time Hypothesis is False” başlığıyla yer alıyor. OpenAI, her sabit k ≥ 2 için polinom uzay kullanan deterministik bir algoritmanın n değişkenli ve m cümlecikli bir k-CNF formülünün sağlayan atamalarını (n+m)^{O_k(1)} 2^{n/(log n)^{1/2+o(1)}} sürede saydığını belirtiyor.

Ayrıca 378 numaralı sonuç, bu algoritmanın sonsuz sayıda girdi uzunluğunda E^NP sınıfındaki bir dil için süper-doğrusal devre alt sınırları (superlinear circuit lower bounds) ürettiğini ekliyor. Üstelik ETH iddiası, OpenAI’ın 26 Ekim duyurusundaki üç büyük başlıktan yalnızca biri. OpenAI aynı pakette matematik alanında her boyutta yerel düzgünleştirme sanısının (local smoothing conjecture) kanıtlandığını (ki bu sonuç tüm boyutlarda Kakeya ve Stein kısıtlama sanılarını içeriyor, AI çıktısı 18 Ekim’de, Lean formalizasyonu ertesi gün tamamlandı) ve fizik alanında QCD ile Standart Model’in birleşik tamamlamasını içeren dört boyutlu etkileşimli kuantum alan teorilerinin varlık kanıtını duyurdu. Fizik paketi, Clay Milenyum Ödülü problemlerinden birinin parçası olan saf Yang-Mills varlık kanıtını da kapsıyor (doğal dil kanıtı 9 Eylül, QCD 18 Eylül, Yang-Mills Lean formalizasyonu 16 Ekim).

Anthropic’in reposu ve 27 Ekim’de yüklenen 26 Ekim tarihli Hexagon preprint kaydı ise tamamen 3-SAT üzerine odaklanıyor. “A 2^{o(n)} Time Algorithm for 3-SAT” başlıklı makalenin ana teoremi her sabit k genişliği için k-CNF sayma problemini kapsıyor ve #3-SAT için 2^{O(n log log n / √log n)} deterministik çalışma süresini veriyor.

Peki deterministik bir algoritma tüm dalları gezmeden c^n duvarını nasıl aşar? Anthropic’in makalesinde anlatılan mekanizma, tatmin edici atamaları sayma işini önce bir tensör ağı daraltma (tensor-network contraction) problemine, yani ağ üzerindeki çarpımların toplamına dönüştürüyor. Ağdaki kesişen kısıtlar (crossing constraints) normal şartlarda hesaplama karmaşıklığını patlatırken, algoritma bu kesişmeleri cebirsel sadeleşmeye (cancellation) izin veren işaretli bileşimlerle değiştiriyor ve her terim için özel bir gruplama seçerek özyinelemeli (recursive) biçimde ilerliyor. Bu işaretli sadeleştirmeyi mümkün kılan cebirsel araç ise 1840’lardan kalma klasik bir teorem: oktonyonların çarpımsal normuna dayanan Degen’in sekiz-kare özdeşliği (eight-square identity).

Kriter OpenAI Anthropic
Yayın tarihi 26 Ekim 2026 (blog + openai/math reposu) 27 Ekim 2026 (formal-math reposu + Hexagon, makale 26 Ekim tarihli)
Modelin bulduğu tarih 16 Ekim 2026, şirket içi model 16 Ekim 2026, şirket içi Claude araştırma modeli, 14M çıktı token’ı, sıfır insan girdisi
İddia edilen üst sınır k-CNF çözümlerini (n+m)^{O_k(1)}·2^{n/(log n)^{1/2+o(1)}} sürede sayar 3-SAT çözümlerini 2^{O(n log log n/√log n)} sürede sayar, her sabit k
Formal doğrulama Lean, 17 Ekim’de formalize edildi Lean 4 v4.33.1, ikinci çekirdek nanoda, 1.050 modül
İnsan incelemesi Impagliazzo, Paturi, Williams grubu Yazım anında bilinen bir insan kontrolü yok (makaleye göre)
Ek iddia E^NP içindeki bir dil için süper-doğrusal devre alt sınırları Tek paragraflık ipucuyla Claude Opus 5.5 tarafından yeniden türetilebilir
Yeşil bir düğümde birleşip üç cam doğrulama kemerinden geçen, ardından küçük bir köprü boşluğu ve büyütece varan raylar
Her iki model de ana algoritmayı 16 Ekim’de buldu ve Lean çekirdek kontrolünden geçti, ancak Lean dosyasının makaleyle birebir aynı şeyi söylediğinin insan gözüyle doğrulanması gerekiyor.

Bu Sonuç P = NP Demek mi, Yoksa Yarın Daha Hızlı Çözücüler Görecek miyiz?

İki sorunun cevabı da net bir hayır. Alt-üstel çalışma süresi (2^{o(n)}), polinom süreden (n^{O(1)}) hâlâ çok yavaştır ve P ile NP eşitliğini kanıtlamaz. Ayrıca formüllerdeki sabitler o kadar büyüktür ki yeni algoritma 2^n kaba kuvvet aramasını ancak n > 10^10 (hatta m = 5n için n > 10^10000) üzerinde geçebilir.

Donanım doğrulama, kriptografi veya çizelgeleme için endüstriyel SAT çözücüleri kullanan mühendislerin hayatında yarın sabah hiçbir şey değişmeyecek. Üs kısmındaki doğrusal n çarpanını n / √log n seviyesine indirmek ETH’yi çürütür ama 3-SAT problemini P sınıfına sokmaz. Anthropic’in makalesinde açıkça vurgulandığı üzere bu sonuç P ile NP arasındaki ilişkiyi çözmediği gibi Orthogonal Vectors (Dik Vektörler) hipotezini de çürütmüyor. Dolayısıyla SETH yerine doğrudan Orthogonal Vectors varsayımına dayanan pek çok ikinci dereceden (n^2) alt sınır teoremi ayakta kalmaya devam ediyor.

Pratik açıdan daha önemli neden ise asimptotik formüllerin içindeki devasa sabitler. Anthropic’in makalesi kendi algoritmasının pratik değeri konusunda son derece dürüst rakamlar veriyor:

  • m = 5n cümlecikli bir 3-CNF formülünde kanıtlanan üst sınır, değişken sayısı n > 10^10000 eşiğini geçmedikçe saf 2^n kaba kuvvet aramasından bile daha yavaş kalıyor.
  • Tek başına n cinsinden sadeleştirilmiş sınıra bakıldığında bile yeni algoritmanın 2^n kaba kuvveti geçebilmesi için n > 10^10 olması gerekiyor.
  • Yazarlar bu yaklaşımın genel olarak n > 10^7 altında herhangi bir iyileştirme sağlamasının beklenmediğini, oysa 2^n kaba kuvvet aramasının zaten n = 100 civarında pratik olarak imkânsız hale geldiğini belirtiyor.

Makaledeki cümle durumu tek satırda özetliyor: “Dolayısıyla sonucumuz pratikte formül çözmek hakkında hiçbir şey söylemiyor.”

Uzun perspektifli ızgara bir koridorda ilerleyen ve yalnızca çok uzaktaki ufuk noktasında kesişen iki ışık şeridi
Asimptotik sınır kaba kuvveti yalnızca astronomik ölçeklerde geçiyor: tek başına n için 10^10 değişkenin, m = 5n cümlecikli 3-CNF içinse 10^10000 değişkenin ötesinde.

Lean 4 Neyi Doğruluyor ve Hangi Boşluğu Kapatamıyor?

Lean 4, yazılan formal tanımlardan ana teoreme giden mantıksal adımların standart aksiyomlarla hatasız çıktığını mekanik olarak kanıtlar. Ancak Lean, MainResults.lean dosyasındaki formal tanımın makaledeki gerçek matematiksel iddiayla birebir aynı şeyi söylediğini kendi başına doğrulayamaz.

Frontier modeller ilk bakışta ikna edici görünen ama satır arasında çöken matematiksel argümanlar üretmeye yatkın olduğu için iki laboratuvar da kanıtlarını Lean teorem kanıtlayıcısına dayandırdı. Anthropic’in formal-math/eth reposundaki yapı, Lean 4 v4.33.1 ve Mathlib üzerinde 1.050 Lean modülünden oluşuyor, 24 vCPU ve yaklaşık 7 GB RAM ile 8 dakikada derleniyor. Ana dosya olan MainResults.lean, doğrudan Mathlib Turing makineleri üzerinde ETHIsFalse ve MainTheorem ifadelerini tanımlıyor. Kanıtların yalnızca Lean’in üç standart aksiyomuna (propext, Classical.choice ve Quot.sound) dayandığı hem standart çekirdekle hem leanchecker ile hem de Comparator üzerinden nanoda adlı ikinci ve bağımsız bir çekirdekle kontrol edilmiş durumda.

Geçen haftaki çitler ve formal ispatlar bültenimizde değindiğimiz gibi, bağımsız ikinci bir çekirdekten geçen formal kanıt iç tutarlılık açısından altın standarttır. Arada sorry boşluğu veya özel aksiyom yoksa, tanımlardan teoreme giden mantık zincirinde işlem hatası bulunma ihtimali sıfıra yakındır.

Öyleyse neden hâlâ temkinliyiz? Çünkü formal doğrulamanın kapatamadığı tek bir gedik vardır: tanım ile niyet arasındaki boşluk. Anthropic’in README dosyası bu sınırı tek bir cümleyle açıkça koyuyor:

“Lean kanıtları kontrol eder, ancak bu dosyanın makalede söylenen şeyi söylediğinin kontrolünü hiçbir makine yapmaz.”

Başka bir ifadeyle Lean, MainResults.lean içindeki tanımlardan ETHIsFalse sonucunun çıktığını garanti eder ama o dosyadaki Turing makinesi veya zaman karmaşıklığı tanımının, bilgisayar bilimcilerin kastettiği gerçek tanımla birebir örtüştüğünü garanti edemez. Tanımdaki küçücük bir dejenere durum veya maliyet modelindeki kasıtsız bir kısayol, teoremi teknik olarak doğru ama anlamsız kılabilir. Üstelik Anthropic’in makalesinde çok kritik bir not daha var: Tüm Lean kodları “AI modelleri tarafından yazıldı, aynı modellerin başka örnekleri tarafından incelendi ve bu metnin yazıldığı sırada hiçbir insanın bunları kontrol ettiği bilinmiyor.”

OpenAI tam da bu insan kontrolü darboğazını çözmek için farklı bir süreç kurguladı. 26 Ekim duyurusunda model çıktılarını “ham araştırma verisi” olarak tanımlayan OpenAI, her alanda bağımsız akademisyenlerden oluşan “shepherd” (rehber/koordinatör) gruplarıyla çalıştığını açıkladı. Matematik sonuçlarında grup AI çıktısını doğrudan açmayı seçti. Fizik tarafında David Gross liderliğinde Michael Douglas, Arthur Jaffe, Igor Klebanov ve Nikita Nekrasov’dan oluşan grup, insan fizikçiler makaleyi yazana kadar ham AI çıktılarını bekletme kararı aldı. Bilgisayar bilimindeki ETH iddiasında ise OpenAI doğrudan hipotezin sahiplerine gitti: UC San Diego’dan Russell Impagliazzo ve Ramamohan Paturi ile MIT’den Ryan Williams. Impagliazzo ve Paturi bizzat ETH’yi ortaya atan isimler, Williams ise güçlü ETH varyantlarını çürütmesiyle tanınıyor. Bu üçlü tüm ham verilerin hemen açılmasını ve OpenAI’ın sonuçların etkilerini tartışacak bir konferansa sponsor olmasını istedi, OpenAI da Simons Vakfı’na yaptığı 5 milyon dolarlık çalıştay desteğinin yanında bu talebi kabul etti.

İspatı Bir Model Bulduğunda Akademik Kredi Kime Yazılır?

İki duyuru arasındaki en keskin ayrım, bilimsel yazarlık ve kredi tartışmasında ortaya çıkıyor.

OpenAI akademik işbirliği için dört temel ilke açıkladı: Şeffaflık (gizlilik sözleşmesi/NDA yok), Akademik Kredi Talepsizliği (OpenAI ham AI çıktıları için akademik yazarlık talep etmiyor), Tanınırlık (kredi, çıktıları doğrulayıp bilimsel anlayışa dönüştüren bağımsız araştırmacılara ait) ve Bağımsızlık (akademisyenler gönüllü ve ücretsiz çalışıyor). Yani OpenAI modeli bir teleskop gibi konumlandırıyor, keşif kredisini veriyi anlamlandıran bilim insanlarına bırakıyor.

Anthropic ise tam tersi bir tercih yaparak makalenin yazar satırına Claude (Anthropic) yazdı. Köken notunda şu ifade yer alıyor: “Çekirdek algoritma 16 Ekim’de şirket içi bir Claude araştırma modeli tarafından 14 milyon çıktı token’ı ve sıfır insan girdisiyle bulundu. Anthropic araştırmacıları sunumu iyileştirmek için Claude ile çalıştı.” Makale ayrıca rakip laboratuvarın çalışmasını da açıkça not düşüyor: “Bağımsız ve eşzamanlı olarak OpenAI’daki bir iç model benzer bir sonucu kanıtladığını iddia ediyor.”

Daha da ilginci, Anthropic’in Apache 2.0 lisanslı README dosyasında yer alan tek paragraflık matematiksel özet. Anthropic, tensör ağı kurulumunu ve oktonyon sekiz-kare sadeleşmesini özetleyen bu kısa paragraf verildiğinde, Claude Opus 5.5 modelinin yüksek efor (high effort) modunda her δ > 0 için temel O(2^{δn}) ETH çürütmesini baştan türetebildiğini (keskin 2^{O(n log log n / √log n)} sınırı hariç) belirtiyor. 25 yıllık açık bir problemin çözümü tek paragraflık bir ipucuna sıkıştırılıp başka bir model tarafından yeniden üretilebildiğinde, geleneksel akademik yazarlık kalıpları da kaçınılmaz olarak esniyor.

Önümüzdeki haftalarda gözümüz iki somut doğrulama adımında olacak: İlki Impagliazzo, Paturi ve Williams ekibinin OpenAI’ın 378 numaralı sonucu için yayımlayacağı inceleme ve düzenlenecek konferans, ikincisi ise bağımsız Lean uzmanlarının Anthropic’in MainResults.lean dosyasındaki Turing makinesi tanımlarını satır satır denetlemesi. Eğer her iki formal tanım da insan denetiminden eksiksiz geçerse, 16 Ekim 2026 tarihi iki otonom modelin aynı gün içinde teorik bilgisayar biliminin en sağlam varsayımlarından birini yıktığı gün olarak kayda geçecek.

Sıkça Sorulan Sorular

OpenAI ve Anthropic P = NP olduğunu mu kanıtladı?

Hayır. İki laboratuvar da k-CNF tatmin edici atama sayma problemi için alt-üstel (2^{o(n)}) algoritmalar bulduğunu iddia ediyor. Bu süre her c > 1 sabiti için c^n sınırından asimptotik olarak daha hızlı olduğu için Üstel Zaman Hipotezini (ETH) çürütür ancak polinom süre (n^{O(1)}) olmadığı için P ile NP eşitliğini kanıtlamaz.

Bu algoritmalar pratikte kullanılan SAT çözücülerini hızlandırır mı?

Hayır. Anthropic’in makalesine göre m = 5n cümlecikli bir 3-CNF formülünde yeni sınır n > 10^10000 olmadan, tek başına n cinsinden sınır ise n > 10^10 olmadan 2^n kaba kuvvet aramasını geçemiyor. Dolayısıyla endüstriyel SAT çözücülerinde pratik bir değişiklik yaratmıyor.

Kanıtlar Lean 4 ile doğrulandıysa neden hâlâ iddia olarak adlandırılıyor?

Lean 4 ve bağımsız nanoda çekirdeği, teoremin MainResults.lean dosyasındaki tanımlardan mantıksal olarak çıktığını doğrular. Ancak hiçbir makine o dosyadaki formal Turing makinesi ve karmaşıklık tanımlarının makaledeki gerçek problemle birebir aynı olduğunu denetleyemez. Bu yüzden insan uzmanların tanımları incelemesi şarttır.

Kaynaklar

Oğuzhan Koçaklı

2015 yılından beri profesyonel olarak marketing, gaming ve blockchain dünyasıyla ilgileniyorum. Bir çok önemli markanın pazarlama stratejilerinin oluşturulması ve uygulanmasında görev aldım. Şimdilerde mobil oyunlar ve oyunların blockchain entegrasyonu üzerine çalışmalar yürütüyorum. Yapay zeka çalışmaları ise uzun yıllardır hobim.

Tüm yazıları

Bir yanıt yazın

E-posta adresiniz yayınlanmayacak. Gerekli alanlar * ile işaretlenmişlerdir