यह पेज दुनियाभर में प्रकाशित होने वाले आर्टिफिशियल इंटेलिजेंस संबंधित रिसर्च पेपर्स को संक्षिप्त रूप में प्रस्तुत करता है। यहां Google Gemini का उपयोग करके पेपर्स का सारांश तैयार किया जाता है और यह पेज गैर-लाभकारी रूप से संचालित किया जाता है। पेपर के कॉपीराइट लेखक और संबंधित संस्थान के पास हैं, और साझा करते समय बस स्रोत का उल्लेख करें।
यह शोधपत्र ऑटोवेरस प्रस्तुत करता है, जो रस्ट कोड के लिए स्वचालित रूप से शुद्धता प्रमाण उत्पन्न करने वाला एक सिस्टम है। वेरस सत्यापन उपकरण की क्षमताओं का लाभ उठाने के लिए डिज़ाइन किया गया, ऑटोवेरस मानव विशेषज्ञों के प्रमाण-निर्माण चरणों की नकल करने के लिए लार्ज लैंग्वेज मॉडल (LLM) एजेंटों के एक नेटवर्क का उपयोग करता है: प्रारंभिक प्रमाण उत्पन्न करना, सामान्य सलाह के आधार पर प्रमाणों में सुधार करना, और सत्यापन त्रुटियों के आधार पर प्रमाणों को डीबग करना। हमने ऑटोवेरस का मूल्यांकन 150 असामान्य प्रमाण कार्यों वाले एक बेंचमार्क सूट पर किया है, जो दर्शाता है कि यह 90% से अधिक कार्यों के लिए स्वचालित रूप से सही प्रमाण उत्पन्न करता है और उनमें से आधे से अधिक को 30 सेकंड या तीन LLM कॉल के भीतर हल कर देता है।
Takeaways, Limitations
•
Takeaways:
◦
एलएलएम का उपयोग करके स्वचालित प्रूफ जनरेशन प्रौद्योगिकी विकसित करने की क्षमता का प्रदर्शन।
◦
रस्ट कोड सत्यापन की दक्षता में सुधार करने में योगदान देता है।
◦
ऑटोवेरस द्वारा प्रस्तावित एलएलएम एजेंट नेटवर्क और तीन-चरणीय प्रूफ निर्माण विधि भविष्य के अनुसंधान के लिए महत्वपूर्ण संदर्भ प्रदान करती है।
◦
150 असाधारण प्रमाण कार्यों का एक बेंचमार्क सेट भविष्य के अनुसंधान की प्रगति में योगदान देता है।
•
Limitations:
◦
यह अभी भी प्रारंभिक चरण की तकनीक है और इसने सभी प्रमाण समस्याओं को हल नहीं किया है (10% से भी कम समस्याओं का समाधान किया गया है)।
◦
एलएलएम कॉल की संख्या और समय की कमी के आधार पर प्रदर्शन में गिरावट की संभावना है।
◦
बेंचमार्क की सामान्यता निर्धारित करने के लिए आगे अनुसंधान की आवश्यकता है।
◦
अधिक जटिल और बड़े कोडों पर प्रयोज्यता का और अधिक सत्यापन आवश्यक है।
