OpenAI'nin Navier-Stokes kanıtı, 17 saatte doğrulanan Lean 4 formalizasyonuyla birlikte yayınlandı

Bu haftanın başında OpenAI, akışkan dinamiğini yöneten kısmi diferansiyel denklemler olan Navier-Stokes denklemleriyle ilgili uzun süredir cevaplanmayan bir soruyu çözdüğünü söylediği bir kanıt duyurdu. İddia hemen ses getirdi. Ancak blogunda yazan John D. Cook'a göre duyurunun en önemli ayrıntısı neredeyse tamamen gözden kaçıyor: OpenAI, geleneksel, insan tarafından okunabilir makalesinin yanında, sonucun Lean 4 formel kanıtını da aynı anda yayınladı; Lean 4, bir argümanın her adımını mekanik olarak kontrol eden bir kanıt asistanıdır.

Gözden kaçan ayrıntı

Hacker News ana sayfasında öne çıkan yazısına göre Cook, OpenAI'nin 166 sayfalık bir makale ve kanıtın Lean 4 formalizasyonunu aynı anda yayınladığını belirtiyor. Ayrıca bunun izole bir jest olmadığına dikkat çekiyor: AI desteğiyle yakın zamanda çözülen birçok matematiksel konjektür de benzer şekilde, özellikle Lean 4 formel kanıtlarıyla birlikte geldi.

Formalizasyon eskiden sayfa başına bir hafta tutuyordu

Bunun neden önemli olduğunu açıklamak için Cook, 2005 yılında Henk Barendregt ve Freek Wiedijk'ın yaptığı bir tahmine geri dönüyor: lisans düzeyindeki bir matematik ders kitabının tek bir sayfasını formalize etmek yaklaşık bir iş haftası, yani kırk saat alıyordu. Üstelik bu ders kitapları içindi; kitapta 100. sayfa çoğunlukla 1'den 99'a kadar olan sayfalara dayanır. Bir araştırma makalesindeki bir cümle ise daha önce yayınlanmış herhangi bir şeye atıf yapabilir; bu yüzden yoğunluk, dolayısıyla gereken emek çok daha fazladır.

Cook'un kaba hesabı şöyle: bir araştırma makalesi sayfasının formalize edilmesinin bir ders kitabı sayfasından yirmi kat zor olduğunu varsayalım. OpenAI'nin 166 sayfalık makalesinin elle formalize edilmesi bu durumda yaklaşık 132.800 kişilik saat tutardı. Bunun yerine OpenAI'nin kanıtın Lean ile doğrulanması 17 saat sürdü. Cook, bu kelimeyi kullanmaya çekindiğini yazıyor ama herhangi bir şeyin maliyetini dört büyüklük mertebesi düşürmek devrim niteliğindedir. 132.800 rakamı ölçülmüş bir kıyas noktası değil, 2005 tarihli bir pratik kuraldan yapılan bir dış değerlendirmedir; ancak cömert bir hata payıyla bile fark çarpıcıdır.

Cook, AI'yı kendi çalışmasını kontrol etmek için bir blog yazısında formel kanıtlar üretmek amacıyla zaten kullandığını ekliyor; bu kontrol için birine bir haftalık maaş ödemek gerekseydi bunu aklından bile geçirmezdi.

Matematiğin ötesinde doğrulama

Cook'a göre formel doğrulama salt matematiğe sıkışmış değil. Saydığı uygulamalar arasında şunlar var: bir güvenlik politikaları kümesinin içsel olarak tutarlı olduğunu ve belirtilen varsayımlar altında amacına gerçekten ulaştığını kanıtlamak; bir akıllı sözleşmenin belirli bir azami yükümlülük getirdiğini kanıtlamak; ve görev açısından kritik algoritmaların doğruluğunu teyit etmek. Cook'a göre bu problemler araştırma matematiğini formalize etmekten daha kolay ve yatırımın getirisi de nicel olarak ifade edilmesi daha kolaydır.

Neden önemli

Navier-Stokes sonucu kendi başına büyük bir araştırma olayıdır; ancak kalıcı haber onun çevresindeki ekonomi olabilir. AI artık formel kanıtları elle formalizasyondan birkaç büyüklük mertebesi daha düşük maliyetle üretebiliyorsa, makine doğrulaması ders kitabı alıştırmalarına ayrılmış bir lüks olmaktan çıkıp pratik bir varsayılan hale gelir.

Özellikle AI destekli matematik için bu, güven sorusunu değiştirir. Lean ile doğrulanmış bir kanıtın bir modelden veya yazarlarından inanılması gerekmez, çünkü kanıt asistanı her adımı doğrular. Ve Cook'un gözlemlediği gibi AI ile çözülen konjektürler artık rutin olarak Lean 4 formalizasyonlarıyla geliyorsa, makine doğrulaması büyük sonuçların kabulü için beklenen standart haline gelebilir.

Yazılım mühendisliği için maliyetteki aynı çöküşün daha acil getirileri var. Güvenlik politikaları, akıllı sözleşmeler ve görev açısından kritik algoritmalar, Cook'un ifadesiyle araştırma matematiğinden daha kolay hedeflerdir; bu da formel yöntemlerin, hataların en pahalıya mal olduğu yerde egzotik olmaktan çıkıp rutin hale gelebileceğini düşündürüyor.