OpenAI'nın Navier-Stokes Lean Kanıtı Doğal Dil Sürümüyle Eşleşmiyor, Matematikçiler Diyor

İki Kanıt Arasındaki Uyuşmazlık

OpenAI, 8 Eylül'de Navier-Stokes probleminin çözümünü bulduğunu duyurdu; bu matematikte en bilinen açık problemlerden biridir. Şirket kanıtı iki sürümde yayınladı: biri doğal dilde yazılmış, İngilizce ve matematiksel sembollerin birleşimi, bir insan matematikçinin yazacağı gibi; diğeri ise bilgisayar dili olan Lean'de yazılmış, formalizasyon için tasarlanmış ve bilgisayara her mantıksal önermenin mekanik olarak doğrulanmasına olanak tanıyor.

Şimdi matematikçiler grubu, bu iki sürümün birbiriyle eşleşmediğini söylüyor. Cambridge Üniversitesi'nden Anders Hansen ve Fabian Chirchet, Londra King's College'dan Alexander Bastounis ile birlikte, OpenAI'nın modelinin kanıtın bir kısmını Lean'e çevirirken yanlış çevirdiğini iddia ediyor. Araştırmacılar vurguluyor ki bu, kanıtların yanlış olduğu veya OpenAI'nın problemi çözemediği anlamına gelmiyor; ancak her zaman yapay zekâ tarafından üretilen matematiksel sonuçlara güvenilip güvenilmeyeceği konusunda şüphe uyandırıyor.

Zayıflatılmış Lemma

Grubun iddiası, lemma 8.6 olarak adlandırılan kanıtın bir kısmını ilgilendiriyor. Doğal dilde yazılmış kanıtta bu kısmın eşitliği, belirli bir değerin m + 4'ten küçük olmasını gerektiriyor; burada m tam sayıdır. Lean kanıtında eşdeğer değer m + 5'ten küçük olmalı ki bu matematiksel olarak daha zayıf bir ifadedir. Her iki ifade de doğru olabilir ama farklı şeyler söylüyor ve Lean sürümü daha fazla olası cevabı kabul ediyor.

Araştırmacılara göre, sapma şundan kaynaklanıyor: yapay zekâ'nın derlenen bir Lean kanıtı oluşturması gerekiyor, yani kod tamamen tutarlı olmalı ve hata vermemeli. Model derlenmeyen bir kısm bulursa, doğal dilde yazılmış kanıttan sapma anlamına gelse bile bir geçici yol bulmaya çalışacaktır. OpenAI iki kanıtı aynı olarak sunuyor ve GitHub'da deponun çalışmada verilen sonuçların Lean 4 formalizasyonlarını içerdiğini duyuruyor.

Yapay Zekâ Kanıtlarını Doğrulama Yükü

Sapmayı bulmak emek yoğun bir işe dönüştü. Grup ChatGPT'den iki sürüm arasındaki olası uyuşmazlıkları bulmasını istedi, ardından her birini elle doğruladı. Önerilen birçok uyuşmazlık kontrol sonrası geçersiz çıktı. Toplamda, gerçek bir sapmayı tespit etmek grubun yaklaşık iki hafta sürdü; OpenAI'nın ajanlarının ise kanıtları üretmesi 88 saat sürmüş.

Problem özellikle güncel çünkü OpenAI 722 matematiksel çalışma serisi yayınladı ve bunların yalnızca bir kısmına Lean kanıtları eşlik ediyor ki bunlar elle doğrulanmamış. Londra Imperial College'dan Kevin Buzzard, Navier-Stokes probleminin doğru çö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öyledi. Hansen, sağlam otomatik formalizasyon teknikleri geliştirmek için daha fazla çalışma gerektiğini ve bunun nihai yolun tamamen bilinmediğini belirtti.

Kaynaklar: newscientist.com