ProofOfThought: Z3 theorem proving का उपयोग करने वाला LLM-आधारित reasoning

• ProofOfThought large language model (LLM) और Z3 theorem prover को जोड़कर शक्तिशाली और व्याख्येय reasoning को सक्षम बनाता है
• यह प्रोजेक्ट natural language queries के लिए सटीक और भरोसेमंद reasoning परिणाम प्रदान करता है
• high-level Python API के माध्यम से डेवलपर्स जटिल reasoning tasks को आसानी से implement और experiment कर सकते हैं
• Z3DSL के जरिए JSON-आधारित low-level DSL access भी मिलता है, जिससे flexible customization संभव है
• Sys2Reasoning Workshop NeurIPS 2024 में प्रकाशित होकर यह नवीनतम research outcomes के practical उपयोग के फायदे दिखाता है

---

ProofOfThought ओपन सोर्स प्रोजेक्ट का परिचय

ProofOfThought एक ओपन सोर्स reasoning library है, जो large language model (LLM) और Z3 theorem prover को मिलाकर neuro-symbolic (neural-symbolic) program synthesis approach अपनाती है। यह वास्तविक दुनिया की जटिल समस्याओं के लिए मजबूत और व्याख्येय reasoning परिणाम प्रदान करती है, और यही बात इसे practical उपयोग और research दोनों दृष्टियों से महत्वपूर्ण बनाती है।

ओपन सोर्स होने के कारण कोई भी इसे research, services और development आदि में स्वतंत्र रूप से उपयोग कर सकता है। पारंपरिक सरल LLM-आधारित reasoning systems की तुलना में इसका बड़ा लाभ यह है कि reasoning process का verification और error interpretation आसान होता है। अन्य reasoning systems की तुलना में natural language input → logical program में automatic conversion → Z3-आधारित reasoning जैसी structural transparency इसकी प्रमुख विशेषता है।

सिस्टम आर्किटेक्चर और मुख्य घटक

• high-level API (z3dsl.reasoning) :

  • natural language-आधारित reasoning queries चलाना
  • शुरुआती उपयोगकर्ताओं के लिए भी आसानी से अपनाई जा सकने वाली Python interface उपलब्ध कराना

• low-level DSL (z3dsl) :

  • JSON-आधारित Z3 theorem prover access उपलब्ध
  • जटिल customization और automation pipelines बनाने के लिए उपयोगी

मुख्य फीचर्स के उदाहरण

• LLM input query को logical expression (symbolic program) में बदलता है

• Z3 prover के जरिए true/false (yes/no) या condition-आधारित interpretation result तैयार किया जाता है

• उदाहरण:

  • query: "Will Nancy Pelosi publicly denounce abortion?"
  • result: False (नहीं)

• evaluation pipeline (EvaluationPipeline) उपलब्ध:

  • बड़े datasets पर batch evaluation संभव
  • accuracy आदि की automatic reporting

उपयोग और application cases

• research उद्देश्यों के लिए reasoning benchmark automation
• LLM-आधारित knowledge graph या higher-order logic problems के automatic proving services
• जटिल policy queries, natural language debates की automatic classification जैसी विभिन्न AI services में उपयोग की संभावना

शोधगत महत्व और विशेषताएँ

• NeurIPS 2024 के Sys2Reasoning workshop में प्रस्तुत
• मौजूदा LLM सीमाओं (reasoning uncertainty) को पूरक करने वाली symbolic interpretation-आधारित reliability
• reasoning results और उनके आधार की transparency तथा interpretability, वास्तविक services development में बड़ी ताकत

निष्कर्ष

ProofOfThought, LLM और Z3 theorem prover की खूबियों को मिलाकर मजबूत और व्याख्येय AI reasoning infrastructure बनाना चाहने वाले डेवलपर्स और शोधकर्ताओं को वास्तविक मूल्य प्रदान करता है। प्रोजेक्ट का license और structure open source ecosystem के अनुरूप डिज़ाइन किया गया है, इसलिए यह academic research और industrial उपयोग दोनों के लिए आकर्षक है।

[GN⁺]

Hacker News राय

