Pekin Üniversitesi bünyesinde matematikçi Dong Bin liderliğinde geliştirilen sistem, 2014 yılında Iowa Üniversitesi profesörü Dan Anderson tarafından ortaya atılan cebir problemini çözdü. Anderson, 2022 yılında hayatını kaybetmişti.

Araştırmacılara göre yapay zeka, onlarca yıllık matematik literatürünü analiz ederek problemi çözdü ve elde ettiği sonucu yine kendi başına doğruladı. Çalışma henüz hakem değerlendirmesinden geçmemiş olup 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.
Araştırmada kullanılan sistem, birden fazla bileşenden oluşuyor. “Rethlas” adlı akıl yürütme motoru, “Matlas” isimli teorem arama motorundan yararlanarak çö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.
Araştırmacılar, yapay zekanın söz konusu problemi yaklaşık 80 saatlik çalışma süresi içinde çözdüğünü ifade etti.
Bilim insanları, matematiksel ispatların yüksek doğruluk gerektirdiğini ve mevcut yapay zeka sistemlerinin hâlâ hata yapma veya “halüsinasyon” üretme riski taşıdığını vurguladı. Buna rağmen geliştirilen bu yaklaşımın, matematiksel araştırmaların önemli ölçüde otomatikleştirilebileceğini gösteren somut bir örnek sunduğu belirtiliyor.

Araştırmaya göre, insan rehberliği eklenmesi durumunda sürecin daha da hızlanabileceği ifade edilirken; yeni yaklaşımın, resmi ve gayri resmi akıl yürütme sistemlerini bir araya getirerek doğrulanabilir sonuçlar üretme konusunda umut vadettiği kaydedildi.
Okuyucu Yorumları 0 yorum