Biçimsel teorem ispatlama için üretken ödül modelleri: Metotlar, denektaşları ve ağaç yapılı arama entegrasyonu

Otomatik teorem ispatı, insan müdahalesini en aza indirerek makine tarafından doğrulanabilir matematiksel kanıtlar üretmeyi amaçlar; ancak etkili ispat araması hâlâ önemli bir zorluktur. Ağaç arama algoritmaları, üstel olarak büyüyen ispat uzaylarında hangi durumların araştırılmaya değer olduğunu belirlemek için yönlendirmeye ihtiyaç duyar. Mevcut yaklaşımlar temel sınırlamalara sahiptir: log-olasılık temelli sezgiler üretim olasılığını adım kalitesiyle karıştırır, ispat yardımcılarından gelen ikili geri bildirim ilerleme hakkında bilgi vermez ve ayrık ödül modelleri karmaşık muhakemeyi açıklamasız tek bir sayıya indirger. Ayrıca, altyapı parçalanmışlığı tekrarlanabilirliği zorlaştırmakta ve değerlendirme çerçevelerinin yokluğu, biçimsel matematikte ödül modellerinin sistematik gelişimini engellemektedir. Bu tez, söz konusu sorunları ele alan üç temel katkı sunmaktadır. İlk olarak, biçimsel teorem ispatı için en-iyi-önce arama, ışın arama ve Monte Carlo ağaç aramasını birleştiren modüler bir Python kütüphanesi olan TreeThink geliştirilmiştir. Mimari, arama stratejisini, ortam etkileşimini ve model çıkarımını açık biçimde ayırarak yeniden üretilebilir deneyler ve adil algoritma karşılaştırmaları yapılmasına olanak tanır. Tüm bileşenler, hesaplama verimliliği için asenkron yürütme ve toplu çıkarımı destekler. İkinci olarak, ispat adımlarını değerlendiren doğal dil açıklamaları üreten üretici ödül modelleri için bir çerçeve sunulmuştur. Sayısal değerler üreten ayrık modellerin aksine, bu yaklaşım doğruluk, hedefe ilerleme ve stratejik değer hakkında yapılandırılmış metinsel eleştiriler üretir ve ağaç arama algoritmalarında kullanılmak üzere sayısal skorlar içerir. Kritik tasarım unsuru, değerlendirmeyi yalnızca tahminlere değil, ispat yardımcısının yürütme çıktılarından gelen çevresel geri bildirime koşullamaktır. Bu çerçeve, hem önceden eğitilmiş modellerle sıfır-atış (zero-shot) kullanım hem de ispat yörüngeleri üzerinde pekiştirmeli öğrenme ile eğitimi kapsamaktadır. Üçüncü olarak, biçimsel teorem ispatında ödül modellerini değerlendirmek için geliştirilen ilk kıyaslama seti olan FormalRewardBench tanıtılmaktadır. Bu kıyaslama, doğru Lean 4 ispatlarını; zorlanmış hatalar, minimal değişiklikler, karmaşık ancak hatalı ispatlar, doğal dil gerekçelendirme ve Python kodu enjeksiyonu gibi gerçekçi hata türlerini hedefleyen beş farklı stratejiyle üretilmiş yanlış varyantlarla eşleştiren tercih çiftlerinden oluşur. Kalite kontrol süreçleri, hataların yüzeysel değil anlamsal olmasını garanti eder ve değerlendirme protokolleri, konum yanlılığını azaltan noktasal ve ikili karşılaştırmaları destekler. Bu katkılar bir arada ele alındığında, otomatik teorem ispatında sistematik deneyler için birleşik bir altyapı, yürütme geri bildirimiyle temellendirilmiş yorumlanabilir yönlendirme sinyalleri ve biçimsel matematikte ödül modellerinin geliştirilmesini mümkün kılan değerlendirme çerçeveleri sunulmaktadır. Bu çalışma, otomatik teorem ispatındaki temel boşlukları ele almakta ve daha yetenekli ve yorumlanabilir ispat arama sistemleri için sağlam bir temel oluşturmaktadır.