अल्फाप्रूफ कोड आणि सिग्नल: तपासलेले मशीन-कोड सुरक्षा पुरावे आणि विश्वसनीय गृहितके

या व्हिडिओमध्ये काय समाविष्ट आहे

• एआय एजंट संभाव्य पुरावे तयार करतात; लीनचे कर्नल तपासते की ते मानवी-मंजूर औपचारिक दावा स्थापित करतात की नाही.
• सत्यापित लक्ष्य हे विशिष्ट संकलित लिबसिंग्नल CLI हार्नेस आहे, ज्यामध्ये विश्वसनीय सिमेंटिक्स आणि क्रिप्टोग्राफिक करार आहेत.
• संकलित बायनरी सिद्ध केल्याने त्या बायनरीच्या नमूद केलेल्या गुणधर्मांसाठी रस्ट कंपाइलर विश्वसनीय बेसपासून दूर होतो.
• संशोधकांनी पूर्वी दुरुस्त केलेल्या बग्सचे दोन स्वतंत्र पुन्हा सादर केले, जे त्यांच्या प्रतीकात्मक सुरक्षा प्रमेयाचे उल्लंघन करतात.
• तुलनाकर्ता प्रमेय आणि प्रत्येक अवलंबून असलेली व्याख्या संरक्षित मंजूर तपशीलाविरुद्ध तपासतो; दुरुस्त्या एका स्वतंत्र पुनरावलोकन केलेल्या प्रक्रियेतून जातात.

अनुवादित प्रतिलेख

मूळ इंग्रजी निवेदनातून अनुवादित. उपलब्ध ऑडिओ आणि मथळे YouTube द्वारे नियंत्रित आहेत.

एआय सुरक्षा पुरावा कोण तपासतो?

0:00 एआय सुरक्षा ऑडिट अजूनही चॅटबॉटवर विश्वास ठेवण्यासारखे वाटते. गुगलचा नवीन सिग्नल परिणाम एका स्वतंत्र कर्नलद्वारे गणितीय पुराव्यांसह येतो तपासणी करतो. या व्हिडिओमध्ये, गुगलने काय सिद्ध केले? आणि ते एजंटला गोलपोस्ट्स हलवण्यापासून कसे थांबवतात? येथे उपयुक्त उत्तर आहे. मॉडेल्स संभाव्य पुरावे लिहितात, आणि लीन संकलित कोडबद्दल मानवी-मंजूर दाव्याविरुद्ध पुरावे तपासतो. मानवी-मंजूर दाव्याविरुद्ध निवडक संकलित कोडबद्दल. दावा आणि गृहितके अजूनही मानवांच्या मालकीची आहेत.

0:21 आपण मॉडेलच्या विजयाच्या भाषणावर विश्वास न ठेवता परिणाम तपासू शकता. एक स्वतंत्र तपासणी प्रश्न शांतपणे बदलण्यापासून थांबवते. आपण व्याख्यांपर्यंत खाली जाऊ. आज मंगळवार, नोव्हेंबर दहा, आणि हे The Daily Diff आहे. अल्फाप्रूफ कोड हे गुगलचे सॉफ्टवेअर तपशील मानवी मार्गदर्शनाखाली लिहिण्यासाठी आणि एआय एजंट्ससह तपासलेले पुरावे तयार करण्यासाठीचे फ्रेमवर्क आहे. मानवी मार्गदर्शनाखाली आणि एआय एजंट्ससह तपासलेले पुरावे तयार करण्यासाठीचे फ्रेमवर्क आहे. हे अभ्यास libsignal ला लक्ष्य करतो, सिग्नलच्या संदेशन प्रोटोकॉलची अंमलबजावणी करणारी रस्ट लायब्ररी, एका विशिष्ट कमांड-लाइन प्रोग्राममध्ये. गुगलने आज या कामाची घोषणा केली.

0:45 गुगलने आज या कामाची घोषणा केली. त्याच्या पेपरमध्ये म्हटले आहे की पाच संशोधकांनी चार आठवड्यांहून अधिक काम केले. एजंट्सने पुरावे लिहिले, तर मानवांनी त्यांचा बहुतेक प्रयत्न तपशीलांवर खर्च केला. आवश्यकता अधिक महागड्या बैठका बनण्याचा मार्ग शोधत आहेत. आवश्यकता अधिक महागड्या बैठका बनण्याचा मार्ग शोधत आहेत. तपशील सांगतो की प्रोग्रामने काय केले पाहिजे,

दावा पुरावा लक्ष्य कसा बनतो?

