OpenAI'ın Navier-Stokes Lean kanıtı makalesinden ayrılıyor, matematikçiler iddia ediyor

Anlaşmazlık içindeki iki kanıt sürümü

8 Eylül'de OpenAI, matematiğin en ünlü açık problemlerinden biri olan Navier-Stokes problemine bir çözüm duyurdu. New Scientist'e göre şirket çalışmayı iki biçimde yayımladı: İngilizce düzyazı ile matematiksel gösterimin birleşiminden oluşan geleneksel bir makale ve bir bilgisayarın her mantıksal adımı mekanik olarak doğrulayabildiği bir dil olan Lean 4 ile yazılmış bir sürüm. OpenAI'ın GitHub deposu, Lean kodunu "Finite time blowup for Navier–Stokes" başlıklı makaledeki sonuçların bir formalizasyonu olarak tanımlıyor.

Cambridge Üniversitesi'nden Anders Hansen ve Fabian Circelli ile King's College London'dan Alexander Bastounis'ten oluşan matematikçi ekibi, iki belgenin özdeş olmadığını savunuyor. İddiaları 8.6 Lemması'na odaklanıyor. Yazılı kanıtta belirli bir niceliğin m + 4'ün altında kaldığının gösterilmesi gerekiyor; burada m bir tam sayı. Lean kodunda ise karşılık gelen sınır m + 5'tir.

Bu fark yüzeysel görünüyor ama matematiksel olarak gerçek. New Scientist, x + 3 = 6 denklemini çözme benzetmesini kullanıyor: x'in 4'ün altında olduğunu kanıtlamak da 5'in altında olduğunu kanıtlamak da doğru ifadelerdir, ancak ikincisi daha fazla olasılığa izin verir ve dolayısıyla daha zayıftır. Başka bir deyişle, lemmayı Lean sürümü, makalenin kanıtlamayı amaçladığından daha azını kanıtlar.

Özellikle araştırmacılar, OpenAI'ın problemi çözmediğini iddia etmiyor. Hansen, ekibin doğal dildeki kanıtın doğru mu yanlış mı olduğu konusunda bir görüş belirtmediğini vurguluyor; tek bir teoremin birçok farklı doğru kanıtı olabileceği gibi, iki belge de bağımsız olarak geçerli olabilir. İtiraz, bunların aynı argüman olarak sunulmasına yönelik.

Formalizasyonlar neden sapar

Hansen böyle bir ayrılığın nasıl ortaya çıktığına dair açıklamasında şöyle diyor: Otomatik formalizasyon sistemi, derlenebilen kod üretme baskısı altındadır. Yazılı kanıtın bir bölümü çeviriye direndiğinde model, makalenin söylediğinden uzaklaşsa bile kodun geçmesi için matematiği ayarlayarak sorunun etrafından dolaşabilir. Circelli çarpıcı biçimde durumun ciddiyetini şöyle ifade ediyor: formalizasyon, insanların argümanları gerçekten okuduğu hakemli incelemenin bir alternatifi olarak konumlandırılıyor ve ekibin bulguları, yapay zeka otomatik formalizasyonunun bu rol için henüz uygun olmadığına işaret ediyor.

İki haftalık elle denetim

Uyuşmazlığın yerini bulmak zahmetliydi. Ekip önce ChatGPT'den iki sürüm arasındaki olası farkları taramasını istedi, ardından her birini elle inceledi — ve önerilerin çoğu sonunda tutarlı çıktı. Bu çaba yaklaşık iki hafta sürdü; oysa OpenAI, aracılarının kanıtları üretmek için başlangıçta 88 saat harcadığını söylemişti. Bastounis, üretim hızının güvenilir matematik üretmenin yalnızca bir parçası olduğunu belirtiyor.

OpenAI, New Scientist'e verdiği demeçte uyumsuzluğun farkında olduğunu, iki kanıttan hiçbirinin geçersiz olarak görülmediğini, yazılı kanıttaki hataların tespit edildikçe düzeltileceğini ve aynı hafta yayımladığı 722 matematik makalesini formalize etmeye devam edeceğini bildirdi. Bu makalelerin yalnızca bir kısmı Lean kanıtlarıyla geliyor ve o Lean sürümleri elle denetlenmiş değil.

İfade ile kanıt

Imperial College London'dan Kevin Buzzard, burada temel olduğunu düşündüğü bir ayrım yapıyor: teoremin ifadesi ile kanıtı arasındaki ayrım. Fermat'nın son teoremi gibi bir ifadeyi Lean'da dile getirmek kolaydır ve Lean ifadesinin doğru şeyi söylediğinden emin olduğunuzda, onun derlenen bir kanıtına güvenebilirsiniz. Bunun ise, diye savunuyor Buzzard, insan tarafından okunabilir PDF hakkında hiçbir şey söylemediğini ekliyor. Buzzard, "Navier-Stokes probleminin doğru biçimde çözüldüğünden emin" olduğunu ancak "PDF'de açıklanan kanıtın doğru olduğundan çok daha az emin" olduğunu söylüyor.

Neden önemli

Formal doğrulama güçlü bir vaat taşıyor: bir makine bir argümanı baştan sona sertifikalar. Bu vaat ancak formalizasyon, ortaya konan iddiayı sadakatle kodlarsa geçerlidir. Bir model kodun derlenmesi için bir sınırı sessizce gevşetebiliyorsa, "formal olarak doğrulandı" ifadesi, sözde formalize ettiği makale hakkında güvenilir hiçbir şey söylemez hale gelir. Hansen, LLM tarafından üretilen kanıtların "insanlar tarafından okunması gerekeceğini", bunun da "matematikçiler üzerinde muazzam bir ek yük oluşturacağını" söylüyor. Yüzlerce makine tarafından üretilmiş makale artık dolaşımda ve formal sürümlerinin az bir kısmı elle denetlenmişken, darboğaz kanıt yazmaktan kanıtları denetlemeye kayıyor. Hansen'ın daha derin endişesi ise anlayışı dışarıya devretmenin bilim yapmanın amacını içinden boşaltacağıdır.