OpenAI'nin Navier-Stokes sürümü Yalın 4'ün resmi kanıtını içeriyordu

Dün OpenAI akışkanlar dinamiğindeki Navier-Stokes denklemleri hakkında uzun süredir devam eden bir soruyu çözen bir kanıtı duyurdu. Duyuru beklendiği gibi çok fazla ses getirdi. Ancak OpenAI'in çalışmasının kimsenin hakkında konuştuğunu görmediğim bir yönü var: Geleneksel insan tarafından okunabilen kanıtlarıyla aynı zamanda Yalın 4 resmi kanıtını da yayınladılar. Yakın zamanda yapay zeka kullanılarak pek çok başka matematiksel varsayım da çözüme kavuşturuldu ve bunlara özellikle Yalın 4 kullanılarak resmi kanıtlar da eşlik etti. Çok yakın zamana kadar, makine tarafından doğrulanabilen resmi kanıtların üretilmesi dayanılmaz derecede sıkıcıydı. 2005'te Henk Barendregt ve Freek Wiedijk şunu yazdı: Biçimlendirme için ne kadar çalışmaya ihtiyaç duyulduğuna dair bir gösterge vermek amacıyla, lisans düzeyindeki bir matematik ders kitabının bir sayfasını biçimlendirmenin yaklaşık bir çalışma haftası (sekiz çalışma saatinden beş iş günü) sürdüğünü tahmin ediyoruz. Temel kural buydu: sayfa başına kırk saat. Ve bu lisans ders kitapları bağlamında. Araştırma yayınları ders kitaplarından çok daha yoğundur. Ayrıca, bir ders kitabının 100. sayfası muhtemelen çoğunlukla 1. sayfadan 99. sayfaya kadar olan materyale dayanmaktadır. Bir araştırma makalesindeki bir cümle, daha önce yayınlanmış herhangi bir şeye atıfta bulunabilir. Diyelim ki bir araştırma makalesini biçimlendirmek, lisans ders kitaplarındaki sayfalardan 20 kat daha fazla çaba gerektiriyor. Daha sonra OpenAI'den itibaren 166 sayfalık makalenin resmileştirilmesi 132.800 insan-saat sürecektir. Yalın'daki kanıtlarını doğrulamak OpenAI 17 saat sürdü.

Devrimci kelimesini kullanmakta tereddüt ediyorum ama herhangi bir şeyin maliyetini dört kat azaltmak devrim niteliğindedir. Sadece küçük bir blog yazısı için çalışmamı kontrol etmek amacıyla resmi kanıtlar oluşturmak için yapay zekayı kullandım. İşimi kontrol etmesi için birine bir haftalık maaş ödemek zorunda kalsaydım bunu yapmayı hayal bile etmezdim. Resmi doğrulama sadece matematik için geçerli değildir. Örneğin, bir dizi güvenlik politikasının tutarlı olduğunu ve belirli varsayımlar göz önüne alındığında amaçlarına ulaştıklarını resmi olarak doğrulayabilirsiniz. Akıllı bir sözleşmenin belirli bir maksimum sorumluluk getirdiğini resmi olarak doğrulayabilirsiniz. Görev açısından kritik algoritmaların doğruluğunu doğrulayabilirsiniz. Bu problemler matematik araştırmasını resmileştirmekten daha kolaydır ve yatırım getirisini ölçmek daha kolaydır.