0:59 हल्ला करणारा काय नियंत्रित करतो, आणि युक्तिवादाला कोणत्या गृहितकांची आवश्यकता आहे. पुनरावलोकनकर्ते विचारतात की ते लोकांना ज्या सुरक्षिततेची काळजी आहे ते कॅप्चर करते का. एका कमकुवत प्रश्नाला सुंदरपणे तपासलेले उत्तर तो प्रश्न तसाच ठेवतो. टीम सिग्नलच्या हँडशेक आणि त्याच्या मेसेज-की रॅचेटवरील आधीच्या संशोधनावर आधारित आहे. औपचारिक विश्लेषणांनी आधीच त्या डिझाइन्सचा अभ्यास केला आहे. गुगलचा दावा त्यांच्या सुरक्षा युक्तिवादांना एका अपरिवर्तित उत्पादन लायब्ररीच्या संकलित अंमलबजावणीशी जोडतो, जिथे डिझाइनला वास्तविक कोडच्या संपर्कात टिकून राहावे लागते. सिग्नलचे मुख्य तंत्रज्ञान अधिकारी, एहरेन क्रेट,

1:27 आधीच्या पडताळणीच्या लहान कार्यक्षेत्रांपलीकडे विस्ताराचे वर्णन करतात. अंमलबजावणीच्या तपशीलांमध्ये आउट-ऑफ-ऑर्डर संदेश आणि विलंबित संदेशांसाठी संग्रहित सत्रे समाविष्ट आहेत. वास्तविक सॉफ्टवेअर तुमच्या सुंदर आकृतीने टाकून दिलेल्या पावत्या ठेवते. संशोधक अपरिवर्तित रस्ट लायब्ररीला मानक कंपाइलरसह आर्म सिक्सटी-फोर लिनक्स एक्झिक्यूटेबलमध्ये संकलित करतात.

संकलित बायनरी का सिद्ध करावी?

1:41 संशोधक अपरिवर्तित रस्ट लायब्ररीला मानक कंपाइलरसह आर्म सिक्सटी-फोर लिनक्स एक्झिक्यूटेबलमध्ये संकलित करतात. त्यांचे प्रमेय औपचारिक सूचना मॉडेल वापरून त्या बायनरीचे वर्णन करतात, स्रोत आणि ऑप्टिमाइझ केलेल्या मशीन कोडमधील अंतर ओलांडून. एक कंपाइलर त्रुटी जी नमूद केलेला गुणधर्म मोडते, त्याचे प्रमेय खोटे ठरवेल. म्हणून कंपाइलर या बायनरीसाठी विश्वसनीय बेस सोडतो. आपण अजूनही सूचना मॉडेल आणि लीनच्या तपासकावर विश्वास ठेवता. विश्वासाची सीमा हलली आहे, आणि तिला एक पत्ता आहे. सुमारे साडेसहा दशलक्ष ओळींचे तपासलेले पुरावे अंदाजे सव्वीस हजार विश्वसनीय तपशील आणि सूचना-सिमेंटिक्स ओळींवर आधारित आहेत.

2:06 हजार विश्वसनीय तपशील आणि सूचना-सिमेंटिक्स ओळींवर आधारित आहेत. हे आर्टिफॅक्ट गणना आहेत. त्यांना बुद्धिमत्तेचे गुण मानणे म्हणजे विकासकांना त्यांच्या नोड मॉड्यूल्स फोल्डरच्या आकारानुसार क्रमवारी लावण्यासारखे आहे. त्यांना बुद्धिमत्तेचे गुण मानणे म्हणजे विकासकांना त्यांच्या नोड मॉड्यूल्स फोल्डरच्या आकारानुसार क्रमवारी लावण्यासारखे आहे.

कोणत्या सुरक्षा गुणधर्मांनी अंमलबजावणीतील अंतर टिकवून ठेवले?

2:16 युक्तिवादांमध्ये संदेश गोपनीयता आणि प्रमाणीकरण समाविष्ट आहे, नमूद केलेल्या मॉडेल्समध्ये फॉरवर्ड सिक्रेसी आणि पोस्ट-कॉम्प्रमाइज सिक्रेसीसह. ते शेवटचे दोन चोरी झालेल्या-की नुकसानाची मर्यादा आणि नवीन देवाणघेवाणीनंतरची पुनर्प्राप्ती वर्णन करतात. प्रत्येक हमीला हल्ला करणारा आणि सत्रावर अटी आहेत. क्रिप्टोग्राफिक प्रिमिटिव्हज विश्वसनीय करारांमागे बसलेले आहेत. पुरावा गृहीत धरतो की त्या रूटीन्स नमूद केल्यानुसार वागतात आणि क्रिप्टोग्राफिक सुरक्षा गृहितकांवर अवलंबून असतात. सुरक्षा गृहितकांवर अवलंबून असतात. एक पुरावा क्रिप्टोग्राफीला आदर्श बनवतो; दुसरा हल्ला करणाऱ्याच्या यश संभाव्यतेबद्दल विचार करतो. सुरक्षा गृहितकांवर अवलंबून असतात. एक पुरावा क्रिप्टोग्राफीला आदर्श बनवतो; दुसरा हल्ला करणाऱ्याच्या यश संभाव्यतेबद्दल विचार करतो.

