AlphaProof Code and Signal: การตรวจสอบหลักฐานความปลอดภัยของโค้ดเครื่องและการสันนิษฐานที่เชื่อถือได้

วิดีโอนี้ครอบคลุมอะไรบ้าง

• AI agents สร้างหลักฐานที่เป็นไปได้; เคอร์เนลของ Lean ตรวจสอบว่าหลักฐานเหล่านั้นยืนยันข้อเรียกร้องอย่างเป็นทางการที่มนุษย์อนุมัติหรือไม่
• เป้าหมายที่ได้รับการยืนยันคือชุดคำสั่ง CLI ของ libsignal ที่คอมไพล์แล้วโดยเฉพาะ โดยมีความหมายที่เชื่อถือได้และสัญญาการเข้ารหัสลับ
• การพิสูจน์ไบนารีที่คอมไพล์แล้วจะลบ Rust compiler ออกจากฐานที่เชื่อถือได้สำหรับคุณสมบัติที่ระบุของไบนารีนั้น
• นักวิจัยรายงานการนำข้อผิดพลาดที่เคยแก้ไขแล้วกลับมาใช้ใหม่สองครั้ง ซึ่งละเมิดทฤษฎีความปลอดภัยเชิงสัญลักษณ์ของพวกเขา
• ตัวเปรียบเทียบจะตรวจสอบทฤษฎีและคำจำกัดความที่เกี่ยวข้องทั้งหมดเทียบกับข้อกำหนดที่ได้รับการอนุมัติซึ่งได้รับการป้องกัน; การแก้ไขจะผ่านกระบวนการตรวจสอบแยกต่างหาก

บทถอดเสียงที่แปลแล้ว

แปลจากการบรรยายภาษาอังกฤษต้นฉบับ เสียงและคำบรรยายที่มีให้จะควบคุมโดย YouTube

ใครเป็นผู้ตรวจสอบหลักฐานความปลอดภัยของ AI?

0:00 การตรวจสอบความปลอดภัยของ AI ยังคงฟังดูเหมือนการเชื่อใจแชทบอท ผลลัพธ์ Signal ใหม่ของ Google มาพร้อมกับการพิสูจน์ทางคณิตศาสตร์แยกต่างหาก ตรวจสอบ ในวิดีโอนี้ Google พิสูจน์อะไร? และพวกเขาจะหยุดเอเจนต์จากการเปลี่ยนเป้าหมายได้อย่างไร? นี่คือคำตอบที่เป็นประโยชน์ โมเดลเขียนหลักฐานที่เป็นไปได้ และ Lean ตรวจสอบหลักฐานเทียบกับ ข้อเรียกร้องที่มนุษย์อนุมัติเกี่ยวกับโค้ดที่คอมไพล์แล้วที่เลือกไว้ มนุษย์ยังคงเป็นเจ้าของข้อเรียกร้องและสมมติฐาน

0:21 คุณสามารถตรวจสอบผลลัพธ์ได้โดยไม่ต้องเชื่อคำกล่าวอ้างชัยชนะของโมเดล การตรวจสอบแยกต่างหากจะจับการเปลี่ยนแปลงคำถามอย่างเงียบๆ เราจะติดตามลงไปถึงคำจำกัดความ วันนี้วันอังคารที่สิบพฤศจิกายน และนี่คือ The Daily Diff AlphaProof Code คือกรอบงานของ Google สำหรับการเขียนข้อกำหนดซอฟต์แวร์ด้วย คำแนะนำจากมนุษย์และการสร้างหลักฐานที่ตรวจสอบแล้วด้วย AI agents การศึกษานี้กำหนดเป้าหมาย libsignal ซึ่งเป็นไลบรารี Rust ที่ใช้โปรโตคอลการส่งข้อความของ Signal ภายในโปรแกรม command-line เฉพาะ

