अब हमारे पास ऑटोमेशन का प्रमाण है
सॉफ़्टवेयर की formal verification, जिसे लंबे समय से बहुत महंगा और विशेषीकृत माना जाता था, अब बड़े language models द्वारा रूपांतरित हो रही है जो Lean जैसे systems के भीतर कई proofs generate और automate कर सकते हैं। टिप्पणीकारों का तर्क है कि इससे high-assurance code और यहाँ तक कि verified assembly भी अधिक domains के लिए व्यावहारिक हो सकती है, विशेष रूप से security-critical क्षेत्रों में, लेकिन वे इस बात पर ज़ोर देते हैं कि अच्छी specifications और abstractions लिखना अभी भी कठिन हिस्सा है और formal methods flawed spec के साथ गलत behavior को भी सही साबित कर सकते हैं। dependent types और total functions की real-world maintenance में scalability तथा क्या LLM-driven verification mainstream software engineering practices को वास्तव में बदलेगी या critical edge cases तक ही सीमित रहेगी, इस पर सक्रिय बहस जारी है.
LLMs + प्रमाण स्वचालन
- कई लोग LLMs + theorem provers (Lean, HOL-style systems, आदि) को एक बड़ा बदलाव मानते हैं: अब वे उन प्रमाणों के बड़े हिस्से को निपटा सकते हैं जिन्हें पहले दिनों या हफ्तों लगते थे।
- proof irrelevance और automation समृद्ध dependent-type प्रणालियों को अधिक व्यावहारिक बना सकती हैं, जिससे “proof engineering” का प्रयास कम हो सकता है, हालांकि अच्छे problem decomposition और abstractions अभी भी महत्वपूर्ण हैं।
- कुछ लोग सफल प्रयोगों का वर्णन करते हैं जहाँ LLMs ने बहु-दिवसीय formal proofs को मिनटों में फिर से बनाया, जिससे संकेत मिलता है कि पहले “insane” माने जाने वाले verification प्रोजेक्ट्स (kernels, प्रमुख theorems) अब एकल प्रयासों के लिए भी संभव हो सकते हैं।
बॉटलनेक के रूप में specifications
- कई लोगों का तर्क है कि सबसे कठिन हिस्सा correctness को साबित करना नहीं, बल्कि उसे परिभाषित करना है: वास्तविक दुनिया के software में अक्सर edge cases (network failures, backups, serializers, आदि) के लिए सटीक व्यवहार नहीं होता।
- formal specs लिखना code की लंबाई और जटिलता से भी अधिक हो सकता है; specs में bugs सीधे “verified” लेकिन गलत systems में बदल जाते हैं।
- partial specs (जैसे round-tripping, compress/decompress को inverses मानना, “arbitrary code कभी execute नहीं करता”) अभी भी बहुत मूल्यवान माने जाते हैं।
Dependent Types, Maintenance, और भाषा डिज़ाइन
- एक पक्ष का कहना है कि dependent types और total functions बड़े systems के लिए scale नहीं करते: कोई नया property जोड़ने के लिए कई types और proofs में नए invariants thread करने पड़ सकते हैं।
- प्रतिवाद: यह किसी भी बड़े system में correctness बनाए रखने जैसा ही है; अच्छा structuring (concerns को अलग करना, opaque types का उपयोग, छोटे trusted cores) इस कठिनाई को कम करता है।
- verification को type system में एकीकृत करने वाली भविष्य की languages आशाजनक मानी जाती हैं, लेकिन कई लोगों की अपेक्षा है कि अधिकांश programs केवल critical parts को verify करेंगे, पूरे systems को नहीं।
Security, Crypto, और Verified Assembly
- Blockchains और crypto को प्रमुख उम्मीदवारों के रूप में रेखांकित किया गया है: शक्तिशाली adversaries, formal methods का इतिहास, और verified assembly तथा compilers में रुचि।
- जैसे-जैसे exploit-finding सस्ता होता जाता है (AI सहित), कुछ लोगों का तर्क है कि formal verification आर्थिक रूप से अधिक आकर्षक हो जाता है; अन्य लोग सोचते हैं कि organizations “good enough” automated bug-finding पर ही रुक जाएँगी।
LLM व्यवहार, alignment, और सीमाएँ
- LLMs अक्सर भारी proof work से बचते हैं जब तक उन्हें दृढ़ता से prompt न किया जाए, सतही समाधानों को प्राथमिकता देते हैं, और शक्तिशाली libraries को भी बाध्य किए बिना अनदेखा कर सकते हैं।
- वे किसी feature को गलत तरीके से implement कर सकते हैं और फिर ऐसे tests/specs बना सकते हैं जो उस गलत behavior को “prove” कर दें, इसलिए specs की human review अभी भी अनिवार्य है।
- उत्साही लोग formal methods + LLMs को रूपांतरकारी मानते हैं; संशयवादी चेतावनी देते हैं कि इससे कठिनाई मुख्यतः उच्च-स्तरीय specification की ओर स्थानांतरित होगी और यह testing या human judgment की जगह नहीं लेगा।