h1’in tek çalıştırma başarı oranı 5 Erdős probleminde %82,5, altı problemde %68,75 oldu

Yapay zekâ teorem ispatlama sistemi h1, birlikte değerlendirilen beş Erdős probleminde tek çalıştırmada %82,5 başarı oranına ulaştı. Başarılı ispat başına API tarifesiyle hesaplanan ortalama maliyet 121 dolar (yaklaşık 160 bin Güney Kore wonu) oldu. Aynı problem grubunda AlphaProof Nexus’un başarı oranı %76, maliyeti ise 317 dolardı (yaklaşık 420 bin Güney Kore wonu). Altıncı problem de hesaba katıldığında h1’in başarı oranı düştü.

Meta’nın (META) FAIR araştırma birimi ile New York Üniversitesi (NYU) araştırmacılarının da yer aldığı ekip, “h1: A Taste of the Bitter Lesson in Automated Theorem Proving” başlıklı makaleyi 25 Ekim’de yayımladı. Araştırmacılar makalede h1’i diğer teorem ispatlama sistemleriyle performans ve maliyet bakımından karşılaştırdı; çeşitli kıyaslama kümelerinde dil modellerinin ispat yeteneğini değerlendirdi.

AlphaProof Nexus ile karşılaştırmaya, üç sistemin de en az bir kez çözebildiği beş Erdős problemi dahil edildi. Sistem yapılandırmalarının etkisini karşılaştırmak için h1 ve AlphaProof Nexus’ta aynı Gemini 3.1 Pro modelinden yararlanıldı.

Bu beş problemde h1’in tek çalıştırmadaki başarı oranı %82,5 ile AlphaProof Nexus’un %76’sını aştı. Yalnızca başarılı ispatlar hesaba katıldığında ortalama maliyet h1 için 121 dolar, AlphaProof Nexus için 317 dolar oldu.

h1, dil modelinin Lean 4 ispat dosyaları yazıp düzenlemesiyle çalışıyor. Doğrulayıcı hata veya henüz ispatlanması gereken hedefleri geri gönderdiğinde model bu geri bildirimi kullanarak yeniden deniyor.

Lean 4, matematiksel önermeleri ve ispatları belirli bir biçimde ifade edip makineyle denetlemeye yarayan bir araç. Bu nedenle doğrulama sonucu, girilen biçimsel önermenin ispatının kabul edilip edilmediğini gösteriyor.

Araştırmacılar problemi önceden birkaç adıma bölmedi ve belirli ispat araçlarının sabit bir sırayla kullanılmasını şart koşmadı. Modelin çalışma dosyasını koruyup doğrulama geri bildiriminden ve kendi denetiminden yararlanarak sonraki adımı belirlemesine izin verdi.

Başka bir kıyaslama kümesinde GPT-5.5 ile çalışan h1, PutnamBench’teki 672 problemin 670’ini çözdü. Ancak PutnamBench’in resmî sıralama tablosunda 672 problemin tamamını çözen sistemler de bulunduğundan, 670 çözüm en iyi sonuç değil.

GPT-5.6 Sol ile yapılan deneyde sistem, FATE-X’teki 100 problemin 90’ını ve FormalConjectures100-Solved’daki 100 problemin 78’ini çözdü. Bu kıyaslama sonuçları, her problem için bir kez çalıştırma yapılan deneylerden elde edildi.

Makalede verilen dolar maliyetleri, kaydedilen token kullanımına API fiyat tarifesinin uygulanmasıyla hesaplandı. Bu rakamlar gerçek harcamayı göstermiyor. 121 ve 317 dolarlık maliyetler de başarısız görevleri dışarıda bırakıp yalnızca başarılı ispatları kapsıyor.

Başarısız denemelerin maliyeti de dahil edilen h1 içi karşılaştırmada, tek bir uzun çalıştırmayla %82,5 başarı oranına ulaşmanın ortalama maliyeti 138 dolar (yaklaşık 180 bin Güney Kore wonu) oldu. Aynı başarı oranı üç çalıştırma yöntemiyle sağlandığında maliyet 202 dolara (yaklaşık 270 bin Güney Kore wonu) çıktı. Bu hesaplama, AlphaProof Nexus ile yapılan maliyet karşılaştırmasından farklı.

Karşılaştırmaya alınmayan Erdős 125 probleminde h1’in 16 denemesinin tümü Lean çalıştırma zaman aşımıyla sonuçlandı. Bu problemde AlphaProof Nexus daha başarılı oldu.

Altı problemin tamamı hesaba katıldığında h1’in tek çalıştırmadaki başarı oranı %68,75’e geriledi ve AlphaProof Nexus’un %71,67’lik oranının altında kaldı. Bu nedenle beş problemde görülen başarı ve maliyet üstünlüğünü bütün teorem ispatlama görevlerine genellemek mümkün değil.

Araştırmacılar, FormalConjectures’ta çözümsüz olarak sınıflandırılan sekiz önermeyi ispatladıklarını bildirdi. Makalenin ekinde, Written on the Wall II kapsamındaki iki problemin önerme ifadeleri değiştirildikten sonra ispatlandığı belirtiliyor.

Depoya birleştirilen ilgili değişiklik talebi, bu problemlerin beşini çözülmüş olarak işaretleyip Lean ispatlarına bağlantı veriyor. Makalede bildirilen sekiz problem ile değişiklik talebinde gösterilen beş problem aynı kapsamı taşımıyor.

Bir ispatın makine tarafından kabul edilmesiyle, girilen önermenin amaçlanan matematik problemini doğru ifade etmesi birbirinden ayrı konular. Makalenin eki de biçimsel hale getirilen önermelerde sorun bulunabileceğini belirtiyor.

Çalışma matematik teoremlerinin ispatlanmasına yönelik deneyleri ele aldı; blokzincir veya akıllı sözleşme doğrulama performansını değerlendirmedi.