0:45 Google ได้ประกาศงานนี้ในวันนี้ เอกสารระบุว่านักวิจัยห้าคนทำงานกว่าสี่สัปดาห์ Agents เขียนหลักฐาน ในขณะที่มนุษย์ใช้ความพยายามส่วนใหญ่ไปกับ ข้อกำหนด ความต้องการได้พบวิธีที่จะกลายเป็น การประชุมที่แพงขึ้น ข้อกำหนดระบุว่าโปรแกรมต้องทำอะไร

ข้อเรียกร้องจะกลายเป็นเป้าหมายการพิสูจน์ได้อย่างไร?

0:59 สิ่งที่ผู้โจมตีควบคุม และสมมติฐานใดที่การโต้แย้งต้องการ ผู้ตรวจสอบถามว่ามันครอบคลุมความปลอดภัยที่ผู้คนให้ความสำคัญหรือไม่ คำตอบที่ตรวจสอบอย่างสวยงามสำหรับคำถามที่อ่อนแอทำให้คำถามนั้นยังคงอยู่ ทีมงานสร้างจากงานวิจัยก่อนหน้าเกี่ยวกับการจับมือของ Signal และกุญแจข้อความ ratchet การวิเคราะห์อย่างเป็นทางการได้ศึกษาการออกแบบเหล่านั้นแล้ว ข้อเรียกร้องของ Google เชื่อมโยงข้อโต้แย้งด้านความปลอดภัยของพวกเขากับการผลิตที่ไม่ถูกแก้ไข การใช้งานไลบรารีที่คอมไพล์แล้ว ซึ่งการออกแบบต้องรอดพ้นจากการสัมผัสกับ โค้ดจริง Ehren Kret ประธานเจ้าหน้าที่ฝ่ายเทคโนโลยีของ Signal

1:27 อธิบายการขยายตัวนอกเหนือจากขอบเขตที่เล็กกว่าของการตรวจสอบก่อนหน้า รายละเอียดการใช้งานรวมถึงข้อความที่ไม่เรียงลำดับ และเซสชันที่เก็บถาวรสำหรับ ข้อความที่ล่าช้า ซอฟต์แวร์จริงเก็บใบเสร็จที่คุณทิ้งไปในแผนภาพที่สวยงาม นักวิจัยคอมไพล์ไลบรารี Rust ที่ไม่ถูกแก้ไขด้วยคอมไพเลอร์มาตรฐาน

ทำไมต้องพิสูจน์ไบนารีที่คอมไพล์แล้ว?

1:41 เป็นไฟล์ปฏิบัติการ Arm 64 Linux ทฤษฎีของพวกเขาอธิบายไบนารีนั้นโดยใช้โมเดลคำสั่งที่เป็นทางการ ครอบคลุมช่องว่างระหว่างโค้ดต้นฉบับและโค้ดเครื่องที่ได้รับการปรับแต่ง ข้อผิดพลาดของคอมไพเลอร์ที่ทำให้คุณสมบัติที่ระบุเสียไปจะทำให้ทฤษฎีของมันเป็นเท็จ ดังนั้นคอมไพเลอร์จึงออกจากฐานที่เชื่อถือได้สำหรับไบนารีนี้ คุณยังคงเชื่อมั่นในโมเดลคำสั่งและตัวตรวจสอบของ Lean ขอบเขตความเชื่อมั่นเปลี่ยนไปแล้ว และมันมีที่อยู่ หลักฐานที่ตรวจสอบแล้วประมาณหกและครึ่งล้านบรรทัดอยู่บนพื้นฐานของประมาณยี่สิบหก

2:06 พันบรรทัดของข้อกำหนดที่เชื่อถือได้และบรรทัดความหมายของคำสั่ง นี่คือจำนวนสิ่งประดิษฐ์ การถือว่ามันเป็นคะแนนความฉลาดก็เหมือนกับการจัดอันดับนักพัฒนาตามขนาดของ โฟลเดอร์โมดูลโหนดของพวกเขา

คุณสมบัติความปลอดภัยใดบ้างที่รอดพ้นจากช่องว่างของการใช้งาน?

