AlphaProof Code සහ Signal: යන්ත්‍ර-කේත ආරක්ෂක සාධනයන් සහ විශ්වාසදායී උපකල්පන පරීක්ෂා කරන ලදී

මෙම වීඩියෝවෙන් ආවරණය වන දේ

• AI නියෝජිතයන් අපේක්ෂක සාධනයන් නිපදවයි; Lean ගේ කර්නලය මගින් ඒවා මිනිසා විසින් අනුමත කරන ලද විධිමත් හිමිකම තහවුරු කරන්නේද යන්න පරීක්ෂා කරයි.
• සත්‍යාපනය කරන ලද ඉලක්කය වන්නේ විශ්වාසදායී අර්ථ ශාස්ත්‍රය සහ ගුප්ත ලේඛනගත කොන්ත්‍රාත්තු සහිත විශේෂිත සම්පාදනය කරන ලද libsignal CLI හානස් එකකි.
• සම්පාදනය කරන ලද ද්විමය ගොනුව සාධනය කිරීමෙන් එම ද්විමය ගොනුවේ ප්‍රකාශිත ගුණාංග සඳහා Rust සම්පාදකය විශ්වාසදායී පදනමෙන් ඉවත් කරයි.
• පර්යේෂකයන් විසින් ඔවුන්ගේ සංකේතාත්මක ආරක්ෂක ප්‍රමේයය උල්ලංඝනය කරන, මීට පෙර නිවැරදි කරන ලද දෝෂ දෙකක් හුදකලාව නැවත හඳුන්වා දීම වාර්තා කරයි.
• සංසන්දකයක් විසින් ප්‍රමේයය සහ සෑම රඳා පවතින අර්ථ දැක්වීමක්ම ආරක්ෂිත අනුමත පිරිවිතරයකට එරෙහිව පරීක්ෂා කරයි; සංශෝධන වෙනම සමාලෝචනය කරන ලද ක්‍රියාවලියක් හරහා සිදු වේ.

පරිවර්තනය කරන ලද පිටපත

මුල් ඉංග්‍රීසි නිරූපණයෙන් පරිවර්තනය කරන ලදී. පවතින ශ්‍රව්‍ය සහ ශීර්ෂ පාඨ YouTube මගින් පාලනය වේ.

AI ආරක්ෂක සාධනයක් පරීක්ෂා කරන්නේ කවුද?

0:00 AI ආරක්ෂක විගණනයක් තවමත් චැට්බෝට් එකක් විශ්වාස කිරීමක් සේ පෙනේ. Google හි නව Signal ප්‍රතිඵලය වෙනම කර්නලයක් මගින් ගණිතමය සාධනයන් සමඟ පැමිණේ පරීක්ෂා කරයි. මෙම වීඩියෝවෙන්, Google විසින් ඔප්පු කළේ කුමක්ද? තවද ඔවුන් නියෝජිතයෙකු ඉලක්ක චලනය කිරීම නවත්වන්නේ කෙසේද? මෙන්න ප්‍රයෝජනවත් පිළිතුර. මාදිලි අපේක්ෂක සාධනයන් ලියන අතර, Lean සාධනයන් මානව-අනුමත තෝරාගත් සම්පාදිත කේතය පිළිබඳ හිමිකමක් සමඟ පරීක්ෂා කරයි. මානවයන් තවමත් හිමිකම සහ උපකල්පන වල අයිතිකරුවන්ය.

0:21 මාදිලියේ ජයග්‍රාහී කථාව විශ්වාස නොකර ඔබට ප්‍රතිඵලය පරීක්ෂා කළ හැකිය. වෙනම පරීක්ෂාවකින් ප්‍රශ්නය නිශ්ශබ්දව වෙනස් කිරීම අල්ලා ගනී. අපි එය අර්ථ දැක්වීම් දක්වා අනුගමනය කරන්නෙමු. අද නොවැම්බර් දහය, අඟහරුවාදා වන අතර මෙය The Daily Diff. AlphaProof Code යනු මානව මග පෙන්වීම යටතේ මෘදුකාංග පිරිවිතර ලිවීමට සහ AI නියෝජිතයන් සමඟ පරීක්ෂා කරන ලද සාධනයන් ජනනය කිරීම සඳහා Google හි රාමුවයි. මෙම අධ්‍යයනය ඉලක්ක කරන්නේ Signal හි පණිවිඩකරණ ප්‍රොටෝකෝලය ක්‍රියාත්මක කරන Rust පුස්තකාලය වන libsignal, විශේෂිත විධාන රේඛා වැඩසටහනක් තුළය.

