ProofOfThought: Z3 teorem ispatını kullanan LLM tabanlı akıl yürütme

• ProofOfThought, büyük dil modeli (LLM) ile Z3 teorem ispatlayıcısını birleştirerek güçlü ve yorumlanabilir akıl yürütmeyi destekler
• Bu proje, doğal dil sorguları için doğru ve yüksek güvenilirlikli akıl yürütme sonuçları sunar
• Yüksek seviyeli Python API sayesinde geliştiriciler karmaşık akıl yürütme görevlerini kolayca uygulayıp deneyebilir
• Z3DSL üzerinden JSON tabanlı düşük seviyeli DSL erişimi de sunularak esnek özelleştirme mümkün olur
• Sys2Reasoning Workshop NeurIPS 2024'te yayımlanması, güncel araştırma çıktılarının pratikleşme avantajını gösterir

---

ProofOfThought açık kaynak projesine giriş

ProofOfThought, büyük dil modelleri (LLM) ile Z3 teorem ispatlayıcısını birleştiren nörosembolik (sinirsel-sembolik) program sentezi yaklaşımını benimseyen açık kaynaklı bir akıl yürütme kütüphanesidir. Gerçek dünyadaki karmaşık problemler için sağlam ve yorumlanabilir akıl yürütme sonuçları sunması, hem pratik kullanım hem de araştırma açısından önemli bir anlam taşır.

Açık kaynak niteliği sayesinde herkes bunu araştırma, servis ve geliştirme gibi alanlarda serbestçe kullanabilir; mevcut basit LLM tabanlı akıl yürütme sistemlerine kıyasla akıl yürütme sürecini doğrulamak ve hataları yorumlamak daha kolaydır. Diğer akıl yürütme sistemleriyle karşılaştırıldığında, doğal dil girdisi → mantık programına otomatik dönüşüm → Z3 tabanlı akıl yürütme akışı şeklindeki yapısal şeffaflık en belirgin özelliklerinden biridir.

Sistem mimarisi ve ana bileşenler

• Yüksek seviyeli API (z3dsl.reasoning) :

  • Doğal dil tabanlı akıl yürütme sorgularını yürütme
  • Yeni başlayanların da kolayca kullanabileceği bir Python arayüzü sunma

• Düşük seviyeli DSL (z3dsl) :

  • JSON tabanlı Z3 teorem ispatlayıcısı erişimi
  • Karmaşık özelleştirmeler ve otomasyon pipeline'ları kurmak için avantajlıdır

Başlıca özellik örnekleri

• LLM, verilen sorguyu mantık ifadesine (sembolik programa) dönüştürür

• Z3 ispatlayıcısı aracılığıyla doğru/yanlış (yes/no) ya da koşul tabanlı yorumlama sonuçları üretir

• Örnek:

  • Sorgu: "Nancy Pelosi kürtajı kamuoyu önünde kınar mı?"
  • Sonuç: False (hayır)

• Değerlendirme pipeline'ı (EvaluationPipeline) sunulur:

  • Büyük veri kümeleri üzerinde toplu değerlendirme yapılabilir
  • Doğruluk gibi metrikler otomatik raporlanır

Uygulama ve kullanım örnekleri

• Araştırma amaçlı akıl yürütme benchmark'larının otomasyonu
• LLM tabanlı bilgi grafiği veya yüksek dereceli mantık problemleri için otomatik ispat servisleri
• Karmaşık politika sorguları, doğal dil tartışmalarının otomatik sınıflandırılması gibi çeşitli yapay zeka servislerine uygulanma potansiyeli

Araştırma açısından önemi ve özellikleri

• NeurIPS 2024'ün Sys2Reasoning workshop'unda sunuldu
• Mevcut LLM sınırlamalarını (akıl yürütme belirsizliği) tamamlayan sembolik yorumlama tabanlı güvenilirlik
• Akıl yürütme sonuçları ile dayanaklarının şeffaflığı ve yorumlanabilirliği, gerçek servis geliştirmede büyük bir avantajdır

Sonuç

ProofOfThought, LLM ile Z3 teorem ispatlayıcısının güçlü yanlarını birleştirerek sağlam ve yorumlanabilir yapay zeka akıl yürütme altyapısı kurmak isteyen geliştiriciler ve araştırmacılar için somut değer sunar. Projenin lisansı ve yapısı açık kaynak ekosistemine uygun biçimde tasarlandığından, hem akademik araştırma hem de endüstriyel kullanım açısından çekicidir.

[GN⁺]

Hacker News görüşleri

