ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers
यह शोध पत्र ITPEval प्रस्तुत करता है, जो चार प्रमुख इंटरैक्टिव थ्योरम प्रूवर्स (interactive theorem provers) में स्वचालित औपचारिक प्रमाण अनुवाद (automated formal proof translation) के मूल्यांकन के लिए पहला बेंचमार्क और एकीकृत बुनियादी ढांचा है, जो यह प्रकट करता है कि वर्तमान लार्ज लैंग्वेज मॉडल्स लाइब्रेरी मिसमैच (library mismatches) के कारण प्रमाण अनुवाद में काफी संघर्ष करते हैं और केवल नेटिव टाइप-चेकिंग (native type-checking) अक्सर सिमेंटिक फिडेलिटी (semantic fidelity) का अतिरंजित अनुमान लगाती है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
एक ऐसी दुनिया की कल्पना करें जहाँ गणितज्ञ चार अलग-अलग भाषाएँ बोलते हैं, लेकिन वे सभी बिल्कुल एक ही पहेलियों को हल करने की कोशिश कर रहे हैं। "औपचारिक प्रमेय सिद्ध करने" (formal theorem proving) के उच्च-दांव वाले अखाड़े में, कंप्यूटर अंतिम रेफरी के रूप में कार्य करते हैं, जो यह सुनिश्चित करने के लिए गणितीय प्रमाण के हर एक चरण की जाँच करते हैं कि वह 100% सही है। हालाँकि, ठीक वैसे ही जैसे फ्रांसीसी, जापानी, स्वाहिली और अरबी बोलने वाले इंसान होते हैं, इन कंप्यूटर प्रणालियों (जिन्हें इंटरएक्टिव थ्योरम प्रूवर्स या ITPs कहा जाता है) की भी अपनी अनूठी व्याकरण, शब्दावली और पूर्व-अनुमोदित तथ्यों के पुस्तकालय होते हैं। एक प्रणाली में पूर्णता से लिखा गया प्रमाण दूसरी प्रणालियों के लिए निरर्थक हो सकता है। यह एक अकेली समस्या पैदा करता है: यदि एक शानदार प्रमाण एक भाषा में लिखा गया है, तो उसे अन्यों द्वारा आसानी से उपयोग या जांचा नहीं जा सकता है। वैज्ञानिक इस अंतर को पाटने के लिए "सार्वभौमिक अनुवादक" बनाने की कोशिश कर रहे हैं, इस उम्मीद में कि आर्टिफिशियल इंटेलिजेंस (AI) इन गणितीय प्रमाणों को स्वचालित रूप से अनुवादित करना सीख सकता है, जिससे पूरा समुदाय अपना काम साझा कर सके।
यहाँ ITPEVAL है, एक नया अध्ययन जो एक विशाल, कठोर भाषा परीक्षा की तरह कार्य करता है। शोधकर्ताओं ने यह देखना चाहा कि क्या आज के सबसे स्मार्ट AI मॉडल वास्तव में चार प्रमुख प्रणालियों: Lean 4, Rocq, Isabelle, और HOL Light के बीच औपचारिक गणितीय प्रमाणों का अनुवाद कर सकते हैं। उन्होंने केवल AI से अनुमान लगाने के लिए नहीं कहा; उन्होंने 1,500 से अधिक स्रोत फ़ाइलों और लगभग 7,000 प्रमेयों के साथ एक विशेष परीक्षण क्षेत्र बनाया। उन्होंने परीक्षण को दो स्तरों में विभाजित किया: एक "नियंत्रित" (Controlled) स्तर जिसमें सरल, स्व-निहित गणितीय समस्याएँ थीं (जैसे कि बिना किसी बाहरी संदर्भ वाला शब्दावली क्विज़), और एक "पारिस्थितिकी तंत्र" (Ecosystem) स्तर जो वास्तविक, जटिल लाइब्रेरी कोड का उपयोग करता है जो विशिष्ट प्रणाली-आधारित नियमों पर निर्भर करता है (जैसे कि मुहावरों और सांस्कृतिक संदर्भों के साथ एक पूरी बातचीत)।
परिणाम "बुरा नहीं है" और "अभी भी बहुत कठिन है" का मिश्रण थे। जब AI ने प्रमेयों के केवल कथनों (क्या) को अनुवादित करने की कोशिश की, तो सर्वश्रेष्ठ मॉडल लगभग 29.1% सही रहे। लेकिन जब वास्तविक प्रमाणों (कैसे) को अनुवादित करने के लिए कहा गया, तो सफलता दर गिरकर केवल 10.5% रह गई। अध्ययन में पाया गया कि सबसे बड़ी बाधा गणित स्वयं या विभिन्न तार्किक आधार नहीं था; बल्कि "पारिस्थितिकी तंत्र" था। AI को सबसे अधिक संघर्ष तब करना पड़ा जब उसे लक्षित प्रणाली के विशिष्ट पुस्तकालयों, नामकरण परंपराओं और स्वचालन शैलियों को समझना था। यह ऐसा ही है जैसे AI "बिल्ली चटाई पर बैठी है" वाक्य को समझ सकता है, लेकिन जब उससे उस विशिष्ट बोली में अनुवाद करने के लिए कहा गया जिसमें एक विशिष्ट ब्रांड की चटाई और एक विशिष्ट प्रकार की बिल्ली की आवश्यकता थी, तो वह विफल हो गया।
इसके अलावा, शोधकर्ताओं ने पाया कि केवल कंप्यूटर को "यह सही दिखता है" (एक टाइप-चेक) कहने के लिए प्रेरित करना पर्याप्त नहीं है। उन्होंने एक गहरा "अर्थ जाँच" (meaning check) चलाया और पाया कि भले ही AI का अनुवाद कंप्यूटर के बुनियादी परीक्षण में पास हो गया हो, लेकिन 46% मामलों में यह अक्सर गणितीय रूप से कमजोर या मूल से थोड़ा भिन्न था। अध्ययन सुझाव देता है कि जबकि AI बुनियादी बातों में बेहतर हो रहा है, इसे वास्तव में एक सार्वभौमिक अनुवादक बनने से पहले प्रत्येक गणित प्रणाली की अनूठी "संस्कृति" के अनुकूल होने का प्रशिक्षण लेने की आवश्यकता है। लेखकों ने एक "राउंड-ट्रिप" परीक्षण का भी पता लगाया, जहाँ उन्होंने गणित को प्राकृतिक भाषा में और फिर वापस अनुवादित किया, जिससे पता चला कि परिणाम इस बात पर बहुत अधिक निर्भर करते थे कि किस प्रणाली का उपयोग किया गया था, जो संकेत देता है कि कई प्रणालियों का एक साथ उपयोग करना मदद कर सकता है, लेकिन यह अभी तक कोई जादुई समाधान नहीं है।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।