Case study: proving sqrt(2) irrational with LPTP and an LLM

कल्पना कीजिए कि आप एक जासूस हैं जो एक ऐसे रहस्य को सुलझाने की कोशिश कर रहे हैं जिसने दो हज़ार वर्षों से मनुष्यों को चकित कर रखा है: क्या 2 का वर्गमूल (square root) एक "परिमेय" (rational) संख्या है? गणित की दुनिया में, एक परिमेय संख्या एक आदर्श भिन्न (fraction) की तरह होती है, जैसे पाई का एक साफ टुकड़ा (जैसे 3/4 या 5/2)। एक अपरिमेय (irrational) संख्या एक बिखरी हुई, कभी न खत्म होने वाली दशमलव संख्या होती है जिसे कभी भी एक सरल भिन्न के रूप में नहीं लिखा जा सकता। 2 का वर्गमूल 1 लंबाई वाले किनारों वाले एक वर्ग के विकर्ण (diagonal) की लंबाई है, और प्राचीन गणितज्ञों ने सिद्ध किया है कि यह बिखरा हुआ है—इसे भिन्न के रूप में नहीं लिखा जा सकता।

अब, कल्पना कीजिए कि आपके पास इस रहस्य को सुलझाने के लिए दो बहुत अलग उपकरण हैं। पहला एक अत्यंत सख्त, रोबोटिक रेफरी है जिसे LPTP कहा जाता है। यह एक बहुत ही सटीक, तार्किक भाषा बोलता है (जो प्रोलॉग (Prolog) पर आधारित है) और यह केवल तभी एक प्रमाण स्वीकार करेगा जब उसका हर एक चरण गणितीय रूप से पूर्ण हो। यदि आप एक छोटी सी भी गलती करते हैं, तो यह हथौड़ा मारकर कहता है, "नहीं, अमान्य।" दूसरा उपकरण एक लार्ज लैंग्वेज मॉडल (LLM) है, जो एक अत्यंत बुद्धिमान, रचनात्मक छात्र की तरह है जिसने लगभग सब कुछ पढ़ा है। यह छात्र अगला कदम या किसी कहानी के अगले हिस्से का अनुमान लगाने में बहुत अच्छा है, लेकिन कभी-कभी यह "भ्रम" (hallucinate) भी करता है, यानी ऐसी बातें बना देता है जो सुनने में तो सही लगती हैं लेकिन वास्तव में गलत होती हैं।

बड़ा सवाल आज के वैज्ञानिकों के सामने यह है: क्या हम इन दोनों को एक टीम के रूप में जोड़ सकते हैं? क्या हम इस रचनात्मक छात्र को प्रमाण लिखने का भारी काम करने दे सकते हैं, जबकि सख्त रेफरी यह सुनिश्चित करने के लिए हर वाक्य की जांच करे कि छात्र झूठ तो नहीं बोल रहा है? यह शोध पत्र ठीक इसी साझेदारी की खोज करता है, जिसमें 2 के वर्गमूल के प्राचीन रहस्य को एक परीक्षण मामले के रूप में उपयोग किया गया है।

---

महान प्रमाण-जांच टीम-अप (The Great Proof-Checking Team-Up)

इस शोध पत्र में, लेखकों ने यह देखने का प्रयास किया कि क्या वे एक आधुनिक AI (विशेष रूप से, 'क्लॉड' (Claude) नामक एक मॉडल) का उपयोग यह सिद्ध करने के लिए कर सकते हैं कि 2 का वर्गमूल अपरिमेय है, लेकिन एक मोड़ के साथ: प्रमाण को एक बहुत ही विशिष्ट, सख्त प्रारूप में लिखा जाना था जिसे रोबोटिक रेफरी (LPTP) समझ सके और सत्यापित कर सके। वे केवल यह नहीं चाहते थे कि AI यह कहे कि "यह सत्य है"; वे चाहते थे कि AI वास्तविक चरण-दर-चरण तर्क लिखे, जिसे रेफरी फिर से ग्रेड करे।

कहानी एक सरल विचार के साथ शुरू होती है। 2 के वर्गमूल के अपरिमेय होने को सिद्ध करने के लिए, आप आमतौर पर इसके विपरीत मान लेते हैं: कि यह दो पूर्ण संख्याओं, $p$ और $q$ से बना एक भिन्न है, जो आपस में कोई सामान्य गुणनखंड साझा नहीं करते हैं (वे "सह-अभाज्य" या coprime हैं)। यदि आप गणित करते हैं, तो आप अंततः एक विरोधाभास (contradiction) तक पहुँच जाते हैं जहाँ दोनों संख्याएँ सम (even) होनी चाहिए, जिसका अर्थ है कि वे एक गुणनखंड (2) साझा करती हैं। यह उस नियम को तोड़ देता है कि वे सह-अभाज्य थे, जिससे मूल धारणा गलत साबित होती है।

लेखकों ने AI को LPTP की सख्त भाषा में यह प्रमाण लिखने के लिए प्रेरित करने की कोशिश की। शुरुआत में, AI एक ऐसे छात्र की तरह था जो कहानी तो जानता है लेकिन उसे आवश्यक प्रारूप में निबंध नहीं लिख पाता। वह चरणों को छोड़ने या तार्किक छलांग लगाने की कोशिश करता था जिन्हें रेफरी स्वीकार नहीं करता।