2:42 दोन्हीमध्ये त्यांनी समाविष्ट केलेल्या परिस्थितीवर मर्यादा आहेत. कोणती बिल्ड, कोणता गुणधर्म आणि कोणती गृहितके विचारा. हा परिणाम संशोधकांच्या कमांड-लाइन हार्नेसशी संबंधित आहे. गट संदेशन हे भविष्यातील काम आहे, आणि कम्प्यूटेशनल मॉडेल मल्टी-डिव्हाइस स्थिती वगळते. प्रत्येक सिग्नल इन्स्टॉलेशनला बग-मुक्त म्हणणे प्रमेयाच्या बाहेर भटकते. संशोधकांनी पूर्वी दुरुस्त केलेले दोन सिग्नल बग्स वेगळ्या प्रतींमध्ये पुन्हा सादर केले आणि त्यांना संकलित केले.

तपशील तुटलेला कोड नाकारू शकतो का?

3:02 संशोधकांनी पूर्वी दुरुस्त केलेले दोन सिग्नल बग्स वेगळ्या प्रतींमध्ये पुन्हा सादर केले आणि त्यांना संकलित केले. तपासलेल्या पुराव्यांनी दाखवले की त्या बायनरींनी प्रतीकात्मक सुरक्षा प्रमेयाचे उल्लंघन केले. त्याने तपासले की तपशील वास्तविक तुटलेल्या अंमलबजावणींना नाकारू शकतो का. तुमच्या हिरव्या चेकला लाल चाचणीची आवश्यकता आहे. गुगल तपासणीच्या सूचनांसह तपशील आणि पुरावे प्रकाशित करते. रिपॉझिटरी म्हणते की स्वच्छ बिल्डला काही तास आणि लक्षणीय मेमरी लागते. लॅपटॉपवर घोषणा वाचणे खूप सोपे आहे. हार्डवेअर मॉडेल आणि विश्वसनीय करारांना अजूनही पुनरावलोकनाची आवश्यकता आहे.

3:26 मी या भागासाठी प्रचंड आर्टिफॅक्ट पुन्हा तयार केले नाही. आम्ही प्रकाशित परिणाम आणि त्याच्या मर्यादांची नोंद करत आहोत. बाहेरील लोकांना त्याची तपासणी करण्याचा मार्ग आहे, जो मला दुसऱ्या एआय विजयाच्या फेरीपेक्षा जास्त महत्त्वाचा वाटतो. बाहेरील लोकांना त्याची तपासणी करण्याचा मार्ग आहे, जो मला दुसऱ्या एआय विजयाच्या फेरीपेक्षा जास्त महत्त्वाचा वाटतो. आता सापळा.

एक योग्य पुरावा चुकीच्या प्रश्नाचे उत्तर देऊ शकतो का?

3:36 लीन अशा विधानाचा योग्य पुरावा स्वीकारू शकते जे जवळजवळ काहीच मागत नाही. अशक्य गृहितके प्रमेयाला निरर्थक बनवू शकतात. मुख्य प्रमेयाच्या खाली दडलेली व्याख्या बदलल्याने ध्येय कमकुवत होऊ शकते. पेपर यासाठी तपासण्या डिझाइन करतो. द्वारपाल एक संरक्षित मंजूर तपशील ठेवतो ज्यावर पुरावा एजंट लिहू शकत नाहीत. ते एका स्वतंत्र दुरुस्ती प्रक्रियेद्वारे सुधारणा प्रस्तावित करू शकतात. सुरक्षा कमकुवत होणे संभाव्य बग म्हणून वाढवले जाते. सिद्ध करणार्‍याच्या यशाच्या घोषणेला येथे कोणताही अधिकार नाही.

4:00 मानव विश्वसनीय गृहितकांच्या बदलांवर निर्णय घेतात, थेट किंवा त्यांच्या धोरणाद्वारे, आणि प्रत्येक मोहिमेनंतर दुरुस्त्यांचे पुनरावलोकन करतात. तज्ञांचा निर्णय अजूनही धोक्यात असतो. एजंट वेगळी असाइनमेंट मागू शकतो. तो स्वतःला उत्तीर्ण गुण देऊ शकत नाही.

हलत्या गोलपोस्ट्सला काय पकडते?