• Gemini 2.5 Pro के साथ एक दिलचस्प अनुभव साझा किया गया। एक ऑनलाइन CAS सिस्टम में simultaneous equations हल करने की कोशिश के दौरान CAS अपेक्षा के अनुसार काम नहीं कर रहा था, इसलिए Gemini से मदद मांगी गई, और Gemini ने सीधे समाधान दे दिया। उसने बताया कि उसने Python के sympy पैकेज का उपयोग किया। इस बात से यह प्रभाव मिला कि अस्पष्ट LLM और सख्त tools का संयोजन शक्तिशाली असर दे सकता है
  • यह इंसानों जैसा ही लगता है। हम जटिल गणनाओं में कमजोर होते हैं, लेकिन शानदार कंप्यूटर बनाते हैं जो यह काम अच्छी तरह करते हैं। और फिर बहुत मेहनत के बाद हमने ऐसे प्रोग्राम भी बना लिए जो संख्या-आधारित गणना पर टिके रहते हुए किसी तरह text prediction कर लेते हैं, लेकिन कठिन गणनाओं में अनाड़ी रहते हैं। आखिरकार यह प्रोग्राम उन प्रोग्रामों को बनाना और इस्तेमाल करना predict करने लगते हैं जो संख्या-गणना में मजबूत होते हैं
  • गणित के लिए LLM और sympy का संयोजन मुझे सच में बहुत पसंद है। अगर LLM से sympy code लिखवाया जाए, तो यह भरोसा किया जा सकता है कि symbolic operations सही हुई हैं। code खुद output के रूप में बचा रहता है, जिसे इंसान हो या LLM, धीरे-धीरे edit और improve कर सकते हैं, और git history वगैरह से manage भी किया जा सकता है। tests और verification पास करके mathematical correctness पर भरोसा बनाए रखा जा सकता है। मैं sympy code से आसानी से latex में बदलने वाले helper functions भी इस्तेमाल करता हूँ। हाल में quantum eraser experiment से जुड़े गणितीय काम भी मैंने इसी तरह किए। github लिंक
  • tools के साथ LLM के जरिए problem-solving process को follow करना एक ठीक तरीका हो सकता है, यह समझ में आता है। वास्तव में यह उम्मीद से बेहतर काम करता है। लेकिन CAS का इस्तेमाल न करके LLM से गणित करवाने की कोशिश करना ऐसा है जैसे apartment shift करने के लिए freight truck की जगह bus से कई चक्कर लगाए जाएँ। सिर्फ इसलिए कि आपके पास पहले से bus pass है
• इस बात पर जोर दिया गया कि LLM आखिरकार statistical language models ही हैं। logic programs, खासकर Prolog source code, generate करना अनुभव के अनुसार उम्मीद से बेहतर काम करता है। शायद इसलिए कि Prolog को symbolic natural language processing में अपनाया गया था, और training datasets में translation samples भी भरपूर हैं। Z3 में SMTLib syntax की जगह Datalog syntax आज़माने पर भी विचार किया जा सकता है। संबंधित demo और Z3 Datalog syntax देखने की सिफारिश की गई
  • Z3 में Datalog syntax काफ़ी शानदार है। हमने grammars पेपर में SMT का इस्तेमाल किया था, क्योंकि कई solvers के साथ compatibility सबसे ज्यादा थी। लेकिन NeurIPS review process के दौरान हमने यह भी test किया कि वही तरीका PROLOG में भी अच्छी तरह काम करता है। उम्मीद है कि यह Datalog में भी चलेगा। पेपर लिंक, datalog उदाहरण
• यह एक दिलचस्प approach लगती है। हमारी टीम ने भी इसी तरह LEAN के साथ business operations policies को encode करने वाला एक prototype बनाया था। internal wiki या Google Docs की knowledge base को LLM पहले LEAN code में convert करता था। फिर consistency verification के लिए solver चलाया जाता था। wiki में बदलाव होते ही पूरा process फिर से चल पड़ता था, और एक तरह से process linter का काम करता था। हालांकि LEAN conversion में ही engineer review की जरूरत पड़ती थी, इसलिए यह prototype stage से आगे नहीं बढ़ा। फिर भी legal और financial compliance वाले domains में यह promising तरीका है
  • automatic formalization की दीवार सच में बहुत ऊँची है। हमारे NeurIPS 2025 paper में हमने well-defined grammar को target करके automatic formalization की uncertainty को quantify करके analyze किया था। पेपर लिंक यदि विस्तृत चर्चा चाहिए तो कभी भी संपर्क करें
  • जो लोग LEAN क्या है, यह जानना चाहते हैं, उनके लिए परिचय: यह Microsoft का Lean Theorem Prover है। प्रोजेक्ट लिंक
  • वास्तविक उदाहरण जानने की उत्सुकता है। ऐसी कौन-सी policies हैं जिन्हें वास्तविक दुनिया में LEAN में define करने लायक पर्याप्त precision के साथ लिखा जाता है, इसका उदाहरण सुनना चाहूँगा
  • इस तरह का तरीका विरोधाभासी guidelines की व्यवस्थित पहचान करने में बहुत उपयोगी हो सकता है
