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