ProofOfThought: Penalaran berbasis LLM dengan pembuktian teorema Z3

• ProofOfThought menggabungkan large language model (LLM) dan pembukti teorema Z3 untuk mendukung penalaran yang kuat dan dapat diinterpretasikan
• Proyek ini memberikan hasil penalaran yang akurat dan andal untuk kueri bahasa alami
• Melalui API Python tingkat tinggi, pengembang dapat dengan mudah mengimplementasikan dan bereksperimen dengan tugas penalaran yang kompleks
• Melalui Z3DSL, tersedia juga akses DSL tingkat rendah berbasis JSON sehingga memungkinkan kustomisasi yang fleksibel
• Publikasi di Sys2Reasoning Workshop NeurIPS 2024 menunjukkan manfaat praktis dari penerapan hasil riset terbaru

---

Pengenalan proyek open source ProofOfThought

ProofOfThought adalah pustaka penalaran open source yang mengadopsi pendekatan sintesis program neurosimbolik (neural-symbolic) yang menggabungkan large language model (LLM) dan pembukti teorema Z3. Kemampuannya untuk memberikan hasil penalaran yang tangguh dan dapat diinterpretasikan terhadap masalah kompleks di dunia nyata memiliki makna penting baik untuk penggunaan praktis maupun penelitian.

Karena bersifat open source, siapa pun bebas memanfaatkannya untuk riset, layanan, maupun pengembangan. Dibandingkan sistem penalaran berbasis LLM yang sederhana, keunggulannya adalah proses penalaran lebih mudah diverifikasi dan kesalahan lebih mudah diinterpretasikan. Ciri pembeda utamanya dibanding sistem penalaran lain adalah transparansi struktural berupa alur input bahasa alami → konversi otomatis ke program logika → penalaran berbasis Z3.

Arsitektur sistem dan komponen utama

• API tingkat tinggi (z3dsl.reasoning) :

  • Menjalankan kueri penalaran berbasis bahasa alami
  • Menyediakan antarmuka Python yang mudah digunakan bahkan oleh pemula

• DSL tingkat rendah (z3dsl) :

  • Memungkinkan akses ke pembukti teorema Z3 berbasis JSON
  • Menguntungkan untuk kustomisasi kompleks dan pembangunan pipeline otomatis

Contoh fitur utama

• LLM mengubah kueri yang diberikan menjadi formula logika (program simbolik)

• Melalui pembukti Z3, menghasilkan hasil interpretasi benar/salah (yes/no) atau berbasis kondisi

• Contoh:

  • Kueri: "Apakah Nancy Pelosi akan secara terbuka mengecam aborsi?"
  • Hasil: False (tidak)

• Menyediakan pipeline evaluasi (EvaluationPipeline):

  • Mendukung evaluasi batch untuk dataset dalam jumlah besar
  • Pelaporan otomatis seperti akurasi

Penerapan dan contoh penggunaan

• Otomatisasi benchmark penalaran untuk tujuan riset
• Layanan pembuktian otomatis untuk knowledge graph berbasis LLM atau masalah logika tingkat tinggi
• Berpotensi diterapkan pada berbagai layanan AI seperti kueri kebijakan yang kompleks dan penentuan otomatis atas debat bahasa alami

Signifikansi dan karakteristik riset

• Dipresentasikan di workshop Sys2Reasoning pada NeurIPS 2024
• Keandalan berbasis interpretasi simbolik yang melengkapi keterbatasan LLM yang ada (ketidakpastian penalaran)
• Transparansi hasil penalaran dan dasar pembuktiannya menjadi keunggulan besar dalam pengembangan layanan nyata

Kesimpulan

ProofOfThought menggabungkan keunggulan LLM dan pembukti teorema Z3 untuk memberikan nilai nyata bagi pengembang dan peneliti yang ingin membangun infrastruktur penalaran AI yang tangguh dan dapat diinterpretasikan. Lisensi dan strukturnya dirancang agar sesuai dengan ekosistem open source, sehingga menarik baik untuk penelitian akademik maupun pemanfaatan industri.

[GN⁺]

Komentar Hacker News

