Yapay zeka alanında matematik teoremi ispatlama konusunda önemli bir ilerleme kaydedildi. Araştırmacılar, geleneksel otomatik teorem ispatlama sistemlerindeki önemli bir eksikliği gidermek için yeni bir yaklaşım geliştirdi.
Mevcut sistemlerin çoğu 'Kolay Mod' olarak adlandırılan bir yöntemle çalışıyor - yani ispat edilecek teorem önceden sistem tarafından biliniyor. Ancak bu durum, gerçek matematikçilerin karşılaştığı zorluklardan çok farklı. Yeni geliştirilen sistem ise 'Zor Mod'da çalışıyor: önce teoremi keşfetmeli, sonra ispatlamalı.
'Discover and Prove' (Keşfet ve İspatla) adlı bu framework, büyük dil modellerinin doğal dil işleme yeteneklerini kullanarak mantık yürütme yapıyor. Sistem, kendi kendini sorgulama mekanizması ile önce problemi analiz ediyor, çözümü buluyor, ardından formal matematik diline çeviriyor.
Test sonuçları oldukça etkileyici. CombiBench veri setinde önceki en iyi sistemin çözdüğü 7 problemin yanına, yeni sistem 10 problem çözmeyi başardı. PutnamBench testinde ise bu alanda ilk başarılı sonuçları elde eden sistem oldu.
Bu gelişme, yapay zekanın matematik alanındaki gerçek kapasitesini ölçmek için daha objektif bir değerlendirme imkanı sunuyor.