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