• Menceritakan pengalaman menarik dengan Gemini 2.5 Pro. Saat mencoba menyelesaikan sistem persamaan di sistem CAS online dan CAS tidak bekerja seperti yang diharapkan, ia meminta bantuan Gemini, lalu Gemini langsung memberikan solusinya. Gemini menjelaskan bahwa ia menggunakan paket sympy Python. Ia membagikan kesan bahwa gabungan antara LLM yang ambigu dan alat yang ketat bisa menghasilkan efek yang kuat
  • Rasanya mirip manusia. Kita lemah dalam perhitungan rumit, tetapi kita membuat komputer hebat untuk melakukannya dengan baik. Lalu, setelah upaya besar, kita juga membuat program yang berdasarkan perhitungan angka bisa cukup lumayan dalam prediksi teks, tetapi buruk dalam perhitungan sulit. Pada akhirnya program ini menjadi mampu memprediksi cara membuat dan menggunakan program lain yang kuat dalam perhitungan angka
  • Sangat menyukai kombinasi LLM dan sympy untuk matematika. Jika menyuruh LLM menulis kode sympy, kita bisa percaya bahwa operasi simboliknya dilakukan dengan benar. Kodenya sendiri tetap menjadi artefak hasil yang bisa diperbaiki dan ditingkatkan secara bertahap, baik oleh manusia maupun LLM, serta dapat dikelola dengan riwayat git dan sejenisnya. Kepercayaan terhadap ketepatan matematis dipertahankan lewat lolosnya pengujian dan verifikasi. Ia juga menggunakan fungsi helper yang dengan mudah mengubah kode sympy menjadi latex. Baru-baru ini ia juga mengerjakan matematika terkait eksperimen quantum eraser dengan cara ini. tautan github
  • Memahami bahwa mengikuti proses pemecahan masalah bersama LLM dengan bantuan alat adalah pendekatan yang masuk akal. Dalam praktiknya, ini bekerja lebih baik dari yang diharapkan. Namun, tidak memakai CAS dan malah mendorong LLM untuk mengerjakan matematika diibaratkan seperti pindahan apartemen dengan naik bus bolak-balik berkali-kali alih-alih memakai truk barang. Menurutnya itu terjadi hanya karena sudah terlanjur punya bus pass
• Menekankan bahwa LLM pada akhirnya adalah model bahasa statistik. Dari pengalamannya, menghasilkan program logika, khususnya source code Prolog, bekerja jauh lebih baik dari perkiraan. Mungkin karena Prolog pernah diperkenalkan ke pemrosesan bahasa alami simbolik dan ada banyak sampel translasi di dataset pelatihan. Layak juga mempertimbangkan memakai sintaks Datalog milik Z3 alih-alih sintaks SMTLib. Ia merekomendasikan untuk melihat demo terkait dan sintaks Datalog Z3
  • Di Z3, sintaks Datalog cukup bagus. Kami memakai SMT dalam makalah grammars karena kompatibilitasnya paling tinggi dengan berbagai solver. Namun selama proses review NeurIPS, kami menguji bahwa pendekatan itu juga bekerja baik dengan PROLOG. Kemungkinan besar juga akan bekerja dengan Datalog. tautan makalah, contoh datalog
• Menganggap ini pendekatan yang menarik. Tim mereka juga pernah membuat prototipe yang mirip, yaitu meng-encode kebijakan operasional bisnis dengan LEAN. Basis pengetahuan dari wiki internal atau Google Docs terlebih dulu diubah LLM menjadi kode LEAN. Lalu solver dijalankan untuk memeriksa konsistensi. Jika wiki diubah, seluruh proses dijalankan ulang sehingga berfungsi seperti semacam linter proses. Namun, karena transformasi ke LEAN itu sendiri masih perlu ditinjau engineer, proyeknya berhenti di tahap prototipe. Meski begitu, ini terlihat menjanjikan untuk domain yang menuntut kepatuhan hukum dan finansial
  • Menyebut bahwa hambatan autoformalization memang sangat tinggi. Ia membagikan pengalaman dari makalah NeurIPS 2025 mereka yang menganalisis dan mengukur ketidakpastian autoformalization terhadap grammar yang didefinisikan dengan baik. tautan makalah Jika ingin diskusi lebih lanjut, silakan hubungi kapan saja
  • Untuk yang penasaran apa itu LEAN, diperkenalkan sebagai Lean Theorem Prover buatan Microsoft. tautan proyek
  • Penasaran dengan contoh nyata. Ingin mendengar contoh kebijakan seperti apa yang di dunia nyata ditulis cukup presisi hingga layak didefinisikan dengan LEAN
  • Tampaknya sangat berguna karena pendekatan seperti ini dapat membantu mengidentifikasi pedoman yang saling bertentangan secara sistematis