0:45 Google විසින් අද මෙම කාර්යය ප්‍රකාශයට පත් කරන ලදී. එහි ලිපියේ සඳහන් වන්නේ පර්යේෂකයන් පස් දෙනෙකු සති හතරක් පුරා වැඩ කළ බවයි. නියෝජිතයන් සාධනයන් ලියන අතර, මිනිසුන් ඔවුන්ගේ උත්සාහයෙන් වැඩි කොටසක් පිරිවිතරයන් සඳහා යොදවා ඇත. අවශ්‍යතා තව තවත් මිල අධික රැස්වීම් බවට පත් වීමට මාර්ගයක් සොයාගෙන ඇත. පිරිවිතරයෙන් කියැවෙන්නේ වැඩසටහන කළ යුත්තේ කුමක්ද,

හිමිකමක් සාධන ඉලක්කයක් බවට පත් වන්නේ කෙසේද?

0:59 ප්‍රහාරකයෙකු පාලනය කරන්නේ කුමක්ද, සහ තර්කයට අවශ්‍ය උපකල්පන මොනවාද යන්නයි. සමාලෝචකයන් අසන්නේ එය මිනිසුන් සැලකිලිමත් වන ආරක්ෂාව ග්‍රහණය කරන්නේද යන්නයි. දුර්වල ප්‍රශ්නයකට අලංකාර ලෙස පරීක්ෂා කරන ලද පිළිතුරක් එම ප්‍රශ්නය නොවෙනස්ව තබයි. කණ්ඩායම Signal හි හෑන්ඩ්ෂේක් සහ එහි පණිවිඩ-යතුරු රැචට් පිළිබඳ පෙර පර්යේෂණ මත ගොඩනැගී ඇත. විධිමත් විශ්ලේෂණයන් දැනටමත් එම සැලසුම් අධ්‍යයනය කර ඇත. Google හි හිමිකම ඔවුන්ගේ ආරක්ෂක තර්ක නොවෙනස් නිෂ්පාදනයක පුස්තකාලයේ සම්පාදිත ක්‍රියාත්මක කිරීමකට සම්බන්ධ කරයි, එහිදී සැලසුමට සැබෑ කේතය සමඟ සම්බන්ධතාවයෙන් බේරීමට සිදුවේ. Signal හි ප්‍රධාන තාක්ෂණ නිලධාරී, Ehren Kret,

1:27 පෙර සත්‍යාපනයෙහි කුඩා විෂය පථයන් ඉක්මවා පුළුල් කිරීමක් විස්තර කරයි. ක්‍රියාත්මක කිරීමේ විස්තර වලට අනුපිළිවෙලින් තොර පණිවිඩ සහ ගබඩා කරන ලද සැසි ඇතුළත් වේ ප්‍රමාද වූ පණිවිඩ සඳහා. සැබෑ මෘදුකාංගය ඔබේ අලංකාර රූප සටහන ඉවතලන ලද ලදුපත් තබා ගනී. පර්යේෂකයන් විසින් නොවෙනස් Rust පුස්තකාලය සම්මත

සම්පාදනය කරන ලද ද්විමය ගොනුව සාධනය කරන්නේ ඇයි?

1:41 සම්පාදකය සමඟ Arm sixty-four Linux ක්‍රියාත්මක කළ හැකි ගොනුවක් බවට සම්පාදනය කරයි. ඔවුන්ගේ ප්‍රමේයයන් එම ද්විමය ගොනුව විධිමත් උපදෙස් ආකෘතියක් භාවිතා කර විස්තර කරයි, මුලාශ්‍රය සහ ප්‍රශස්තකරණය කරන ලද යන්ත්‍ර කේතය අතර පරතරය හරහා ළඟා වේ. ප්‍රකාශිත ගුණාංගයක් බිඳ දමන සම්පාදක දෝෂයක් එහි ප්‍රමේයය අසත්‍ය කරනු ඇත. එබැවින් සම්පාදකය මෙම ද්විමය ගොනුව සඳහා විශ්වාසදායී පදනමෙන් ඉවත් වේ. ඔබ තවමත් උපදෙස් ආකෘතිය සහ Lean ගේ පරීක්ෂකය විශ්වාස කරයි. විශ්වාසදායී සීමාව චලනය වී ඇති අතර, එයට ලිපිනයක් ඇත. මිලියන හයහමාරක් පමණ පරීක්ෂා කරන ලද සාධන රේඛා දළ වශයෙන් විසිහයදහසක්

2:06 විශ්වාසදායී පිරිවිතර සහ උපදෙස්-අර්ථ ශාස්ත්‍ර රේඛා මත රඳා පවතී. මේවා කෞතුක වස්තු ගණනය කිරීම් වේ. ඒවා බුද්ධි ලකුණු ලෙස සැලකීම, සංවර්ධකයින් ඔවුන්ගේ node modules ෆෝල්ඩරයේ ප්‍රමාණය අනුව ශ්‍රේණිගත කිරීමක් වැනිය.

