Pekin Üniversitesi’nde matematikçi Dong Bin’in liderliğinde geliştirilen yeni bir sistem, 2014 yılında Iowa Üniversitesi profesörü Dan Anderson tarafından ortaya konulan bir cebir problemini başarıyla çözdü. Anderson, 2022 yılında hayatını kaybetmişti.

Araştırmacılar, yapay zekanın onlarca yıllık matematik literatürünü analiz ederek problemi çözdüğünü ve bulduğu sonucu kendi başına doğruladığını açıkladı. Bu çalışma, henüz hakem değerlendirmesinden geçmemiş olmasına rağmen arXiv platformunda yayımlandı.

“İNSAN MÜDAHALESİ YOK”

Geliştirilen sistemin, değişmeli cebirdeki açık bir problemi “neredeyse hiçbir insan müdahalesi olmadan” çözdüğünü ve ispatın otomatik olarak resmileştirildiğini belirten ekip, bu durumun önemine dikkat çekti.

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 faydalanarak çözüm stratejileri geliştiriyor. Daha sonra “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 barındıran geniş bir kütüphaneye dayanmaktadır.

80 SAATTE ÇÖZEBİLDİ

Araştırmacılar, yapay zekanın bu problemi yaklaşık 80 saatlik bir çalışma süresi içinde çözdüğünü belirtmektedir.

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ığına vurgu yaptı. Ancak geliştirilen bu yaklaşımın, matematiksel araştırmaların önemli ölçüde otomatikleştirilebileceğini gösteren somut bir örnek sunduğu ifade edilmektedir.

GELECEĞE DAİR UMUT TAŞIYOR

Araştırmaya göre, insan rehberliği eklendiğinde sürecin daha da hızlanabileceği belirtilmekte; yeni yaklaşımın, resmi ve gayri resmi akıl yürütme sistemlerini bir araya getirerek doğrulanabilir sonuçlar üretme konusunda umut vaat ettiği kaydedilmektedir.