2:16 ข้อโต้แย้งครอบคลุมการรักษาความลับและการรับรองความถูกต้องของข้อความ พร้อมด้วยความลับไปข้างหน้าและความปลอดภัยหลังการละเมิดภายใต้โมเดลที่ระบุ สองรายการสุดท้ายอธิบายขีดจำกัดความเสียหายของกุญแจที่ถูกขโมยและการกู้คืนหลังจากการแลกเปลี่ยนใหม่ การรับประกันแต่ละอย่างมีเงื่อนไขเกี่ยวกับผู้โจมตีและเซสชัน Cryptographic primitives อยู่เบื้องหลังสัญญาที่เชื่อถือได้ การพิสูจน์สมมติว่ารูทีนเหล่านั้นทำงานตามที่ระบุและขึ้นอยู่กับข้อสมมติฐานด้านความปลอดภัยของการเข้ารหัสลับ การพิสูจน์หนึ่งอุดมคติการเข้ารหัสลับ; อีกหนึ่งใช้เหตุผลเกี่ยวกับ ความน่าจะเป็นความสำเร็จของผู้โจมตี

2:42 ทั้งสองมีข้อจำกัดเกี่ยวกับสถานการณ์ที่ครอบคลุม ถามว่าสร้างแบบไหน คุณสมบัติแบบไหน และข้อสมมติฐานแบบไหน ผลลัพธ์นี้เกี่ยวข้องกับชุดคำสั่ง command-line ของนักวิจัย การส่งข้อความแบบกลุ่มคืองานในอนาคต และโมเดลการคำนวณไม่รวม สถานะหลายอุปกรณ์ การเรียกทุกการติดตั้ง Signal ว่าปราศจากข้อผิดพลาดนั้นอยู่นอกขอบเขต ของทฤษฎี นักวิจัยได้นำข้อผิดพลาด Signal ที่เคยแก้ไขแล้วสองรายการกลับมาใช้ใหม่ใน

ข้อกำหนดสามารถปฏิเสธโค้ดที่เสียหายได้หรือไม่?

3:02 สำเนาที่แยกออกและคอมไพล์มัน หลักฐานที่ตรวจสอบแล้วแสดงให้เห็นว่าไบนารีเหล่านั้นละเมิดทฤษฎีความปลอดภัยเชิงสัญลักษณ์ นั่นเป็นการทดสอบว่าข้อกำหนดสามารถปฏิเสธการใช้งานที่เสียหายจริงได้หรือไม่ เครื่องหมายถูกสีเขียวของคุณต้องการการทดสอบสีแดง Google เผยแพร่ข้อกำหนดและหลักฐานพร้อมคำแนะนำในการตรวจสอบ ที่เก็บข้อมูลระบุว่าการสร้างใหม่ที่สะอาดใช้เวลาหลายชั่วโมงและหน่วยความจำจำนวนมาก การอ่านประกาศบนแล็ปท็อปนั้นง่ายกว่ามาก โมเดลฮาร์ดแวร์และสัญญาที่เชื่อถือได้ยังคงต้องได้รับการตรวจสอบ

3:26 ฉันยังไม่ได้สร้างสิ่งประดิษฐ์ขนาดใหญ่สำหรับตอนนี้ เรากำลังรายงานผลลัพธ์ที่เผยแพร่และขอบเขตของมัน คนภายนอกมีเส้นทางในการตรวจสอบ ซึ่งสำคัญกว่าชัยชนะของ AI ครั้งอื่นสำหรับฉัน เอาละกับดัก

การพิสูจน์ที่ถูกต้องสามารถตอบคำถามที่ผิดได้หรือไม่?