ක්‍රියාත්මක කිරීමේ පරතරයෙන් පසු ඉතිරි වූ ආරක්ෂක ගුණාංග මොනවාද?

2:16 තර්ක මගින් පණිවිඩ රහස්‍යභාවය සහ සත්‍යාපනය ආවරණය කරයි, ප්‍රකාශිත මාදිලි යටතේ ඉදිරි රහස්‍යභාවය සහ සම්මුති-පසු ආරක්ෂාව සමඟ. අවසාන දෙකෙන් විස්තර කරන්නේ සොරකම් කරන ලද-යතුරු හානි සහ නව හුවමාරු කිරීම් වලින් පසු ප්‍රතිසාධනය සඳහා වන සීමාවන්ය. සෑම සහතිකයකටම ප්‍රහාරකයා සහ සැසිය සඳහා කොන්දේසි ඇත. ගුප්ත ලේඛනගත ප්‍රාථමිකයන් විශ්වාසදායී කොන්ත්‍රාත්තු පිටුපස සිටී. සාධනය උපකල්පනය කරන්නේ එම රූටීන පිරිවිතරයට අනුව ක්‍රියා කරන බවත්, ගුප්ත ලේඛනගත ආරක්ෂක උපකල්පන මත රඳා පවතින බවත්ය. එක් සාධනයක් මගින් ගුප්ත ලේඛනය කදිම කරයි; අනෙක ප්‍රහාරක සාර්ථකත්ව සම්භාවිතා ගැන තර්ක කරයි.

2:42 දෙකටම ඔවුන් ආවරණය කරන සිදුවීම් සඳහා සීමාවන් ඇත. කුමන ගොඩනැගීම, කුමන දේපල සහ කුමන උපකල්පනදැයි අසන්න. මෙම ප්‍රතිඵලය පර්යේෂකයන්ගේ විධාන රේඛා හානස් එකට අදාළ වේ. කණ්ඩායම් පණිවිඩකරණය අනාගත කාර්යයක් වන අතර, ගණනය කිරීමේ ආකෘතිය බහු-උපාංග තත්ත්වය බැහැර කරයි. සෑම Signal ස්ථාපනයක්ම දෝෂ රහිත යැයි කීම ප්‍රමේයයෙන් පිටතට යයි. පර්යේෂකයන් විසින් මීට පෙර නිවැරදි කරන ලද Signal දෝෂ දෙකක්

පිරිවිතරයට බිඳුණු කේතය ප්‍රතික්ෂේප කළ හැකිද?

3:02 හුදකලා පිටපත් වලට නැවත හඳුන්වා දී ඒවා සම්පාදනය කරන ලදී. පරීක්ෂා කරන ලද සාධනයන් මගින් පෙන්වා දුන්නේ එම ද්විමය ගොනු සංකේතාත්මක ආරක්ෂක ප්‍රමේයය උල්ලංඝනය කරන බවයි. එයින් පිරිවිතරයට සැබෑ බිඳුණු ක්‍රියාත්මක කිරීම් ප්‍රතික්ෂේප කළ හැකිද යන්න පරීක්ෂා කරන ලදී. ඔබේ කොළ පැහැති චෙක් සලකුණට රතු පරීක්ෂණයක් අවශ්‍යයි. Google විසින් පිරිවිතරයන් සහ සාධනයන් පරීක්ෂා කිරීමේ උපදෙස් සමඟ ප්‍රකාශයට පත් කරයි. ගබඩාවේ සඳහන් වන්නේ පිරිසිදු ගොඩනැගීමකට පැය ගණනක් සහ සැලකිය යුතු මතකයක් අවශ්‍ය බවයි. නිවේදනය කියවීම ලැප්ටොප් එකේදී සැලකිය යුතු තරම් පහසුය. දෘඩාංග ආකෘතිය සහ විශ්වාසදායී කොන්ත්‍රාත්තු තවමත් සමාලෝචනය කළ යුතුය.

3:26 මම මෙම කථාංගය සඳහා දැවැන්ත කෞතුක වස්තුව නැවත ගොඩනැගුවේ නැත. අපි ප්‍රකාශිත ප්‍රතිඵලය සහ එහි සීමාවන් වාර්තා කරමු. බාහිර පුද්ගලයන්ට එය පරීක්ෂා කිරීමට මාර්ගයක් ඇත, එය තවත් AI ජයග්‍රාහී වටයකට වඩා මට වැදගත්ය. දැන් උගුල.

නිවැරදි සාධනයකට වැරදි ප්‍රශ්නයකට පිළිතුරු දිය හැකිද?

