LeanPRM: Doğal Dil İspat Doğrulaması İçin Lean Tabanlı Süreç Denetimi

Matematiksel İspat Doğrulamasında Darboğaz ve Mevcut Yaklaşımların Sınırları#

Yapay zeka sistemleri artık uzun ve zorlu matematiksel ispatlar yazabiliyor, ancak bu ispatların adım adım geçerliliğini kontrol etmek giderek büyüyen bir darboğaz haline geliyor. Eğitilmiş bir doğrulayıcı (verifier) modeli bu ispatları düşük maliyetle denetleyebilir; fakat böyle bir modeli eğitmek her adımda doğruluk etiketine ihtiyaç duyar ve açık uçlu ispatlar için bu etiketleri elde etmek oldukça zordur.

Mevcut yöntemler şu temel kısıtlamalarla karşılaşıyor:

• Etiketleri insan etiketleyicilerden almak yüksek maliyet yaratır.
• Etiketleri nihai yanıtlardan türetmek açık uçlu ispatlarda mümkün değildir çünkü bu ispatların tek bir sonuç değeri yoktur.
• Her bir ispatı Lean ortamında biçimselleştirmek (formalize etmek) uzman çabası gerektirir.

LeanPRM Çerçevesi ve Otomatik Etiketleme Süreci#

Doğal dildeki ispatlar için adım düzeyinde etiketler oluşturmak amacıyla Lean ispat asistanını kullanan LeanPRM çerçevesi geliştirilmiştir. Sistem şu adımlarla çalışır:

• Bir model, Lean'den herhangi bir geri bildirim almadan doğal dildeki bir ispatı eşleştirilmiş biçimsel (formal) bir ispatla birlikte yazar.
• Ardından Lean her bir adımı etiketler.
• İkinci bir model, yalnızca biçimsel sözdiziminden (syntax) kaynaklanan hataları eler; böylece negatif etiketler doğrudan matematiksel hataları işaret eder.
• Bu süreç sonucunda elde edilen LeanPRM veri seti, sıfır insan etiketlemesiyle 10.634 ispat ve 152 bin etiketlenmiş adım içerir.

Deneysel Sonuçlar ve Model Performansı#

LeanPRM üzerinde eğitilen modeller, süreç denetimi (process supervision) ve doğrulama kıyaslamalarında belirgin bir üstünlük sağlamaktadır:

• LeanPRM ile eğitilen bir Qwen3-4B doğrulayıcısı, ayrılmış 200 ispattan oluşan LeanPRM-Bench test setindeki tam adım etiketi doğruluğunu 48,2'den 74,7'ye çıkarırken, aynı temel model PRM800K üzerinde eğitildiğinde bu oran 60,3 seviyesinde kalmaktadır.
• Uluslararası Matematik Olimpiyatı (IMO) seviyesindeki problemlerde best-of-N seçiminde daha iyi ispatlar seçmektedir.
• Dört harici doğrulama kıyaslamasının üçünde PRM800K ile eğitilmiş doğrulayıcıyı geride bırakmaktadır.
• LeanPRM ile yapılan eğitim; LeanPRM-Bench, Hard2Verify ve IMO-GradingBench kıyaslamalarında 0,6B ile 8B parametre arasındaki her boyuttaki doğrulayıcıyı geliştirmektedir.

Yazılım Geliştirme ve Öğrenme Açısından Pratik Çıkarımlar#

İleri akıl yürütme ve doğrulama sistemleri geliştiren mühendisler için bu çalışma önemli mimari dersler sunmaktadır:

• Derleyici ve Biçimsel Araç Destekli Sentetik Veri: İnsan etiketlemesinin darboğaz olduğu karmaşık akıl yürütme görevlerinde, deterministik doğrulayıcılar (Lean gibi) otomatik süreç ödül modelleri (PRM) üretmek için güçlü bir temel sağlar.
• Sözdizimi ve Mantık Hatalarını Ayrıştırma: Otomatik doğrulama boru hatlarında, biçimsel araçlardan dönen derleme veya sözdizimi hatalarını ikinci bir filtreleme modeliyle ayıklamak, eğitim verisinin yalnızca gerçek mantıksal hatalara odaklanmasını sağlar.
• Küçük Modellerle Ölçeklenebilir Denetim: Doğru süreç etiketleriyle eğitilen 0,6B - 8B aralığındaki küçük ve orta ölçekli modeller, üretim ortamında best-of-N örneklemesi ve LLM-as-a-Judge kurgularında maliyet etkin ve yüksek doğruluklu filtreler olarak konumlandırılabilir. Etiketler insan müdahalesi gerektirmediği için sistem, biçimsel ifadelerin arzıyla birlikte ölçeklenerek insanların kontrol etmesi zor olan yapay zeka çıktılarında adım düzeyinde geri bildirim yolu açar.

---

Bu konuyu derinlemesine öğrenmek isterseniz: İleri Akıl Yürütme Teknikleri modülüne göz atın.