OpenAI, kendi bünyesinde geliştirdiği öncü bir modelin ürettiği geniş kapsamlı matematik araştırması koleksiyonunu yayımladı ve matematikçilerin makine tarafından üretilen yüzlerce sonuca erişmesini sağladı.
372 araştırma ailesi altında düzenlenen 722 makaleden oluşan koleksiyon, herkese açık bir GitHub deposunda yer alıyor. Çalışmalar saf matematik, teorik bilgisayar bilimi ve matematiksel fizik alanlarını kapsıyor.
Sonuçların bir kısmı, uzun matematiksel akıl yürütme zincirleri gerektiren problemleri ele alıyor. OpenAI, bilgisayarların altta yatan mantığı denetlemesine imkan tanımak adına bir çok ispatın Lean dilindeki resmîleştirilmiş sürümlerini de yayımladı.
Yüzlerce Sonuç
Depo, sayı teorisi, karmaşıklık teorisi, geometri ve matematiksel fiziği içeren problemleri kapsıyor. Bazı sonuçlar, küçük ilerlemelerin bile ciddi teknik çaba gerektirdiği alanlara kadar uzanıyor.
Örneklerden biri, pi sayısının irrasyonellik üssüyle bağlantılı. Söz konusu değer, rasyonel sayıların pi sayısına ne kadar yakın yaklaşabileceğini ölçüyor. Model, bu yaklaşımın matematiksel davranışını inceleyen bir sonuç ortaya koydu.
Başka bir araştırma ailesi ise NP-zorluğunu inceliyor. Hesaplamalı karmaşıklık teorisinde yer alan bu problemler, verimli bir şekilde çözülmesi zor kabul edilen görevleri kapsıyor. Modelin çalışması, bu geniş araştırma alanına yeni matematiksel sonuçlar kazandırıyor.
Diğer makaleler Mahler varsayımları, aritmetik diziler ve serbest grup faktörlerini içeren soruları ele alıyor. Koleksiyon ayrıca kuantum Heisenberg ferromanyetleri ve rölativistik Vlasov-Maxwell denklemleri üzerine çalışmaları da içeriyor.
OpenAI, tekil sonuçların birbiriyle nasıl bağlandığını göstermek için ilişkili makaleleri araştırma aileleri altında topladı. Depoda ayrıca modelin akıl yürütme sürecinin kısa özetlerini içeren 10 araştırma ailesi yer alıyor.
Lean Bir Kontrol Katmanı Ekliyor
Lean, bu yayın için önemli bir doğrulama katmanı sağlıyor. Bu programlama dili, araştırmacıların matematiksel ifadeleri ve ispatları resmî koda dönüştürmesine olanak tanıyor. Böylece bir bilgisayar, her mantıksal adımın belirtilen varsayımlardan türetilip türetilmediğini denetleyebiliyor. Ancak bu durum, koleksiyondaki her araştırma iddiasının kesin olarak doğru olduğu anlamına gelmiyor.
Birçok makalenin henüz resmî Lean sürümü yok. OpenAI, araştırmacılar doğrulama çalışmalarını tamamladıkça daha fazla resmîleştirilmiş kod ekleyeceğini belirtiyor.
Depo aynı zamanda makale revizyonlarını takip ediyor ve atıf kılavuzu sunuyor. Bu da yazarlar önceki bir çalışmayı düzelttiğinde veya genişlettiğinde araştırmacılara daha net bir kayıt sağlıyor. OpenAI yayın sürecini, Institute for Advanced Study bünyesindeki bağımsız Matematik ve YZ Danışma Grubu’nun tavsiyeleriyle geliştirdi.
Model Binlerce Problemi Test Etti
OpenAI, matematiksel değerlendirmesinin ölçeğine dair detayları da paylaştı. Model, araştırma sürecinde yaklaşık 4.000 problemi çözmeyi denedi.
Kabul edilen bir sonuç için ortalama olarak yaklaşık üç saatlik ChatGPT Pro düşünme süresine eşdeğer hesaplama gücü kullanıldı. OpenAI ayrıca denenen problemler ve ortaya çıkan araştırma sonuçlarına ilişkin ek istatistikler de yayımladı.
Şirket, akıl yürütme özetlerinin araştırmacılara modelin seçilen matematik sorularına nasıl yaklaştığını daha yakından inceleme imkanı sunduğunu belirtiyor. Bu özetler, Lean dilindeki resmî ispatlardan ayrı tutuluyor.
OpenAI, YZ tarafından üretilen büyük matematiksel sonuçları anlamaya odaklanan atölyeleri, konferansları ve özel programları desteklemeyi planlıyor. Şirket ayrıca matematikçilerden gelecek geri bildirimlerin gelecekteki paylaşımlara yön vermesini bekliyor.
Dolayısıyla bu yayın yalnızca bir makale koleksiyonu sunmuyor. Aynı zamanda makine tarafından üretilen matematiğin, yeniden üretilebilir kayıtlar, bilgisayar tarafından kontrol edilebilen kanıtlar ve sonuçların ortaya çıkış sürecine ilişkin daha fazla görünürlükle araştırma sürecine nasıl dahil olabileceğini test ediyor.
Kaynak: https://interestingengineering.com/ai-robotics/openai-largest-math-release-lean-proofs