3:36 Lean හට කිසිවක් පාහේ ඉල්ලා නොසිටින ප්‍රකාශයක නිවැරදි සාධනයක් පිළිගත හැකිය. අසම්භාව්‍ය උපකල්පන මගින් ප්‍රමේයයක් හිස් කළ හැකිය. ප්‍රධාන ප්‍රමේයයට යටින් වළලන ලද අර්ථ දැක්වීමක් වෙනස් කිරීම මගින් ඉලක්කය දුර්වල කළ හැකිය. ලිපිය මගින් මෙය පරීක්ෂා කිරීමට සැලසුම් කරයි. ගේට්කීපර් විසින් සාධන නියෝජිතයන්ට ලිවීමට නොහැකි වන පරිදි රඳවා තබාගත් අනුමත පිරිවිතරයක් තබා ගනී. ඔවුන්ට වෙනම සංශෝධන ක්‍රියාවලියක් හරහා නිවැරදි කිරීම් යෝජනා කළ හැකිය. ආරක්ෂක දුර්වල කිරීමක් විභව දෝෂයක් ලෙස උග්‍ර කරයි. සාධකයාගේ සාර්ථකත්ව ප්‍රකාශයට මෙහි අධිකාරියක් නොමැත.

4:00 මානවයන් විශ්වාසදායී උපකල්පන වල වෙනස්කම් තීරණය කරයි, සෘජුව හෝ ඔවුන්ගේ ප්‍රතිපත්තිය හරහා, සහ සෑම ව්‍යාපාරයකින් පසුවම සංශෝධන සමාලෝචනය කරයි. විශේෂඥ තීන්දුව තවමත් වගකීම දරයි. නියෝජිතයාට වෙනත් පැවරුමක් ඉල්ලා සිටිය හැකිය. එයට තමාටම සමත් ලකුණක් ලබා දිය නොහැක.

චලනය වන ඉලක්ක අල්ලා ගන්නේ කුමක්ද?

4:13 මෙන්න පොරොන්දු වූ පරීක්ෂාව. Lean ගේ සංසන්දකයක් විසින් ප්‍රමේයය සහ එය රඳා පවතින සෑම අර්ථ දැක්වීමක්ම ආරක්ෂිත අනුමත පිටපත සමඟ සසඳයි. එය අවසර ලත් ස්වයංසිද්ධීන් ද පරීක්ෂා කරන අතර, නැවුම් කර්නලයක සාධනය නැවත ධාවනය කරයි. උපකාරක අර්ථ දැක්වීමක් නිශ්ශබ්දව දුර්වල කිරීම මගින් සංසන්දනය කරන දේ වෙනස් කරයි. පිළිගත් සාධනයක් අනුමත ඉලක්කය තහවුරු කළ යුතුය. එය තවමත් ශක්තිමත් ඉලක්කයක් සහ අවංක උපකල්පන තෝරා ගැනීමේ වගකීම මිනිසුන්ට පවරයි. ඔබේම AI වැඩ ප්‍රවාහය සඳහා, පිළිගැනීමේ නිර්ණායක සේවකයාගේ සංස්කරණ අවසර වලින් පිටත තබා

4:37 යෝජිත වෙනස්කම් වෙන වෙනම සමාලෝචනය කරන්න. Google හි ප්‍රතිඵලය එම වෙන් කිරීම සංයුක්ත කරයි. සාධන ලේඛකයා කාර්යය කරයි; පරීක්ෂා කිරීමේ සීමාව මගින් එය ගණන් ගන්නේද යන්න තීරණය කරයි. ඔබට මෙය මම කියනු අසනවාට වඩා කියවීමට අවශ්‍ය නම්, සෑම උදෑසනකම ඔබේ එන ලිපි වෙත නොමිලේ daily diff dot dev හිදී diff එක ගොඩබසිනු ඇත, සබැඳිය පහතින්. එබැවින් අද තීන්දුව වන්නේ SHIP IT.

මම මෙම සාධන වැඩ ප්‍රවාහය SHIP IT කරන්නේද?

4:54 මම මෙම පරීක්ෂා කරන ලද-සාධන වැඩ ප්‍රවාහය SHIP IT කරන්නේ අනුමත හිමිකම පිළිතුර නිපදවන නියෝජිතයාගෙන් වෙන්ව පවතින බැවිනි. මම සෑම ප්‍රතිඵලයකටම විෂය පථය සහ උපකල්පන අමුණා තබන්නෙමි. දායක වන්න, සීනුව ඔබන්න, සහ ඔබ එය වෙනස් ආකාරයකින් මුද්දර දැමුවේ නම් අදහස් වල කියන්න. තවද එය අද සඳහා වන diff එකයි. මම Axrisi වෙතින් Niko. වගකීමෙන් යුතුව ඒකාබද්ධ කරන්න.

මූලාශ්‍ර

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