4:13 येथे वचनबद्ध तपासणी आहे. लीनचा तुलनाकर्ता प्रमेय आणि ते अवलंबून असलेल्या प्रत्येक व्याख्येची त्या संरक्षित मंजूर प्रतीशी तुलना करतो. ते अवलंबून असलेल्या प्रत्येक व्याख्येची त्या संरक्षित मंजूर प्रतीशी तुलना करतो. ते मंजूर स्वयंसिद्धके देखील तपासते आणि ताज्या कर्नलमध्ये पुरावा पुन्हा चालवते. म्हणून, मदतनीस व्याख्या शांतपणे कमकुवत केल्याने तुलना केली जात असलेली वस्तू बदलते. एका स्वीकृत पुराव्याला मंजूर लक्ष्य स्थापित करावे लागते. ते अजूनही मानवांना एक मजबूत लक्ष्य आणि प्रामाणिक गृहितके निवडण्यासाठी जबाबदार ठेवते. आपल्या स्वतःच्या एआय वर्कफ्लोसाठी, स्वीकृती निकष कर्मचाऱ्याच्या संपादन परवानगीच्या बाहेर ठेवा आणि प्रस्तावित बदलांचे स्वतंत्रपणे पुनरावलोकन करा.

4:37 आपल्या स्वतःच्या एआय वर्कफ्लोसाठी, स्वीकृती निकष कर्मचाऱ्याच्या संपादन परवानगीच्या बाहेर ठेवा आणि प्रस्तावित बदलांचे स्वतंत्रपणे पुनरावलोकन करा. गुगलचा परिणाम ते वेगळेपण ठोस करतो. पुरावा लेखक काम करतो; तपासणीची सीमा ठरवते की ते मोजले जाते की नाही. आपण हे ऐकण्याऐवजी वाचणे पसंत करत असाल, तर रोज सकाळी आपल्या इनबॉक्समध्ये डिफ येतो, daily diff dot dev वर विनामूल्य, खाली लिंक आहे. तर आजचा निकाल SHIP IT आहे.

मी ही पुरावा वर्कफ्लो शिप करेन का?

4:54 मी हे तपासलेले-पुरावा वर्कफ्लो शिप करेन कारण मंजूर दावा एजंटपासून वेगळा राहतो जो उत्तर तयार करतो. मी हे तपासलेले-पुरावा वर्कफ्लो शिप करेन कारण मंजूर दावा एजंटपासून वेगळा राहतो जो उत्तर तयार करतो. मी प्रत्येक परिणामाला व्याप्ती आणि गृहितके संलग्न ठेवीन. सदस्यत्व घ्या, बेल दाबा आणि टिप्पण्यांमध्ये सांगा की तुम्ही त्याला वेगळ्या प्रकारे शिक्का मारला असता का. आणि आजचा डिफ एवढाच. मी Axrisi कडून निको आहे. जबाबदारीने विलीन करा.

स्रोत

1. AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — technical scope, trusted base and gatekeepingSwarat Chaudhuri and colleagues / Google DeepMind and Google
2. Introducing AlphaProof Code — November 10 announcement and attributed Signal CTO responsePushmeet Kohli and Swarat Chaudhuri / Google DeepMind
3. Code-verification repository — initial commit, public artifacts and checking instructionsGoogle DeepMind / GitHub
4. The PQXDH Key Agreement Protocol — older official specification and prior-analysis contextEhren Kret and Rolfe Schmidt / Signal
5. The Double Ratchet Algorithm — Triple Ratchet sectionTrevor Perrin, Moxie Marlinspike and Rolfe Schmidt / Signal
6. Google DeepMind leadership — Demis Hassabis's relevant lab identityGoogle DeepMind
7. Demis Hassabis in 2025 — authentic portrait, cropped/resized/compressed and unflipped; no background removal or generated expression/detail; lab identity only, no authorship, proof writing, current reaction or endorsementChristopher P. Michel / Cmichel67 / Wikimedia Commons
8. Portrait licence — CC BY-SA 4.0; attribution, adaptation disclosure and ShareAlikeCreative Commons
9. Expanding Brain template — cropped/captioned artifact-count satire, brief transformed <=2s commentary; no benchmark, hosting licence, legal-clearance or blanket reuse claimImgflip / user-uploaded meme template
10. Tom and Jerry — Boomerang Official actual animated reaction, silent resized/captioned 1.875s excerpt; brief transformed process commentary, no actual researcher or executive reaction, hosting licence, legal-clearance or blanket reuse claimBoomerang Official / GIPHY / Tom and Jerry
11. Boomerang GIF source link — uploader-provided provenanceBoomerang
12. AlphaProof Code discussion — attention context, anonymous opinions excluded from factual proof claimsHacker News
13. Code-verification licence — Apache 2.0 for Google code, third-party licences retainedGoogle / GitHub