Pekin Üniversitesi’nden yapay zeka, 10 yıllık karmaşık bir cebir problemini 80 saatte çözerek matematik dünyasında dikkat çekti. Sistem, insan müdahalesi olmadan ispatı da otomatik olarak resmileştirdi.
Pekin Üniversitesi’nden matematikçi Dong Bin liderliğindeki bir ekip, 2014 yılında Iowa Üniversitesi’nden Dan Anderson tarafından ortaya atılan 10 yıllık bir cebir problemini yapay zeka kullanarak saatler içinde çözdü. Problem, Anderson’ın 2022 yılındaki vefatından sonra çözülememişti.
Geliştirilen yapay zeka sistemi, on yıllarca süren matematiksel literatürü analiz ederek problemi çözdü ve elde ettiği sonucu kendi başına doğruladı. Henüz hakem değerlendirmesinden geçmemiş olan çalışma, arXiv platformunda yayımlandı.
Ekip, geliştirdikleri sistemin değişmeli cebirdeki açık bir problemi neredeyse hiçbir insan müdahalesi olmadan çözdüğünü ve ispatı otomatik olarak resmileştirdiğini belirtti. Bu başarı, matematiksel araştırmaların otomasyon potansiyelini gözler önüne seriyor.
Sistem, ‘Rethlas’ adlı akıl yürütme motorunu kullanarak ‘Matlas’ isimli teorem arama motorundan stratejiler geliştiriyor. Ardından ‘Archon’ adlı ikinci bir sistem, bu çözümü ‘LeanSearch’ aracılığıyla resmi bir ispat haline getiriyor.
Ortaya çıkan ispatlar, bir programlama dili ve teorem ispatlayıcı olan Lean 4 üzerinde doğrulanıyor. Bu doğrulama süreci, yüz binlerce matematiksel tanım ve teorem içeren geniş bir kütüphaneye dayanıyor.
Araştırmacılar, yapay zekanın söz konusu problemi yaklaşık 80 saatlik bir çalışma süresi içinde tamamladığını belirtti. Bu durum, karmaşık matematiksel sorunların çözümünde yapay zekanın hızını ve verimliliğini gösteriyor.
Bilim insanları, matematiksel ispatların yüksek doğruluk gerektirdiğini ve mevcut yapay zeka sistemlerinin hala hata yapma veya ‘halüsinasyon’ üretme riski taşıdığını vurguladı. Ancak bu yeni yaklaşım, matematiksel araştırmaların önemli ölçüde otomatikleştirilebileceğine dair somut bir örnek sunuyor.
Araştırmaya göre, insan rehberliği eklendiğinde sürecin daha da hızlanabileceği ifade ediliyor. Yeni yaklaşımın, resmi ve gayri resmi akıl yürütme sistemlerini bir araya getirerek doğrulanabilir sonuçlar üretme potansiyeli taşıdığı kaydedildi.
Yorum Yap