• यह बहुत दिलचस्प research area है। कुछ साल पहले मैंने logic और probability-आधारित reasoning engines का उपयोग करके verify किया था कि premises से conclusions सही तरह निकलते हैं या नहीं। साथ ही agents का उपयोग करके domain knowledge को synthesize, formalize और criticize भी कराया था। यह कोई silver bullet नहीं है, लेकिन इससे एक हद तक accuracy सुनिश्चित की जा सकती थी। मुझे लगता है कि कुछ स्तर की symbolic reasoning और agent-as-a-judge की अवधारणा भविष्य में promising हो सकती है। संदर्भ पेपर
  • मैंने वह research पढ़ी है। काफ़ी शानदार है। हाल में AWS ARChecks में autoformalization agent बनाने का अनुभव भी रहा है। यह अभी public नहीं है, लेकिन एक आम तौर पर उपलब्ध product मौजूद है, इसलिए वह देखना उपयोगी हो सकता है AWS ब्लॉग
  • Agent/LLM को judge की तरह इस्तेमाल करना biased होता है, और मेरी नज़र में यह सिर्फ bootstrapping के लिए उपयुक्त है। जब performance काफी बढ़ जाएगी, तो LLM judge खुद एक artificial bottleneck बन जाएगा, इसलिए अंततः expert human judges या deterministic oracle की ओर जाना पड़ेगा
• यह उल्लेख किया गया कि RHEL का knife-edge rolling kernel proof of concept में इस्तेमाल हुआ
• ऐसा लगा कि repository में विस्तृत explanation की कमी है, हालांकि यह संभव है क्योंकि यह paper के supplementary artifact की भूमिका निभा रही हो। मूल रूप से यह ऐसा API लगता है जो LLM से Z3 programs generate करवाने की कोशिश करता है। यह real-world queries को logical रूप में व्यक्त करने के लिए प्रेरित करता है, ताकि facts, inference rules, और goals सभी शामिल हो सकें। supervision का काम यह है कि logic specification को सीधे पढ़ा जा सके, solver चलाया जा सके, और true/false की जाँच की जा सके। संदेह की बात यह है: SMT rules को कौन एक-एक करके पढ़कर वास्तविक दृष्टिकोण से मिलाएगा, constants को कौन verify करेगा, और क्या LLM गलती से या goal हासिल करने के लिए logical या real-world sense से हटे हुए rules नहीं जोड़ देगा? पेपर में logic benchmark पर 51% false positive दर्ज किया गया, जो चौंकाने वाला काफी ऊँचा आँकड़ा है, और इसका अर्थ यह निकाला गया कि LLM logical modeling में कमजोर है या incomplete rules generate करता है। evaluation कमजोर लगती है, इसलिए यह स्पष्ट नहीं हो पाता कि ऐसा क्यों हुआ
  • यह दावा किया गया कि यह paper पिछले साल GPT-4o के साथ लिखा गया था, और नवीनतम models में स्थिति काफी बेहतर हो गई है। उदाहरण के लिए हाल का पेपर के Tab 1 में text-based और SMT-based performance की तुलना की गई है। o3-mini text reasoning और SMT के परिणामों को अच्छी तरह align करता है। commercial product AWS Automated Reasoning Checks में domain model बनाया जाता है, उसे verify किया जाता है, और answer generation चरण में LLM के Q/A pairs को policies के अनुरूप होने के लिए सख्त solver verification से गुजारा जाता है। इसके जरिए policy-संबंधित validity को 99% से अधिक सुनिश्चित किया जा सकता है, यह बात रेखांकित की गई AWS ब्लॉग
• एक सवाल पूछा गया कि क्या मेरी व्याख्या सही है। यदि LLM का probabilistic output logic model में जाता है, तो क्या यह आखिरकार “garbage in, garbage out” ही नहीं है?
  • formal logic एक filter की तरह काम करता है। यानी “garbage in, filtered garbage out”। इसकी तुलना evolution से की गई, जहाँ random “garbage” mutations को natural environment filter कर देता है
  • यह कहा गया कि हमेशा “garbage” नहीं निकलता। यह काफी बार useful output देता है, इसलिए इसका महत्व है
  • यह एक subjective judgment है। आखिर पिछले हजारों सालों में इंसानों ने जो कुछ बनाया है, उसे भी garbage कहा जा सकता है। अगर बात बढ़ाई जाए, तो गुफाओं में जीना शायद ज्यादा simple रहा होगा
• यह बात बहुत रोचक है कि AI सिर्फ सोचता ही नहीं, बल्कि एक verifiable diary भी छोड़ता है। यह ऐसा है मानो कोई दार्शनिक cryptographic notary के साथ जीवन जी रहा हो। सच में अद्भुत काम है
• मुख्य विचार यह है कि LLM reasoning process का structured, JSON DSL में प्रारूप तैयार करता है, जिसे बाद में deterministically first-order logic में बदला जाता है और Z3 theorem proving की कोशिश की जाती है। इसलिए final output में या तो provable conclusion मिलता है या counterexample, और इसीलिए यह सिर्फ भरोसेमंद लगने वाली text chain से अलग है
• यह दिलचस्प research है। DSL examples देखने के लिए repo देखा, लेकिन कोई साफ example ढूँढना कठिन था। अच्छा होता अगर README में example code snippets होते
  • रुचि के लिए धन्यवाद, उन्हें जल्द जोड़ा जाएगा। फिलहाल paper के पेज 11 से कई scenarios का विवरण है पेपर PDF