पत्र में Why3 के लिए एक चरणबद्ध LLM-आधारित पाइपलाइन Diversify2Verify पेश किया गया है जो स्वचालित सत्यापन योग्यता को बढ़ाने के लिए विविध पुनरावर्ती और आदेशात्मक एरे/लिस्ट कार्यान्वयन उत्पन्न करता है। दृष्टिकोण प्रतिनिधित्व-विशिष्ट अनुबंधों का अनुमान लगाता है और सत्यापन विफलताओं को संभालने के लिए सीमित सत्यापक-मार्गदर्शित टिप्पणी मरम्मत का उपयोग करता है।
- लेखकों ने पूर्णांकों, एरे और लिस्ट पर 73 कार्यों का एक बेंचमार्क तैयार किया, जिससे 292 कार्यान्वयन भिन्नताएं प्राप्त हुईं।
- Diversify2Verify ने प्रारंभ में 96 आर्टिफैक्ट्स को सत्यापित किया, दो मरम्मत पास के बाद यह बढ़कर 154 हो गया।
- आर्टिफैक्ट-स्तर पर सत्यापन 32.9% से बढ़कर 52.7% हो गया।
- कार्य स्तर पर, 73 कार्यों में से कम से कम एक भिन्नता 49 कार्यों के लिए सत्यापित हुई, जिससे 67.1% सफलता दर प्राप्त हुई।
ये परिणाम दर्शाते हैं कि कार्यान्वयन विविधता कार्य-समकक्ष प्रोग्रामों में सत्यापन-अनुकूल आर्टिफैक्ट्स खोजने में मदद करती है।