यह पेज दुनियाभर में प्रकाशित होने वाले आर्टिफिशियल इंटेलिजेंस संबंधित रिसर्च पेपर्स को संक्षिप्त रूप में प्रस्तुत करता है। यहां Google Gemini का उपयोग करके पेपर्स का सारांश तैयार किया जाता है और यह पेज गैर-लाभकारी रूप से संचालित किया जाता है। पेपर के कॉपीराइट लेखक और संबंधित संस्थान के पास हैं, और साझा करते समय बस स्रोत का उल्लेख करें।
यह पत्र प्रस्तावात्मक स्वचालित औपचारिकीकरण के क्षेत्र में मजबूत स्वचालित मूल्यांकन मीट्रिक विकसित करने की चुनौतियों को संबोधित करता है, जो प्राकृतिक भाषा प्रस्तावों को स्वचालित रूप से औपचारिक भाषा में परिवर्तित करता है। मौजूदा मूल्यांकन विधियों की सीमाओं को संबोधित करने के लिए, जिसमें अपर्याप्त अर्थगत समझ, उच्च कम्प्यूटेशनल लागत और स्वचालित प्रमेय सिद्धि में सीमित प्रगति शामिल है, यह पत्र एक नया मूल्यांकन ढांचा, सामान्यीकृत वृक्ष संपादन दूरी (GTED) प्रस्तावित करता है। GTED औपचारिक प्रस्तावों को सामान्यीकृत करता है, उन्हें ऑपरेटर वृक्षों में रूपांतरित करता है, और फिर GTED मीट्रिक का उपयोग करके अर्थगत समानता को मापता है। GTED ने अत्याधुनिक प्रदर्शन का प्रदर्शन करते हुए miniF2F और ProofNet बेंचमार्क पर उच्चतम सटीकता और कप्पा मान प्राप्त किया। यह कम कम्प्यूटेशनल लागत के साथ एक विश्वसनीय स्वचालित मूल्यांकन मीट्रिक प्रदान करता है। कोड और प्रयोगात्मक परिणाम https://github.com/XiaoyangLiu-sjtu/GTED में पाए जा सकते हैं ।
मौजूदा स्वचालित मूल्यांकन मेट्रिक्स की सीमाओं को दूर करने के लिए एक नया मूल्यांकन ढांचा, GTED, प्रस्तावित किया गया है।
◦
मिनीएफ2एफ और प्रूफनेट बेंचमार्क पर उच्च सटीकता और कप्पा मान प्राप्त करके प्रदर्शन सत्यापन प्राप्त किया गया।
◦
यह एक मूल्यांकन मीट्रिक प्रदान करता है जो कम्प्यूटेशनल रूप से कम खर्चीला है और अर्थगत समानता को बेहतर ढंग से प्रतिबिंबित करता है।
◦
स्वचालित प्रस्ताव औपचारिकता पर अनुसंधान के विकास में योगदान दिया।
•
Limitations:
◦
यह निर्धारित करने के लिए आगे अनुसंधान की आवश्यकता है कि क्या GTED के प्रदर्शन को अन्य बेंचमार्क या अधिक जटिल प्रस्तावों पर सामान्यीकृत किया जा सकता है।
◦
अभी भी कुछ पहलू ऐसे हैं जो स्वचालित प्रूफ़ तकनीकों की प्रगति पर निर्भर हैं। (अंतर्निहित सीमाएँ)
◦
कुछ प्रकार के प्रस्तावों (अंतर्निहित सीमाओं) के लिए अनुकूलन संभावनाओं का अस्तित्व।
