Pekin Üniversitesi’nde geliştirilen yapay zeka, 10 yıl önce ortaya atılan karmaşık bir cebir problemini 80 saatte çözerek matematik dünyasında dikkat çekti.
Pekin Üniversitesi’nde matematikçi Dong Bin liderliğindeki bir ekip, 2014 yılında Iowa Üniversitesi profesörü Dan Anderson tarafından ortaya atılan 10 yıllık bir cebir problemini yapay zeka kullanarak çözdü. Yapay zeka, onlarca yıllık matematiksel literatürü analiz ederek problemi çözüp sonucunu kendi başına doğruladı. Çalışma henüz hakem değerlendirmesinden geçmedi ve arXiv platformunda yayınlandı.
Ekip, geliştirdikleri sistemin değişmeli cebirdeki açık bir problemi neredeyse insan müdahalesi olmadan çözdüğünü ve ispatı otomatik olarak resmileştirdiğini belirtti. Araştırmada kullanılan sistem, ‘Rethlas’ adlı akıl yürütme motoru ile ‘Matlas’ isimli teorem arama motorunu entegre ederek çözüm stratejileri geliştiriyor. Ardından ‘Archon’ adlı ikinci sistem, bu çözümü ‘LeanSearch’ aracılığıyla resmi bir ispat haline getiriyor.
Ortaya çıkan ispatlar, aynı zamanda bir programlama dili ve etkileşimli teorem ispatlayıcı olan Lean 4 üzerinde doğrulanıyor. Bu sistem, yüz binlerce matematiksel tanım ve teorem içeren geniş bir kütüphaneye dayanıyor. Yapay zekanın bu problemi yaklaşık 80 saatlik çalışma süresi içinde çözdüğü ifade edildi.
Bilim insanları, matematiksel ispatların yüksek doğruluk gerektirdiğini ve mevcut yapay zeka sistemlerinin hata yapma veya halüsinasyon üretme riski taşıdığını vurguladı. Buna rağmen geliştirilen bu yaklaşım, matematiksel araştırmaların önemli ölçüde otomatikleştirilebileceğini gösteren somut bir örnek sunuyor.
Araştırmaya göre, insan rehberliği eklenmesi durumunda sürecin daha da hızlanabileceği belirtildi. Yeni yaklaşım, resmi ve gayri resmi akıl yürütme sistemlerini bir araya getirerek doğrulanabilir sonuçlar üretme konusunda umut vadediyor.
Yorum Yap