यह शोधपत्र कोबलस्टोन का प्रस्ताव करता है, जो एक नवीन प्रमाण संश्लेषण उपकरण है जो कॉक जैसे प्रमाण सहायकों का उपयोग करके औपचारिक सत्यापन की दक्षता में सुधार के लिए एक बड़े पैमाने के भाषा मॉडल (एलएलएम) का लाभ उठाता है। कोबलस्टोन एलएलएम का उपयोग करके संभावित प्रमाण उत्पन्न करता है, जिनका उपयोग समस्या को छोटे भागों में विभाजित करने के लिए किया जाता है। यह स्वचालित रूप से सफलतापूर्वक सिद्ध किए गए भागों की पहचान करता है और शेष भागों पर पुनरावृति करके अंततः एक सही प्रमाण उत्पन्न करता है। एलएलएम की अनिश्चितता के बावजूद, कोबलस्टोन उत्पन्न प्रमाणों की शुद्धता की गारंटी देता है। प्रायोगिक परिणाम दर्शाते हैं कि कोबलस्टोन मौजूदा अत्याधुनिक उपकरणों से बेहतर प्रदर्शन करता है, और कई ऐसे प्रमेयों को सिद्ध करता है जिन्हें अन्य एलएलएम-आधारित उपकरण सिद्ध करने में विफल रहते हैं। इसकी दक्षता $1.25 की औसत निष्पादन लागत और 14.7 मिनट के रनटाइम द्वारा प्रदर्शित होती है। इसके अलावा, यह प्रमाण संरचना या संबंधित प्रमेयिकाओं का लाभ उठाने के लिए उपयोगकर्ताओं या अन्य उपकरणों से बाहरी इनपुट का उपयोग कर सकता है, और 58% तक प्रमेयों को सिद्ध कर सकता है। यह अध्ययन औपचारिक सत्यापन स्वचालन की दक्षता में सुधार के लिए आंशिक प्रगति और बाहरी इनपुट का लाभ उठाने की क्षमता को प्रदर्शित करता है।
