Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics
यह शोध पत्र "फॉर्मल कॉन्जेक्चरस" (Formal Conjectures) को प्रस्तुत करता है, जो सक्रिय अनुसंधान से लिए गए 2,615 लीन 4 (Lean 4) औपचारिक गणितीय समस्याओं का एक गतिशील, ओपन-सोर्स बेंचमार्क है, जिसे सामुदायिक सहयोग और एआई-ऑडिटेड सत्यापन के माध्यम से डेटा अखंडता सुनिश्चित करते हुए, नए प्रमाणों की खोज में स्वचालित तर्क प्रणालियों की क्षमताओं का मूल्यांकन करने और उन्हें आगे बढ़ाने के लिए डिज़ाइन किया गया है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप एक रोबोट को उन्नत गणित (advanced mathematics) करना सिखाने की कोशिश कर रहे हैं। अतीत में, आप रोबोट को पुराने गणित के होमवर्क समस्याओं का एक ढेर दे सकते थे। लेकिन एक बड़ी समस्या है: रोबोट ने वास्तव में सोचने के बजाय इंटरनेट से केवल उत्तर रट लिए होंगे। यह उस छात्र की तरह है जिसने परीक्षा के लिए उत्तर कुंजी (answer key) रट ली है लेकिन उसे गणित की समझ नहीं है।
यह शोध पत्र इन रोबोट्स को परखने का एक नया, अधिक स्मार्ट तरीका पेश करता है। वे इसे फॉर्मल कॉन्जेक्चर (Formal Conjectures) कहते हैं।
यह कैसे काम करता है, यहाँ सरल विचारों में दिया गया है:
1. "फ्रेश मीट" टेस्ट (जीरो कंटैमिनेशन/शून्य संदूषण)
AI के लिए अधिकांश गणित परीक्षण "पुराने" होते हैं। उत्तर पहले से ही ऑनलाइन मौजूद हैं, इसलिए AI केवल उन्हें कॉपी कर सकता है।
- उपमा: एक कुकिंग प्रतियोगिता की कल्पना करें जहाँ जज शेफ को एक ऐसी रेसिपी देते हैं जिसे उन्होंने पहले कभी नहीं देखा है, और वह एक गुप्त कोड में लिखी गई है। यदि शेफ वह व्यंजन बना सकता है, तो वह वास्तव में खाना बनाना जानता है। यदि वह नहीं कर पाता, तो वह केवल अनुमान लगा रहा है।
- शोध पत्र का समाधान: लेखकों ने 1,029 अनसुलझे गणितीय प्रश्नों (conjectures) का एक पुस्तकालय बनाया है। ये वे समस्याएँ हैं जिन्हें वास्तविक मानव गणितज्ञ वर्तमान में हल करने की कोशिश कर रहे हैं। क्योंकि अभी तक किसी ने उन्हें हल नहीं किया है, इसलिए AI उत्तरों को रट नहीं सकता। यदि AI एक को हल करता है, तो यह एक वास्तविक खोज है, न कि कॉपी-पेस्ट का काम।
2. "सख्त जज" (Lean 4)
सामान्य गणित में, आप एक ऐसा प्रमाण (proof) लिख सकते हैं जो अच्छा दिखता है लेकिन उसमें एक छोटी सी तार्किक त्रुटि हो सकती है। मनुष्य इसे मिस कर सकते हैं।
- उपमा: एक वीडियो गेम की कल्पना करें जहाँ आपको एक पुल बनाना होता है। यदि आप एक कमजोर ईंट का उपयोग करते हैं, तो पुल गिर जाता है। इस शोध पत्र में, "पुल" एक गणितीय प्रमाण है। लेखक एक विशेष कंप्यूटर भाषा का उपयोग करते हैं जिसे Lean 4 कहा जाता है, जो जज के रूप में कार्य करती है।
- शोध पत्र का समाधान: Lean 4 एक अत्यंत सख्त रेफरी की तरह है। इसे इससे फर्क नहीं पड़ता कि आपका प्रमाण कितना "सुंदर" दिखता है; यह हर एक तार्किक चरण की जाँच करता है। यदि इसमें एक भी छोटी सी गलती होती है, तो रेफरी कहता है, "नहीं, यह गलत है।" यह सुनिश्चित करता है कि जब AI कहता है कि उसने एक समस्या हल कर ली है, तो उसने वास्तव में उसे किया है।
3. "जीवित पुस्तकालय" (एक विकसित होता बेंचमार्क)
आमतौर पर, एक बार टेस्ट बन जाने के बाद, वह हमेशा के लिए एक जैसा रहता है। लेकिन AI हर दिन स्मार्ट होता जा रहा है, इसलिए पुराने टेस्ट बहुत आसान हो जाते हैं।
- उपमा: एक वीडियो गेम की कल्पना करें जो हर सप्ताह अपडेट होता है। जैसे-जैसे खिलाड़ी बेहतर होते हैं, गेम कठिन स्तर जोड़ता है और मैप में बग्स को ठीक करता है।
- शोध पत्र का समाधान: यह बेंचमार्क एक "जीवित" परियोजना है।
- यह बढ़ता है: वे वास्तविक शोध पत्रों से नए प्रश्न जोड़ते रहते हैं।
- यह खुद को ठीक करता है: कभी-कभी, गणित की समस्याएँ अस्पष्ट रूप से लिखी जाती हैं। जब AI उन्हें हल करने की कोशिश करता है, तो वह इसलिए विफल हो सकता है क्योंकि समस्या स्पष्ट नहीं थी। यह विफलता मानव गणितज्ञों को यह समझने में मदद करती है कि, "ओह, हमने वह समस्या गलत लिखी थी!" फिर वे समस्या विवरण को ठीक करते हैं।
- इसके दो ट्रैक हैं:
- डिस्कवरी ट्रैक (खोज ट्रैक): अनसुलझी समस्याओं (यानी "फ्रेश मीट") को हल करने का प्रयास करना।
- ट्रांसलेशन ट्रैक (अनुवाद ट्रैक): उन समस्याओं को लेना जिन्हें मनुष्यों ने पहले ही हल कर लिया है और AI को उन्हें सख्त कंप्यूटर भाषा (Lean 4) में लिखना सिखाना।
4. "सेफ्टी नेट" (धोखाधड़ी से बचना)
लेखक "डेटा लीकेज" (AI द्वारा अपने प्रशिक्षण डेटा में उत्तर देखकर धोखाधड़ी करना) को लेकर चिंतित हैं।
- उपमा: छात्रों को धोखाधड़ी करने से रोकने के लिए, शिक्षक कभी-कभी उत्तर कुंजी को एक तिजोरी में बंद कर देते हैं और उसे केवल टेस्ट के बाद ही खोलते हैं।
- शोध पत्र का समाधान: उन्होंने टेस्ट का एक "फ्रोजन" (जमा हुआ) संस्करण बनाया है। यह 100 समस्याओं का एक स्नैपशॉट है जो समय में लॉक कर दिया गया है। भले ही मुख्य लाइब्रेरी बाद में बदल जाए, यह विशिष्ट स्नैपशॉट वैसा ही रहता है ताकि वैज्ञानिक बिना इस चिंता के विभिन्न AI मॉडल की निष्पक्ष तुलना कर सकें कि टेस्ट उनके नीचे बदल रहा है।
5. यह क्यों महत्वपूर्ण है
शोध पत्र दिखाता है कि यह प्रणाली पहले से ही काम कर रही है।
- वास्तविक परिणाम: वे उल्लेख करते हैं कि इस प्रणाली का उपयोग करके, एक AI (जिसे अरस्तू/Aristotle कहा जाता है) ने एक मानव गणितज्ञ को एक प्रसिद्ध समस्या को हल करने में मदद की जो लंबे समय से खुली हुई थी (Erdős Problem 124)।
- संकेत (The Signal): यह बेंचमार्क एक स्पष्ट "चढ़ने योग्य संकेत" (climbable signal) प्रदान करता है। यह सटीक रूप से दिखाता है कि AI ने कितनी प्रगति की है और उसे और कितनी दूर जाने की आवश्यकता है। यदि एक AI अनसुलझी समस्याओं में से 10% को हल करता है, तो यह एक बड़ी बात है। यदि यह 0% हल करता है, तो यह अभी तैयार नहीं है।
सारांश
फॉर्मल कॉन्जेक्चर (Formal Conjectures) AI गणितज्ञों के लिए एक नया, निरंतर अपडेट होने वाला खेल का मैदान है। यह काम की जाँच करने के लिए एक सख्त कंप्यूटर रेफरी (Lean 4) का उपयोग करता है, धोखाधड़ी को रोकने के लिए अभी तक हल न की गई समस्याओं पर ध्यान केंद्रित करता है, और एक सहयोगात्मक उपकरण के रूप में कार्य करता है जहाँ मनुष्य और AI एक-दूसरे को कठिन गणितीय प्रश्नों को स्पष्ट करने में मदद करते हैं। यह केवल एक परीक्षण नहीं है; यह वास्तविक गणितीय खोजों को करने के लिए एक उपकरण है।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।