Generative reward models for formal theorem proving: Methods, benchmarks, and tree search integration
Biçimsel teorem ispatlama için üretken ödül modelleri: Metotlar, denektaşları ve ağaç yapılı arama entegrasyonu
- Tez No: 999908
- Danışmanlar: DR. ÖĞR. ÜYESİ GÖZDE GÜL ŞAHİN
- Tez Türü: Yüksek Lisans
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2025
- Dil: İngilizce
- Üniversite: Koç Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: Belirtilmemiş.
Özet
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.
Özet (Çeviri)
Automated theorem proving aims to generate machine-verifiable proofs with minimal human intervention, but effective proof search remains challenging. Tree search algorithms require guidance to navigate exponentially large proof spaces. However, existing approaches suffer from fundamental limitations. Log-probability heuristics conflate generation likelihood with step quality, binary feedback from proof assistants provides no notion of progress, and discriminative reward models compress complex reasoning into opaque scalar values. In addition, implementation fragmentation limits reproducibility, and the absence of evaluation frameworks blocks systematic development of reward models for formal mathematics. This thesis makes three contributions addressing these challenges. First, we develop TreeThink, a modular Python library providing unified implementations of best-first search, beam search, and Monte Carlo tree search for formal theorem proving. The architecture cleanly separates search strategy, environment interaction, and model inference, enabling reproducible experimentation and fair comparison across algorithms. All components support asynchronous execution and batched inference for computational efficiency. Second, we introduce a framework for generative reward models that produce natural language critiques evaluating proof steps. Unlike discriminative models that output scalar scores without explanation, our approach generates structured textual feedback describing correctness, progress toward goals, and strategic value, with embedded numerical scores for integration into tree search. A key design element is conditioning reward generation on environmental feedback from proof assistant execution, grounding evaluations in concrete compiler responses rather than predictions alone. We study both zero-shot deployment using pretrained models and reinforcement learning on proof trajectories to align critique scores with proof outcomes. Third, we introduce FormalRewardBench, the first benchmark for evaluating reward models in formal theorem proving. The benchmark consists of preference pairs where correct Lean 4 proofs are paired with incorrect variants generated through five error injection strategies targeting realistic failure modes, including forced mistakes, minimal variations, complex incorrect proofs, natural language justification, and Python code injection. Quality control ensures errors are semantic rather than trivial, and evaluation protocols support both pointwise and pairwise reward models with position bias mitigation. Together, these contributions advance neural theorem proving by providing modular infrastructure for systematic experimentation, richer guidance signals through interpretable natural language feedback grounded in execution, and evaluation frameworks that enable principled development of reward models for formal mathematics. Our work addresses key limitations in automated theorem proving and establishes foundations for more capable and interpretable proof search systems.
Benzer Tezler
- Messiaen the liturgist: A contextual analysis of the vingt regards sur l'Enfant-Jésus
Litürjist Messiaen: Vingt regards sur l'Enfant-Jésus'un bağlamsal analizi
ROBERT AARON MCDONALD
- Architecture of constraints: A mass customization oriented approach for housing design
Kısıtlarla tanımlanan mimarlık: Kitlesel özelleştirme odaklı konut tasarımı
BENGİSU İLKSOY
Yüksek Lisans
İngilizce
2015
Mimarlıkİstanbul Teknik ÜniversitesiMimarlık Ana Bilim Dalı
DOÇ. DR. MİNE ÖZKAR KABAKÇIOĞLU
- Tarihi ahşap yapıların onarımı için kural tabanlı yaklaşım: Göğceli Cami örneği
Rule based approach for historical timber structure: case of Göğceli Mosque
MEHMET SALİH ÖZALP
Yüksek Lisans
Türkçe
2024
Mimarlıkİstanbul Teknik ÜniversitesiBilişim Ana Bilim Dalı
PROF. DR. MİNE ÖZKAR KABAKÇIOĞLU
- Performans yönetimi için dinamik bir stratejik kontrol modeli
A Dynamic strategic control model for performance management
SEÇKİN POLAT
Doktora
Türkçe
1992
Endüstri ve Endüstri Mühendisliğiİstanbul Teknik ÜniversitesiPROF. DR. MEHMET HALUK ERKUT
- Reinforcement-learning control of a hybrid airship using a high-fidelity digital twin
Yüksek doğruluklu dijital ikiz kullanarak bir hibrit hava gemisinin pekiştirmeli öğrenme ile denetimi
NIKOLAY LYAN
Yüksek Lisans
İngilizce
2025
Havacılık ve Uzay Mühendisliğiİstanbul Teknik ÜniversitesiUçak ve Uzay Mühendisliği Ana Bilim Dalı
YRD. DOÇ. DR. İSMAİL BAYEZİT