• Ini bidang riset yang sangat menarik. Beberapa tahun lalu ia pernah memakai mesin penalaran berbasis logika dan probabilitas untuk memverifikasi apakah premis benar-benar mengarah ke kesimpulan. Ia juga memakai agent untuk menyintesis, memformalkan, dan mengkritik pengetahuan domain. Ini bukan peluru perak, tetapi bisa menjamin tingkat akurasi tertentu. Menurutnya, tingkat simbolisme tertentu dan konsep agent-as-a-judge menjanjikan untuk masa depan. makalah referensi
  • Saya sudah membaca riset itu. Cukup keren. Saya juga baru-baru ini membuat agen autoformalization di AWS ARChecks. Belum dipublikasikan, tetapi ada produk yang tersedia secara umum jadi mungkin relevan untuk dilihat blog AWS
  • Menggunakan Agent/LLM sebagai hakim tetap mengandung bias, dan menurutnya hanya cocok untuk bootstrap. Jika performanya cukup tinggi, hakim LLM justru akan menjadi batas buatan, sehingga pada akhirnya harus beralih ke hakim manusia ahli atau oracle deterministik
• Menyebut bahwa kernel rolling knife-edge dari RHEL digunakan dalam proof of concept
• Merasa penjelasan detail di repositori masih kurang, meski mungkin karena ini berfungsi sebagai artefak pendamping makalah. Pada dasarnya ini tampak seperti API yang mencoba membuat LLM menghasilkan program Z3. Tujuannya agar kueri dunia nyata dapat diekspresikan secara logis, memuat fakta, aturan inferensi, dan tujuan sekaligus. Fungsi pengawasannya adalah memungkinkan sistem membaca pernyataan logika secara langsung dan menjalankan solver untuk memeriksa benar/salah. Hal yang diragukan adalah: siapa yang akan membaca aturan SMT satu per satu dan membandingkannya dengan sudut pandang dunia nyata, siapa yang memverifikasi nilai konstanta, dan apakah LLM mungkin secara tidak sengaja atau demi mencapai tujuan menambahkan aturan yang secara logis atau secara nyata menyimpang. Dalam makalah itu tercatat 51% false positive pada benchmark logika, yang ditafsirkan sebagai angka sangat tinggi dan sinyal bahwa LLM lemah dalam pemodelan logika atau menghasilkan aturan yang tidak lengkap. Evaluasinya terasa lemah sehingga tidak menjelaskan dengan jelas mengapa itu terjadi
  • Diklaim bahwa makalah ini ditulis tahun lalu dengan GPT-4o, dan pada model terbaru situasinya sudah jauh membaik. Misalnya, di makalah terbaru Tab 1, performa berbasis teks dan berbasis SMT dibandingkan. o3-mini menunjukkan kecocokan yang baik antara text reasoning dan hasil pada SMT. Dalam produk komersial AWS Automated Reasoning Checks, model domain dibuat dan diverifikasi, lalu pada tahap pembuatan jawaban pasangan tanya-jawab dari LLM diperiksa ketat oleh solver apakah mematuhi kebijakan. Melalui ini, mereka menekankan bahwa validitas pasangan tanya-jawab terkait kebijakan dapat dijamin di atas 99% blog AWS
• Ini pertanyaan apakah interpretasi saya benar. Jika output probabilistik dari LLM diteruskan ke model logika, bukankah itu tetap hanya “garbage in, garbage out”? Ia mengungkapkan keraguan itu
  • Logika formal berfungsi sebagai filter. Jadi bukan “garbage in, garbage out”, melainkan “garbage in, garbage yang sudah difilter keluar”. Ia mengibaratkannya seperti evolusi, di mana mutasi acak yang “sampah” tersaring oleh lingkungan alam
  • Menurutnya, tidak selalu yang keluar itu “sampah”. Cukup sering keluar output yang berguna, dan itu sendiri sudah bermakna
  • Itu penilaian yang subjektif. Apa pun yang dibuat manusia selama ribuan tahun terakhir juga bisa dianggap sampah. Kalau mau diperdebatkan, hidup di gua mungkin justru lebih sederhana
• Sangat menarik bahwa AI bukan hanya berpikir, tetapi juga meninggalkan diary yang bisa diverifikasi. Rasanya seperti filsuf yang hidup ditemani notaris kriptografis. Pekerjaan yang benar-benar menakjubkan
• Gagasan intinya adalah LLM membuat rancangan awal proses penalaran secara terstruktur dalam JSON DSL, lalu itu diterjemahkan secara deterministik ke logika orde pertama untuk mencoba pembuktian teorema Z3. Jadi output akhirnya adalah kesimpulan yang bisa dibuktikan atau counterexample, sehingga berbeda dari rantai teks yang hanya terdengar meyakinkan
• Riset yang menarik. Saya mengecek repo karena penasaran dengan contoh DSL, tetapi sulit menemukan contoh yang jelas. Akan bagus jika ada snippet kode contoh di README
  • Terima kasih atas minatnya, akan segera ditambahkan. Sementara itu, ada penjelasan berbagai situasi mulai halaman 11 makalah PDF makalah