3:36 Lean สามารถยอมรับการพิสูจน์ที่ถูกต้องของข้อความที่เกือบไม่มีอะไรเลย สมมติฐานที่เป็นไปไม่ได้สามารถทำให้ทฤษฎีว่างเปล่าได้ การเปลี่ยนแปลงคำจำกัดความที่ซ่อนอยู่ใต้ทฤษฎีหลักสามารถทำให้ เป้าหมายอ่อนแอลง เอกสารออกแบบการตรวจสอบเพื่อป้องกันสิ่งนี้ ผู้เฝ้าประตูเก็บข้อกำหนดที่ได้รับการอนุมัติซึ่งไม่ได้ถูกเขียนโดย agents ที่พิสูจน์ พวกเขาสามารถเสนอการแก้ไขผ่านกระบวนการแก้ไขแยกต่างหาก การลดความปลอดภัยจะถูกยกระดับเป็นข้อบกพร่องที่อาจเกิดขึ้น การประกาศความสำเร็จของผู้พิสูจน์ไม่มีอำนาจที่นี่

4:00 มนุษย์ตัดสินการเปลี่ยนแปลงสมมติฐานที่เชื่อถือได้ โดยตรงหรือผ่านนโยบายของพวกเขา และตรวจสอบการแก้ไขหลังแต่ละแคมเปญ ผู้เชี่ยวชาญยังคงรับผิดชอบ เอเจนต์สามารถขอการมอบหมายที่แตกต่างกันได้ มันไม่สามารถให้คะแนนผ่านแก่ตัวเองได้

อะไรเป็นตัวจับเป้าหมายที่เคลื่อนไหว?

4:13 นี่คือการตรวจสอบตามสัญญา ตัวเปรียบเทียบของ Lean เปรียบเทียบทฤษฎีและทุกคำจำกัดความที่ทฤษฎีนั้นขึ้นอยู่กับ กับสำเนาที่ได้รับการอนุมัติที่ได้รับการป้องกันนั้น นอกจากนี้ยังตรวจสอบสัจพจน์ที่ได้รับอนุญาตและเล่นซ้ำการพิสูจน์ในเคอร์เนลใหม่ ดังนั้นการลดความแข็งแกร่งของคำจำกัดความผู้ช่วยอย่างเงียบๆ จึงเปลี่ยนสิ่งที่กำลัง เปรียบเทียบ การพิสูจน์ที่ได้รับการยอมรับจะต้องสร้างเป้าหมายที่ได้รับการอนุมัติ นั่นยังคงทำให้มนุษย์รับผิดชอบในการเลือกเป้าหมายที่แข็งแกร่งและสมมติฐานที่ซื่อสัตย์ สำหรับเวิร์กโฟลว์ AI ของคุณเอง ให้เก็บเกณฑ์การยอมรับไว้นอก

4:37 สิทธิ์การแก้ไขของพนักงาน และตรวจสอบการเปลี่ยนแปลงที่เสนอแยกต่างหาก ผลลัพธ์ของ Google ทำให้การแยกส่วนนี้เป็นรูปธรรม ผู้เขียนหลักฐานทำงาน; ขอบเขตการตรวจสอบจะตัดสินว่ามันนับหรือไม่ ถ้าคุณอยากอ่านสิ่งนี้มากกว่าที่จะได้ยินฉันพูด The Daily Diff จะส่งถึงกล่องจดหมายของคุณ ทุกเช้า ฟรีที่ thedailydiff.dev ลิงก์ด้านล่าง ดังนั้นคำตัดสินของวันนี้คือ SHIP IT

ฉันจะใช้เวิร์กโฟลว์การพิสูจน์นี้หรือไม่?

4:54 ฉันจะจัดส่งเวิร์กโฟลว์การพิสูจน์ที่ตรวจสอบแล้วนี้ เพราะข้อเรียกร้องที่ได้รับการอนุมัติยังคงแยกต่างหาก จากเอเจนต์ที่สร้างคำตอบ ฉันจะเก็บขอบเขตและสมมติฐานไว้กับทุกผลลัพธ์ สมัครสมาชิก กดกระดิ่ง และบอกฉันในความคิดเห็นว่าคุณจะประทับมัน แตกต่างกันหรือไม่ และนั่นคือความแตกต่างสำหรับวันนี้ ฉันชื่อ Niko จาก 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