AI से Formal Verification आसान, पर पूरी तरह नहीं
मूल शीर्षक: The ‘Pain in the Ass’ Math That Could Save Vibe Coding From Itself
यह क्यों महत्वपूर्ण है
AI-driven Formal Verification सुरक्षित और भरोसेमंद सॉफ़्टवेयर का आधार बन सकती है, जो पूरे उद्योग को प्रभावित करेगी।
Stanford शोधकर्ता Chuyue Sun ने AI टूल से Signal ऐप के कोड का Formal Verification आधे दिन में $500 से कम में पूरा किया, जो पहले तीन विशेषज्ञों को 5 महीने लेता था। Startup &Truth ने $70 मिलियन जुटाकर गुरुवार को लॉन्च किया।
दशकों से Formal Verification — यानी गणित से यह साबित करना कि सॉफ़्टवेयर बिल्कुल सही काम करता है — एक महंगी और धीमी प्रक्रिया रही है। अब Generative AI इसे बदलने की कोशिश कर रहा है। &Truth के Chief Science Officer Ilya Sergey का कहना है, "पुल और इमारतें इसलिए नहीं गिरतीं क्योंकि पहले गणित होती है। कोड के लिए भी यही क्यों न करें?"
&Truth के अलावा Harmonic — जिसे Robinhood CEO Vlad Tenev ने सह-स्थापित किया और जिसे $295 मिलियन की फंडिंग मिली है — ने इस हफ्ते घोषणा की कि उसका AI एजेंट Aristotle अब C भाषा और Verilog हार्डवेयर डिज़ाइन को Verify कर सकता है। Nvidia का Venture Capital इसमें निवेशक है और Tensordyne समेत कई Chipmaker इसे आज़मा रहे हैं।
पिछले हफ्ते Anthropic और Theorem ने मिलकर Open Source सॉफ़्टवेयर में ऐसे बग पकड़े जो खरबों Tests में नहीं मिले थे। Claude के लिए एक Verification Add-on भी पेश किया गया।
फिर भी यह तकनीक अभी Prototype चरण में है। Antithesis के Will Wilson जैसे जानकार इसे "झंझट भरा गणित" कहते हैं और मानते हैं कि User Error या Hardware खराबी से आए Bugs पकड़ना अभी इसके लिए मुश्किल है। NASA और Apple जैसी संस्थाओं से बाहर इसका आम उपयोग कब होगा, यह साफ नहीं।