यहीं पर टीम वर्क हुआ। लेखकों ने एक फीडबैक लूप बनाया:

1. AI एक प्रमाण चरण लिखने का प्रयास करता है।
2. रेफरी (LPTP) इसकी जाँच करता है।
3. यदि रेफरी को कोई गलती मिलती है, तो वह ठीक उस पंक्ति की ओर इशारा करता है जहाँ तर्क टूटा है।
4. लेखक उस त्रुटि को AI को दिखाते हैं।
5. AI उस विशिष्ट त्रुटि को सुधारते हुए फिर से प्रयास करता है।

यह प्रक्रिया "गर्म और ठंडा" (hot and cold) के खेल की तरह थी। रेफरी केवल यह नहीं कहता था कि "गलत है"; वह कहता था, "आपने चरण 4 में गलती की है," जिससे AI को अपना रास्ता सुधारने का मौका मिला।

परिणाम: एक आंशिक विजय

प्रयोग सफल रहा, लेकिन इसमें कुछ सीमाएँ थीं। AI अपने आप पहेली के कई छोटे, आसान हिस्सों को सिद्ध करने में सक्षम था। उदाहरण के लिए, इसने सफलतापूर्वक सिद्ध किया कि "यदि कोई संख्या सम है, तो उसका वर्ग भी सम है" या "2 गुना एक संख्या सम होती है।" लेखक इन्हें "लेम्मा" (lemppas - छोटे सहायक प्रमाण) कहते हैं। इसने इन्हें सही ढंग से सिद्ध किया, और कभी-कभी नए सहायक विचार भी प्रस्तुत किए जो मनुष्यों के दिमाग में नहीं आए थे।

हालाँकि, प्रमाण के सबसे कठिन हिस्से के लिए—वह विशिष्ट तर्क जो यह दिखाता है कि 2 का वर्गमूल एक भिन्न क्यों नहीं हो सकता—AI अटक गया। वह अपने आप सही रास्ता नहीं खोज सका। इसलिए, मानव लेखकों को हस्तक्षेप करना पड़ा और AI को एक "संकेत" देना पड़ा या स्वयं प्रमाण की मुख्य संरचना लिखनी पड़ी, और फिर AI से छोटे अंतराल भरने के लिए कहा।

अंत में, उन्होंने 2 के अपरिमेय होने का एक पूर्ण, औपचारिक प्रमाण तैयार किया। यह प्रमाण आंशिक रूप से AI द्वारा लिखा गया था और पूरी तरह से रोबोटिक रेफरी द्वारा जांचा गया था। रेफरी ने इसे उत्तीर्ण ग्रेड दिया, जिससे पुष्टि हुई कि तर्क सुसंगत था।

इसका क्या अर्थ है

यह शोध पत्र यह दावा नहीं करता कि AI अब अपने आप सभी गणितीय समस्याओं को हल कर सकता है। वास्तव में, लेखक स्पष्ट रूप से दिखाते हैं कि AI इसे अकेले नहीं कर सकता; मानव मार्गदर्शन और सख्त जाँच के बिना, AI संभवतः एक फर्जी या त्रुटिपूर्ण प्रमाण प्रस्तुत कर देता।

इसके बजाय, यह शोध पत्र काम करने का एक नया तरीका सुझाता है: AI एक ड्राफ्ट लेखक के रूप में, मनुष्य संपादकों के रूप में, और औपचारिक उपकरण तथ्य-जांचकर्ताओं के रूप में। AI तेज़ और रचनात्मक है, जो विचार उत्पन्न करता है और विवरण भरता है, जबकि औपचारिक उपकरण (LPTP) एक बिना पलक झपकाए देखने वाली आँख की तरह कार्य करता है जो भ्रम और त्रुटियों को पकड़ लेता है।

लेखकों ने अन्य स्वचालित गणितीय उपकरणों (जिन्हें ATP कहा जाता है) का भी परीक्षण किया कि क्या वे यह काम तेज़ी से कर सकते हैं। ये उपकरण तेज़ और मुफ्त थे, लेकिन उन्होंने ऐसे प्रमाण प्रस्तुत किए जिन्हें पढ़ना मनुष्यों के लिए कठिन था और जिन्हें सत्यापित गणित की लाइब्रेरी में आसानी से जोड़ा नहीं जा सकता था। AI दृष्टिकोण, हालांकि धीमा था और इसमें मानवीय सहायता की आवश्यकता थी, ऐसे प्रमाण उत्पन्न करता था जो पठनीय थे और जिन्हें भविष्य के उपयोग के लिए सुरक्षित रूप से संग्रहीत किया जा सकता था।

संक्षेप में, यह शोध पत्र दिखाता है कि हमें मानव अंतर्ज्ञान और मशीन की सटीकता के बीच किसी एक को चुनने की आवश्यकता नहीं है। AI को भारी काम (ड्राफ्टिंग) करने देने और सख्त उपकरणों को ग्रेडिंग करने देकर, हम एक ऐसी प्रणाली बना सकते हैं जहाँ AI हमें जटिल गणितीय सत्यों को सिद्ध करने में मदद करता है, बशर्ते हम जहाज को चलाने के लिए एक मानव को और मानचित्र की जाँच के लिए एक सख्त रेफरी को बनाए रखें। 2 का वर्गमूल अपरिमेय ही रहता है, लेकिन अब हमारे पास इसे सिद्ध करने का एक नया, सहयोगात्मक तरीका है।