OpenAI, lokal düzgünleştirme kanıtı, ETH çürütmesi ve Yang-Mills varlığı iddiasında bulundu

dev.to'da yer alan bir habere göre OpenAI, 26 Ekim'de modellerinin matematik, bilgisayar bilimi ve fizik alanlarına yayılan üç büyük sonuç ürettiğini duyurdu. Şirket, üç iddianın da bağımsız doğrulamayı beklediğini açıkça belirtiyor; ancak doğru çıkmaları halinde yapay zekâ destekli bilim için bir dönüm noktası oluştururlardı. Matematik ve bilgisayar bilimi sonuçlarına, GitHub'da yayımlanan Lean formalleştirmeleri eşlik ediyor; fizik materyalleri ise inceleme grubunun kendi kararıyla henüz paylaşılmıyor.

Her boyutta lokal düzgünleştirme çözüldü

OpenAI, modellerinin 1991'de Sogge tarafından öne sürülen lokal düzgünleştirme konjektürünü her boyutta kanıtladığını söylüyor. Konjektür, dalga denklemlerindeki enerjinin zamanla nasıl yoğunlaştığını düzenler ve en keskin enerji yoğunlaşmalarının uzun süre devam edemeyeceğini ifade eder. Harmonik analizin temellerinde yer aldığı için, bir kanıt aynı zamanda Kakeya konjektürünü — bir iğnenin her yöne işaret edebilmesi için ne kadar az yere ihtiyaç duyduğu sorusunu — ve tüm boyutlarda Stein kısıtlama konjektürünü de çözerdi.

Şirket, model çıktısını 18 Ekim, Lean formalleştirmesini ise ertesi güne tarihlendiriyor. Sonucun, Guth, Wang ve Zhang'ın iki boyuttaki önceki çalışmalarının ve Wang ile Zahl'ın 2025 tarihli üç boyutlu Kakeya konjektürü kanıtının üzerine inşa edildiğini belirtiyor. Dış tavsiye üzerine, yapay zekâ tarafından üretilen yazım GitHub'da açık biçimde yayımlandı; böylece araştırmacılar kendi doğrulama çabalarını organize edebilecekler.

Üstel Zaman Hipotezi çürütüldü

İkinci iddia, Üstel Zaman Hipotezi'ne yönelik — Boolean doğrulanabilirliği probleminin çözümünün ne kadar zor olduğuna dair uzun süredir kabul gören ve grafik teorisinde, hesaplamalı biyolojide, veritabanlarında ve hesaplamalı geometride yüzlerce sonucun dayandığı bir varsayıma. OpenAI, sisteminin hipotezin yanlış olduğunu gösterdiğini ve sonucun ardından Lean'de doğrulandığını söylüyor. Doğal dildeki çürütme 16 Ekim, formalleştirme ise 17 Ekim tarihli; ikisi de GitHub'da herkese açık.

UC San Diego'dan Russell Impagliazzo ve Ramamohan Paturi ile MIT'den Ryan Williams liderliğindeki bir doğrulama grubu, çalışmayı inceleyip açıklayacak. Grup, tüm ham verinin kamuya açıklanmasını ve OpenAI'nin bir konferans finanse etmesini talep etti; OpenAI her ikisini de kabul etti. Çürütme doğru çıkarsa, bu tür hesaplamaların gerçekte ne kadar hızlandırılabileceği sorusunu yeniden gündeme getirir.

Yang-Mills varlığı ve Standart Model

Üçüncü iddia en ağır sonuçları taşıyanı. OpenAI, modellerinin dört boyutlu belirli etkileşimli kuantum alan teorileri için — kuantum kromodinamiği ve Standart Model'in birleşik bir tamamlaması dahil — matematiksel olarak titiz bir varlık kanıtı ürettiğini ve saf Yang-Mills teorisinin var olduğunu gösterdiğini söylüyor; bu, Clay Matematik Enstitüsü'nün Milenyum Ödül problemlerinden birinin alt problemlerinden biri.

Yang-Mills kanıtı 9 Eylül, kuantum kromodinamiği kanıtı 18 Eylül, Yang-Mills varlığının Lean formalleştirmesi ise 16 Ekim tarihli. Burada yayım süreci diğer ikisinden farklı: Nobel ödüllü David Gross liderliğinde, Michael Douglas, Arthur Jaffe, Igor Klebanov ve Nikita Nekrasov'un yer aldığı bir inceleme grubu, yapay zekâ tarafından üretilen ürünleri şimdilik tutma ve çalışmayı kendisinin yazma kararı aldı.

Bölünmüş bir matematik topluluğu

Tepkiler bölünmüş durumda. Üyeleri arasında Timothy Gowers, Martin Hairer ve Edward Witten'ın bulunduğu Matematik ve Yapay Zekâ Danışma Grubu, OpenAI'nin kendilerine Lean formalleştirmesinin tamamlandığını ve yayımı daha fazla geciktirmek için bilimsel bir neden bulunmadığını söylediğini aktarıyor. Grup, 25 Ekim'de yayımladığı bir bildiride yapay zekâ çıktısının önce belirlenmiş matematikçilere yönlendirilmesi uygulamasını eleştirdi.

Times of AI önemli bir uyarı ekliyor: Lean doğrulaması, bir biçimsel kanıtın biçimsel bir önermeden çıktığını ortaya koyar; biçimsel önermenin, konjektürü özgün haliyle sadakatle yansıttığını değil. Yayın, bu ayrımın OpenAI'nin önceki bir matematik el yazmasında ilgili hale geldiğini not düşüyor.

Neden önemli

Her iddia tek başına bile önemli olurdu. Lokal düzgünleştirmenin çözülmesi, harmonik analizdeki üç merkezî açık problemi birden çözerdi; Üstel Zaman Hipotezi'nin çürütülmesi karmaşıklık teorisinde dalga etkileri yaratır ve koşullu sonuçlardan oluşan büyük bir kümenin ardındaki varsayımları sarsardı; Yang-Mills için titiz bir varlık kanıtı, Clay Milenyum Ödül problemlerinden birini ileriye taşırdı. Birlikte ele alındığında, yapay zekâ sistemlerinin yalnızca mevcut bilgiye dair soruları yanıtlamakla kalmayıp yeni bilim keşfedip kanıtlayabileceğine şimdiye kadarki en güçlü gösterim olurdu. En az bunun kadar kayda değer olan, iddiaların çevresinde şimdi unfolding süreci: makine tarafından doğrulanabilen Lean kanıtları bağımsız doğrulama için bir yol sunarken, yapay zekâ tarafından üretilen sonuçların nasıl ve ne zaman yayımlanacağına dair tartışma, yapay zekâ üretimi bilimde atıf, kontrol ve güvene ilişkin çözümsüz soruları gündeme getiriyor.