• Gemini 2.5 Pro ile ilginç bir deneyim yaşadığını anlatıyor. Çevrimiçi bir CAS sisteminde denklem sistemini çözmeye çalışırken CAS beklediği gibi çalışmayınca Gemini'den yardım istemiş ve Gemini çözümü doğrudan vermiş. Bunu Python'un sympy paketini kullanarak yaptığını açıklamış. Belirsiz çalışan LLM'lerle katı araçların birleşiminin güçlü bir etki yaratabileceği izlenimini paylaşıyor
  • Bu, insana benziyor. Biz karmaşık hesaplamalarda zayıfız ama bunu çok iyi yapan harika bilgisayarlar ürettik. Sonra da büyük çabalar sonunda sayı hesaplamasına dayanarak metin tahminini idare eder biçimde yapan ama zor hesaplamalarda beceriksiz kalan programlar yaptık. Sonunda bu program, sayısal hesaplamada güçlü başka programları nasıl oluşturup kullanacağını tahmin edebilir hale geldi
  • Matematikte LLM ile sympy kombinasyonunu gerçekten seviyorum. LLM'e sympy kodu yazdırırsanız, sembolik işlemlerin doğru yapıldığına güvenebilirsiniz. Kodun kendisi çıktı olarak kalır; ister insan ister LLM olsun, adım adım düzeltilip geliştirilebilir ve git geçmişi gibi araçlarla yönetilebilir. Test ve doğrulamadan geçmesi, matematiksel doğruluğa olan güveni korur. sympy kodundan kolayca latex'e dönüştüren yardımcı fonksiyonlar da kullanıyorum. Son zamanlarda quantum eraser deneyiyle ilgili matematik çalışmalarını da bu şekilde yaptım. github bağlantısı
  • Araçlarla birlikte problem çözme sürecini LLM'le adım adım izlemek makul bir yöntem gibi görünüyor. Gerçekten de beklentimin ötesinde iyi çalıştı. Ama matematiği CAS ile yapmak yerine LLM'i buna yönlendirmek, apartman taşımak için yük kamyonu yerine otobüsle defalarca gidip gelmeye benziyor. Sırf elinizde zaten otobüs kartı var diye böyle yapmak gibi
• LLM'in sonuçta istatistiksel bir dil modeli olduğunu vurguluyor. Mantık programları, özellikle Prolog kaynak kodu üretmenin beklenenden iyi çalıştığını deneyimlemiş. Muhtemelen bunun nedeni Prolog'un sembolik doğal dil işlemede kullanılmış olması ve eğitim veri kümelerinde bol miktarda çeviri örneği bulunması. Z3'ün SMTLib sözdizimi yerine Datalog sözdizimini denemek de değerlendirilebilir. İlgili demo ve Z3 Datalog sözdizimi için bakılmasını öneriyor
  • Z3'te Datalog sözdizimi oldukça iyi. Biz grammars makalesinde SMT kullandık, çünkü farklı çözücülerle en yüksek uyumluluğu sağlıyordu. Ama NeurIPS değerlendirme sürecinde aynı yaklaşımın PROLOG ile de iyi çalıştığını test ettik. Datalog ile de çalışacağını tahmin ediyorum. makale bağlantısı, datalog örneği
• Bunun ilginç bir yaklaşım olduğunu düşünüyor. Ekipleri de benzer şekilde LEAN ile iş operasyon politikalarını kodlayan bir prototip geliştirmiş. Dahili wiki veya Google Docs üzerindeki bilgi tabanı önce LLM tarafından LEAN koduna dönüştürülüyor. Ardından tutarlılık denetimi için çözücü çalıştırılıyor. Wiki değiştiğinde tüm süreç yeniden çalışıyor ve bir tür süreç linter'ı gibi davranıyor. Ancak LEAN'e dönüşümün kendisinde mühendis incelemesi gerektiği için prototip aşamasında kalmış. Yine de hukuki ve finansal uyumluluk gerektiren alanlar için umut verici bir yöntem
  • Otomatik biçimselleştirmenin önündeki engelin gerçekten çok yüksek olduğunu belirtiyor. NeurIPS 2025 makalelerinde, iyi tanımlanmış gramerleri hedef alarak otomatik biçimselleştirmenin belirsizliğini nicel olarak analiz ettiklerini paylaşıyor. makale bağlantısı Daha ayrıntılı tartışmak isteyen olursa istediği zaman ulaşabileceğini söylüyor
  • LEAN'in ne olduğunu merak edenler için açıklıyor: Microsoft tarafından geliştirilen Lean Theorem Prover. proje bağlantısı
  • Gerçek örnekleri merak ediyor. Gerçek hayatta LEAN ile tanımlanacak kadar kesin biçimde ifade edilmiş politikaların neye benzediğine dair örnekler duymak isterdim
  • Bu yaklaşımın çelişkili yönergeleri sistematik olarak tespit edebilmeyi sağlaması çok faydalı görünüyor
• Bu, çok ilginç bir araştırma alanı. Birkaç yıl önce mantık ve olasılık tabanlı çıkarım motorları kullanarak öncüllerin sonuca düzgün biçimde bağlanıp bağlanmadığını doğrulamıştım. Ayrıca agent'larla alan bilgisini sentezlemelerini, biçimselleştirmelerini ve eleştirmelerini sağladım. Sihirli değnek değil ama belli bir doğruluk düzeyi sağlayabiliyordu. Gelecekte belirli bir düzeyde sembolikliğin ve agent-as-a-judge yaklaşımının umut verici olacağını düşünüyorum. ilgili makale
  • Bu çalışmayı okudum. Oldukça etkileyici. Ben de yakın zamanda AWS ARChecks üzerinde bir autoformalization agent'ı geliştirdim. Henüz herkese açık değil ama genel kullanıma uygun ürünler de var; bakmak isteyebilirsiniz AWS blogu
  • Agent/LLM'i yargıç olarak kullanmanın önyargı taşıdığını ve yalnızca bootstrapping için uygun olduğunu düşünüyorum. Performans yeterince yükselince LLM yargıç yapay bir darboğaz haline gelir; bu yüzden sonunda uzman insan yargıçlara veya deterministik oracle'lara geçmek gerekir
• RHEL'in knife-edge rolling kernel'ının proof of concept için kullanıldığını belirtiyor
• Depoda yeterince ayrıntılı açıklama olmadığını düşündüm; muhtemelen makalenin yardımcı çıktılarından biri olduğu için böyledir. Temelde bu, LLM'e Z3 programı üretmeyi deneten bir API gibi görünüyor. Gerçek dünya sorgularını mantıksal olarak ifade etmeye yönlendirerek olguları, çıkarım kurallarını ve hedefleri birlikte yakalıyor. Denetim kısmı ise mantıksal betimlemeyi doğrudan okuyup çözücüyü çalıştırarak doğru/yanlış sonucunu kontrol etmeyi sağlıyor. Aklıma takılan noktalar şunlar: SMT kurallarını kim tek tek okuyup gerçek dünya bakış açısıyla karşılaştıracak, sabit değerleri kim doğrulayacak ve LLM yanlışlıkla ya da hedefe ulaşmak için mantıksal ya da gerçek dünyayla uyumsuz kurallar eklemeyecek mi? Makalede mantık benchmark'ında %51 false positive görülmüş; bu şaşırtıcı derecede yüksek ve LLM'in mantıksal modellemede zayıf kaldığına ya da eksik kurallar ürettiğine işaret ediyor gibi. Değerlendirme de zayıf olduğu için bunun neden yaşandığını net biçimde açıklamıyor
  • Bu makalenin geçen yıl GPT-4o ile yazıldığını, daha yeni modellerde durumun ciddi biçimde iyileştiğini savunuyor. Örneğin yakın tarihli makale içindeki Tab 1'de metin tabanlı ve SMT tabanlı performans karşılaştırılıyor. o3-mini, text reasoning ile SMT üzerindeki sonuçları iyi biçimde hizalıyor. Ticari bir ürün olan AWS Automated Reasoning Checks'te ise önce alan modeli kuruluyor ve doğrulanıyor; ardından yanıt üretim aşamasında LLM'in Soru/Cevap çiftlerinin politikaya uyup uymadığı katı bir çözücü doğrulamasından geçiriliyor. Bunun sayesinde Soru/Cevap çiftlerinin politika açısından geçerliliğinin %99'un üzerinde güvence altına alınabildiği vurgulanıyor AWS blogu
• Benim yorumum doğru mu diye soruyor. Eğer yapı, LLM'in ürettiği olasılıksal çıktıyı bir mantık modeline aktarıyorsa, bu sadece “çöp girerse çöp çıkar” demek değil mi diye kuşku duyuyor
  • Biçimsel mantık burada filtre görevi görüyor. Yani durum “çöp girerse, filtrelenmiş çöp çıkar” şeklinde. Bunu, evrimde rastgele “çöp” mutasyonların doğal çevre tarafından elenmesine benzetiyor
  • Her zaman “çöp” çıkmıyor diyor. Oldukça sık işe yarar çıktılar ürettiği için anlamlı
  • Bu öznel bir değerlendirme. Son birkaç bin yılda insanlığın ürettiklerinin tamamı da çöp sayılabilir. Hatta istenirse mağarada yaşamak daha basitti bile denebilir
• Yapay zekanın sadece düşünmekle kalmayıp doğrulanabilir bir günlük bırakması çok ilginç. Bu, sanki kriptografik bir noter eşliğinde yaşayan bir filozof gibi. Gerçekten etkileyici bir çalışma
• Temel fikir, LLM'in akıl yürütme sürecini yapılandırılmış bir JSON DSL olarak taslaklayıp bunun daha sonra deterministik biçimde birinci dereceden mantığa dönüştürülerek Z3 teorem ispatına tabi tutulması. Böylece nihai çıktı, sadece ikna edici bir metin zinciri değil, kanıtlanabilir bir sonuç ya da bir karşı örnek oluyor
• İlginç bir çalışma. DSL örneklerini merak edip depoya baktım ama açık bir örnek bulmak zordu. README'de örnek kod parçacıkları olsa iyi olurdu
  • İlginiz için teşekkürler, yakında ekleyeceğiz. Bu arada makalenin 11. sayfasından itibaren çeşitli senaryolar açıklanıyor makale PDF